Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 15 Jul 1994 14:58:23 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA21572; Fri, 15 Jul 1994 07:44:42 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA21568; Fri, 15 Jul 1994 07:44:40 -0600 Received: from life.ai.mit.edu by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA08654; Fri, 15 Jul 1994 06:41:09 -0700 Received: from spock (spock.ai.mit.edu) by life.ai.mit.edu (4.1/AI-4.10) for info-hol@cs.uidaho.edu id AA05846; Fri, 15 Jul 94 09:40:44 EDT From: dam@ai.mit.edu (David McAllester) Received: by spock (4.1/AI-4.10) id AA08494; Fri, 15 Jul 94 09:40:41 EDT Date: Fri, 15 Jul 94 09:40:41 EDT Message-Id: <9407151340.AA08494@spock> To: Richard.Boulton@cl.cam.ac.uk Cc: vac@air16.larc.nasa.gov, info-hol@cs.uidaho.edu In-Reply-To: Richard Boulton's message of Fri, 15 Jul 94 10:57:20 +0100 <"swan.cl.cam.:249340:940715095732"@cl.cam.ac.uk> Subject: FM etiquette and accuracy I have not been following this discussion very closely, so I apologize if this is redundant. I have always used the term "rigorous" to refer to acceptable mathematical arguments in English and "formal" to refer to well formed proofs in artificial langauges such as FOL, HOL etc. Common practice amoung mathematicians seems to be to use "formalize" to refer to the translation from nonrigorous to rigorous. In the FM community I would like to see the term formalize reserved for the translation from rigorous to formal. I think that the primary problem facing the FM community is that, even with state of the art automated support, formalizing a given rigorous argument is usually extremely time consuming and requires considerable training above and beyond that needed to construct and verify (by hand) rigorous arguments. David McAllester