Not fully OO ?

[Lawrence D'Oliveiro]

In message
<f9b466b0-9945-42c1-ad9c-2f65c8d4b907 at y38g2000hsy.googlegroups.com>,
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.