What is a type error?

[Joachim Durchholz]

Darren New schrieb:
> 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?

Yes. It's a classical case where the postcondition and the code that 
fulfils it are essentially the same.

 > 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.

Correct.

OTOH, isn't that the grail that many people have been searching for: 
programming by simply declaring the results that they want to see?

> 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.

No, FPLs are actually just that: compilable postconditions.
Computability issues aren't more or less a factor than with other kinds 
of compilers: they do limit what you can do, but these limits are loose 
enough that you can do really useful stuff within them (in particular, 
express all algorithms).

Regards,
Jo