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

[Vinzent Hoefler]

On Tuesday 14 August 2007 06:49, Daniël Mantione wrote:
> 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.

Ok. I'll tell Rod what his company is doing for years now, just ain't 
possi^Wfeasible. ;)
Of course, you won't have much success with a language like Object 
Pascal, but I'd suggest reading a bit about SPARK before.

And yes, FPC as it is is unprovable (first through all the language 
constructs used and second the problem most projects will suffer from: 
it isn't written with proving it in mind).

OTOH, AFAIK, the correctness of the SPARK Examiner is proven. And those 
are a little bit more than just a dozen lines of code. Of course, it 
goes nowhere near a couple of millions of lines of code, but FPC does 
neither, if you just talk about the compiler. And correctness of stuff 
like the RTL can be proven independently from the compiler itself.


Vinzent.