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
http://www.thenewsh.com/~newsham/
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
