[Axiom-developer] Proving Axiom Sane and Continuous Reasoning

[Tim Daly]

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