[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Axiom-developer] Proving Axiom Sane and Continuous Reasoning

From: Tim Daly
Subject: [Axiom-developer] Proving Axiom Sane and Continuous Reasoning
Date: Mon, 20 Aug 2018 04:49:02 -0400

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.


reply via email to

[Prev in Thread] Current Thread [Next in Thread]