One of the (many) reasons people feel that proving code is unacceptable is that every change requires a proof check. This is certainly the case. Of course, code that implements known mathematical functions would have far fewer changes as the specifications would not change.
But, then, every change to a code base SHOULD require a code review. Part of that review would be to check that the change is 'sane' (e.g. passes a proof check against specifications). Since code development is a continuous process, Peter O'Hearn has suggested that proof technology should also be continuous. His paper "Continuous Reasoning: Scaling the Impact of Formal Methods" (LICS 18, ACM, ISBN 978-1-4503-5583) talks about this idea and gives examples from Facebook. They have a tool, called "Infer" that is run on code patches and generates comments (likely proof obligations but I don't know for sure) that would be discussed during code review. The current design for proving Axiom sane includes a compiler stage that does proof checking. Failing proofs would generate proof obligations as "error messages". Peter's paper is worth a read. Tim
_______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
