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