[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 08:08, Florian Klaempfl wrote:
> > Vinzent Hoefler schrieb:
> > > 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.
> > >
> > > There's a company already doing that:
> > >
> > > http://www.praxis-his.com/sparkada/intro.asp
> >
> > As long as they can't prove that Goedel is wrong I don't believe in
> > it :)
> 
> Well, I've seen it in action. And I don't see the reference to Goedel 
> here. Basically it's predicate logic, which is - according to Goedel - 
> both complete and correct.
> 
> Of course, they can't solve the halting problem. But most systems they 
> design are not designed to halt, anyway. ;)

Very true. You can't solve the problem of deciding wether two programs are 
equivalent either, that is simply uncomputable.

You can only that a compiler in such a language performs the *intended* 
Pascal->Assembler transformation correctly, not that the transformation 
produces an assembler program with identical functionality as the Pascal 
program.

Unfortunately the process of designing a transformation from Pascal to 
assembler that is both efficient and correct is difficult.

So, would it be the end of bugs? Not at all. You would prevent 
implementation bugs, not design bugs.

Check the bug repository how mbug reports are due to implementation 
bugs (internalerror, crash) and how many due to design bugs (incorrect 
code generation, incompatibility, standard conformance).

Daniël