Tim Daly
2018-08-20 08:49:02 UTC
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
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