I would venture the proofs are not the real effort in CompCert. The real effort is to formulate the various systems such that the proofs become as simple as possible. So 15.77% is minuscule compared to the total intellectual effort of this project. Your job is not yet in danger (even in your retirement :-)
But, seriously, sometimes I am worried that too much automation is a bad thing, because it can mask the flaws in what one is doing. There are many examples in the study of logics, but let me use programming instead. Start with your favorite terrible programming language (Python happens to be a convenient target, or C++). Now, sure, you can reduce the number of bugs with automatic program analysis, the smarter the better. But you would nevertheless still be better off in a statically typed functional language with a decent module system. You prop up something that would be better left to wither and die. - Frank On Sun, Jul 21, 2019 at 8:29 AM Tim Daly <axiom...@gmail.com> wrote: > Generating Correctness Proof with Neural Networks > https://arxiv.org/pdf/1907.07794.pdf > > Apparently they managed to prove 15.77% of the proofs in > the CompCert verified compiler effort. > > "Now, here, you see, it takes all the running you can do to > keep in the same place. If you want to get somewhere else, > you must run at least twice as fast as that." > -- Alvin Toffler "Future Shock" :-) > > Tim > -- Frank Pfenning, Professor Computer Science Department Carnegie Mellon University Pittsburgh, PA 15213-3891 http://www.cs.cmu.edu/~fp +1 412 268-6343 GHC 6017
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer