[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=EBl 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=EBl