[SystemSafety] Faults in maths proofs

[Roberto Bagnara]

On 10/12/20 16:54, Derek M Jones wrote:
 > There is some discussion of the use of programs to create proofs,
 > and the problem that software contains faults, just like mathematical proofs.

Nonetheless, properly-said proofs created by programs can be presented
as sequences of logical statements, each of which either is an axiom
or can be obtained by means of an inference rule from statements
occurring earlier in the sequence.  So a proof-checker is a much
simpler program than a proof-creator: it will scan the sequence from
the beginning, check whether the required set of prerequisites (none
for the axioms) are there, and whether the deduction step matches an
inference rule.

All this to say that gaining solid confidence in the correctness of a
properly crafted proof-checker is a feasible task.  Such a checker can
be used to validate the output of proof-creators, no matter the
technology used to develop them.

I enjoyed Kevin Buzzard's slides very much: thanks for sharing them.
Kind regards,

    Roberto

-- 
      Prof. Roberto Bagnara

Applied Formal Methods Laboratory - University of Parma, Italy
mailto:bagnara at cs.unipr.it
                               BUGSENG srl - http://bugseng.com
                               mailto:roberto.bagnara at bugseng.com