On 07/06/2010, at 3:05 AM, Michael Schuerig wrote: > I have a hunch that the real restrictions of this kind of software are > not concerned with fixed memory, iterations, whatever, but rather with > guaranteed bounds. If that is indeed the case, how feasible would it be > to prove relevant properties for systems programmed in Haskell?
For full Haskell that includes laziness and general recursion: not very. Proving properties about the values returned by functions is one thing, but giving good guaranteed upper bounds to the time and space used by an arbitrary program can be very difficult. See for example: J ̈orgen Gustavsson and David Sands, Possibilities and limitations of call-by-need space improvement, ICFP 2001: Proc. of the International Conference on Functional Programming, ACM, 2001, pp. 265–276. Adam Bakewell and Colin Runciman, A model for comparing the space usage of lazy evaluators, PPDP 2000: Proc. of the International Conference on Principles and Practice of Declarative Pro- gramming, ACM, 2000, pp. 151–162. Hans-Wolfgang Loidl. Granularity in Large-Scale Parallel Functional Programming. PhD Thesis. Department of Computing Science, University of Glasgow, March 1998. I expect future solutions for this domain will look more like the Hume (family of) languages [1]. They give several language levels, and can give stronger bounds for programs using less language features. [1] http://www-fp.cs.st-andrews.ac.uk/hume/index.shtml _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
