What is a type error?

[Darren New]

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.