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/