Re: [repost]Eorros for me, in the assembly history

randyhyde@xxxxxxxxxxxxx wrote:
\o///annabee wrote:


Sure, lablike tenliners. 


No. Full applications.


Many proofs do exist (e.g., there are proofs
that certain implementations of sorting algorithms are correct).

Ok. Same as I am saying. I was talking about fullblown applications. 


As I just said, full-blown applications have been proven correct.  None
that *you* use, of course. But applications *have* been proven correct.
 We're not talking millions of lines here, but I do believe I recall
proofs for apps that were on the order of 10,000 lines of code, or so
(written in Eiffle, IIRC).

IBM's CICS transaction processing system was specified in Z, a language developed for formal correctness proofs. CICS is in the millions of lines of code range.

--
Regards
Aex McDonald

.