[Haskell-cafe] Reasoning [was: Tutorial on Haskell]

Tim Newsham newsham at lava.net
Wed Apr 18 14:43:12 EDT 2007

> One of the truly powerful things about Haskell is the short distance between 
> theory and practicality.
> But the ability to reason about programs has borne fruit that I *do* 
> think they will appreciate.  Because many of them care about 
> performance.

This is a topic I've been trying to learn more about.  I appreciate
that the language is pure, referentially transparent and that the
semantics have even been formally spelled out.  I like that there
are tools like quickcheck that can be used to automate testing of
formally stated properties.   Now on to the next step...

   - extended static checking -- I'm aware of haskell ESC, but its
     not yet available.  Are there any available tools for statically
     checking program properties (rather than testing for them)?

   - What about program proofs?  Are there any systems that tie
     directly into haskell and let you augment your haskell program
     with a proof that can be machine checked?  I know that some
     groups have taken haskell, translated to isabelle/hol and then
     done proofs in that system.

I would love to be able to make a model (specification), prove some 
properties on it, create a real program based on the model, and by a 
combination of proof (when possible or convenient) and testing (when 
proofs become too cumbersome) assure myself that the program has the same 
properties or show equivalence to the model.  I would love to be able to 
do all of this inside the haskell system (or at least in a system with 
minor extensions to haskell -- ie. proofs could be contained in comments).

> R Hayes
> rfhayes<>@</>reillyhayes.com

btw: semi related question -- are there any tools that can chase down
the closure of all functions called by a program?  Ideally showing it
in graph form?  ie. to track down all calls to "error" in a program.

Tim Newsham

More information about the Haskell-Cafe mailing list