30 May
2007
30 May
'07
8:39 a.m.
Ketil Malde wrote:
On Tue, 2007-05-29 at 21:39 +0100, Andrew Coppin wrote:
Also, for most programs the spec is far more complicated (and hence prone to error) than the actual program, so...
Since the program *is* a (complete) specification of itself, a specification need not be any longer or more complicated than the program.
Almost. A program usually specifies too much, namely how a problem is solved, not only that it's solved. But in 20-30 years when the Curry-Howards isomorphism rules the world, the types *are* the specification and the compiler won't accept anything that doesn't match them. Dependent types for world-domination! :) Regards, apfelmus