> Has anyone here actually formally proved a non trivial program, say a couple of hundred lines on NCSS?
I don't know what NCSS is, so am going to answer as if your sentence stopped two words earlier.
How about the CompCert C compiler [1]? Or CakeML [2]?
And let's not forget seL4 [3], which has a formal proof that the implementation in C conforms to the specification, and a further formal proof that the binary code is a correct translation of the C code.
I don't know what NCSS is, so am going to answer as if your sentence stopped two words earlier.
How about the CompCert C compiler [1]? Or CakeML [2]?
And let's not forget seL4 [3], which has a formal proof that the implementation in C conforms to the specification, and a further formal proof that the binary code is a correct translation of the C code.
[1] http://compcert.inria.fr/compcert-C.html
[2] https://cakeml.org
[3] https://sel4.systems