In message <[EMAIL PROTECTED]>, 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. -- http://mail.python.org/mailman/listinfo/python-list
