Joachim Durchholz wrote:
> Actually, in a functional programming language (FPL), you write just the
> postconditions and let the compiler generate the code for you.
Certainly. And my point is that the postcondition describing "all valid
chess boards reachable from this one" is pretty much going to be as big
as an implementation for generating it, yes? The postcondition will
still have to contain all the rules of chess in it, for example. At best
you've replaced loops with some sort of universal quanitifier with a
"such that" phrase.
Anyway, I expect you could prove you can't do this in the general case.
Otherwise, you could just write a postcondition that asserts the output
of your function is machine code that when run generates the same
outputs as the input string would. I.e., you'd have a compiler that can
write other compilers, generated automatically from a description of the
semantics of the input stream and the semantics of the machine the code
is to run on. I'm pretty sure we're not there yet, and I'm pretty sure
you start running into the limits of computability if you do that.
--
Darren New / San Diego, CA, USA (PST)
This octopus isn't tasty. Too many
tentacles, not enough chops.
--
http://mail.python.org/mailman/listinfo/python-list
