[fpc-pascal] Competitive advantage in showing proof of correctness

[Daniël Mantione]

Op Tue, 14 Aug 2007, schreef Vinzent Hoefler:

> On Tuesday 14 August 2007 06:14, Daniël Mantione wrote:
> 
> > Lastly, pre and post conditions are just another runtime check.
> 
> No. If you can prove that the conditions always hold, you don't even 
> need to compile to the program to prove its correctness.

This isn't feasible. Read on the internet about the Hoare calculus and 
how is only feasible to do it for small programs. However, those programs 
aren't a problem to get correct anyway.

There is no realistic way you can prove that a program like FPC itself is 
correct.

Daniël