Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Date: Fri, 16 Apr 93 18:41:27 -0700
From: val@com.netcom (Dewey Val Schorre)
Message-Id: <9304170141.AA24517@netcom2.netcom.com>
To: info-hol@edu.uidaho.cs.ted
Subject: Worried about mk_tac and the philosophy of ML


In a recent reply, John Harrison mentioned the function mk_tac. The 
reference manual says that it can be used to create a theorem any time
you want to.

Could not some unscrupulous person post a large HOL file alleging to 
prove Fermat's Last theorem, but really containing a mk_thm imbedded 
somewhere? Recipients might be intimidated by the size and complexity 
of the file and so would not bother to study it, but merely run it 
through their HOL system and conclude that the famous theorem had 
indeed been proved.

Perhaps the person posting this file was not unscrupulous at all. 
Perhaps he was in the habit of introducing reasonable lemmas with 
mk_thm and, after proving the original theorem, going back and 
replacing these mk_thm's with actual proofs. It would be easy to 
overlook one of these lemmas and think that the whole theorem had been
proved.

How can we be sure that nothing like this has happened in our HOL 
libraries?

-----------

Now I'm beginning to wonder if there was any advantage of writing HOL 
in ML rather than some other language, such as LISP. One could 
represent a theorem in LISP in the form:

     ('|-' (assumptionLIst) conclusion)

The LISP version of basic-HOL would implement various functions, such 
as rules of inference, that would return theorems. Outside basic-HOL, 
one would be on his honor not to create the atom '|-' except by calls 
on functions in basic-HOL.

There is no way in the LISP system to check that an illegal theorem 
has not been created. ML would make such a check if mk_thm weren't 
available, but it is. So what's the advantage of implementing HOL in 
ML instead of LISP?

I'm probably all mixed up. Somebody please straighten me out.

Val