Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Sun, 18 Apr 1993 03:43:14 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA09074; Sat, 17 Apr 93 19:07:45 -0700 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA09069; Sat, 17 Apr 93 19:07:37 -0700 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Sun, 18 Apr 1993 03:07:20 +0100 To: Matt Kaufmann Cc: info-hol@edu.uidaho.cs.ted Subject: Proof certification In-Reply-To: Your message of Sat, 17 Apr 93 11:21:59 -0500. <9304171621.AA15796@thunder.CLI.COM> Date: Sun, 18 Apr 93 03:07:14 +0100 From: John Harrison Message-Id: <"swan.cl.ca.126:18.04.93.02.07.23"@cl.cam.ac.uk> One could certainly have some sort of automatic tool to check that a proof didn't cheat. However I think the circumstances in which a "proof" is invalid are sufficiently obvious that most users don't worry about it. There's work in progress interfacing HOL to a separate proof checker. In the next version, a new switch |record_proof_flag| will cause the primitive inference rules to create an ML data structure recording the proof. This can then be spat out as a flat Godel-Hilbert proof, and a separate proofchecker (which may be very simple indeed) can make sure it is valid. One might feel that in view of HOL's high level of security, this is rather gilding the lily, but the procedure is recommended in the UK (Interim) Defence Standard[%]: "32.3.1 In practice, it is very unlikely that Formal Proofs of any size will be created by hand. Instead, they will be developed using theorem proving assistants, which are interactive programs that carry out symbol manipulation under the guidance of a human operator. But theorem proving assistants are large programs whose correctness cannot readily be demonstrated by Formal Proof. It is, however, possible to remove the reliance on the correctness of the theorem proving assistant from the case for correctness of an application by arranging that a version of the final proof (omitting all history of its construction) is passed from the theorem proving assistant to a proof checker. For reasonable languages, such a proof checker could be a very simple program (perhaps ten pages in a functional programming language) that could be developed to the highest level of assurance." John. [%] Interim Defence Standard 00-55 (Part 2: Guidance) / Issue 1 (5 Apr 1991). The Procurement of Safety Critical Software in Defence Equipment. (c) Crown Copyright 1991. Published by and obtainable from: Ministry of Defence Directorate of Standardization Kentigern House 65 Brown Street GLASGOW G2 8EX UK.