Not fully OO ?

Lawrence D'Oliveiro ldo at geek-central.gen.new_zealand
Sun Sep 28 08:08:50 CEST 2008

In message
<f9b466b0-9945-42c1-ad9c-2f65c8d4b907 at>,
Aaron "Castironpi" Brady wrote:

> I understand that formal proof systems, as well as automated
> theorem provers, have been difficult to develop.

The basic problem is: having proved that a program satisfies certain
formally-specified criteria, how do you prove that those formal criteria
specifications actually correspond to the original problem you were trying
to solve? The proof just pushes the correctness problem back another level.

More information about the Python-list mailing list