Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Message-Id: <9403141832.AA02733@puma.cs.byu.edu>
To: info-hol@leopard.cs.byu.edu
Subject: [markaa@box.EE.CORNELL.EDU (Mark D. Aagaard): terminology: "rigor" vs 
         "formality" ?]
Date: Mon, 14 Mar 1994 11:32:26 -0700
From: Phil Windley <windley@lal.cs.byu.edu>


We've been having trouble with our mail server, so I've been collecting
messages to info-hol.  We think it might be fixed, so I'll send this one.
If it doesn't generate a million error messages, I'll forward the other two
I have.  Apologies for any inconvinience.  If you get errors from this,
please let me know.

------- Forwarded Message

Organization: Cornell University, Electrical Engineering, Ithaca NY 14853
X-Address: 389 Engineering and Theory Center
X-Phone: (607) 255 0302
X-Fax: (607) 255 9072
X-Mailer: Mail User's Shell (7.2.4 2/2/92)
To: info-hol@cs.uidaho.edu
Subject: terminology: "rigor" vs "formality" ?

Recently I was trying to figure out how to describe the difference
between paper proofs and mechanized proofs such as those done in HOL,
Nqthm, Nuprl, Isabelle, Coq, etc.  I was considering using the words
`formal' and `rigorous' or `more formal' and `more rigorous', but
wasn't sure of the exact difference between rigor and formality.  I
remember having read a description somewhere that said that a tool was
`formal' if it could verify a property without enumerating all
possible cases, but didn't recall any relevant definitions of rigor.
To help with this problem I turned to the dictionary, thinking that it
could help me decide whether mechanized proofs are more rigorous or
more formal than paper proofs.  The results were somewhat interesting:


rigor:

1a1: harsh inflexibility in opinion, temper, or judgment : SEVERITY
1a2: the quality of being unyielding or inflexible : STRICTNESS)
    Mechanized proof systems are rather stubborn and unyielding when
    they don't believe a `theorem' is true, and they aren't very
    flexible about their definition of truth either.

1a3: AUSTERITY
    You might say that HOL's interface is a bit austere.

1b: an act or instance of strictness, severity, or cruelty
    Cruelty? Well some people might think that using a proof system
    constitutes cruel and unusual punishment.

2: a tremor caused by a chill
    Rumors have it that some ex-users still shudder at the sight of `?-'

3: a condition that makes life difficult, challenging, or uncomfortable;
    No doubt about this one.

4: strict precision : EXACTNESS {logical ~}
    I believe that this is what is *meant* when proof systems are
    advertised as being more rigorous.  Unfortunately it ended up
    at the end of the list of possible definitions.


formal:

1a: belonging to or being the essential constitution or structure.
    Even paper proofs would claim to capture the essential structure.

1b: relating to, concerned with, or constituting the outward form of
something as distinguished from its content.
    Hardware verification is supposed to aid in abstracting away from
    unnecessary details and does separate the implementation from the
    specification, but this doesn't seem unique to mechanized proofs.

2a: following or according with established form, custom, or rule :
CONVENTIONAL 2b: done in due form : CEREMONIAL 3a: based on conventional forms
and rules 3b: characterized by punctilious respect for form : METHODICAL 3c:
rigidly ceremonious : PRIM
    Conventional, rigidly ceremonial, and prim --- not exactly words that I
    would associate with the volleyball games I've seen at HUG.

4: having the appearance without substance : NOMINAL
    Not a very positive comment about the quality of a proof.

So, I'm leaning towards using `rigorous' for mechanized proofs and
`formal' (or `prim') for paper proofs.

  Any suggestions, comments or other solutions?

 -mark aagaard
  markaa@ee.cornell.edu


------- End of Forwarded Message