Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 23 Jun 1993 15:47:55 +0100 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA06291; Wed, 23 Jun 93 07:36:03 -0700 Sender: info-hol-request@ted.cs.uidaho.edu Errors-To: info-hol-request@ted.cs.uidaho.edu Precedence: bulk Received: from air52.larc.nasa.gov by ted.cs.uidaho.edu (16.6/1.34) id AA06286; Wed, 23 Jun 93 07:35:59 -0700 Received: by air52.larc.nasa.gov (5.65.1/lanleaf2.4) id AA06115; Wed, 23 Jun 93 10:34:46 -0400 Message-Id: <9306231434.AA06115@air52.larc.nasa.gov> Date: Wed, 23 Jun 93 10:34:46 -0400 From: Victor "A." Carreno To: slind@informatik.tu-muenchen.de Subject: Re: HOL portability In-Reply-To: Mail from 'Konrad Slind ' dated: Tue, 22 Jun 1993 18:18:26 +0200 Cc: info-hol@ted.cs.uidaho.edu slind@informatik.tu-muenchen.de writes: Richard> 2. HOL90 is not as mature as HOL88, and in my opinion has only Richard> recently become mature enough for serious use. >This is a terribly ambiguous statement. Others have used hol90 seriously >for at least the past 2 years. Certainly the system is not in a mature >state, documentation-wise, since it depends on the hol88 documentation. Some times the intangible and ambiguous things are the ones which ultimately count. As long as there are statements like, "has anyone translated `res_quan` and `more_lists` to HOL90? >chou", HOL88 is going to continue to be "the" standard against which all HOLs are compared. Notice that Chou did not say "translated `res_quan` and `more_lists` from HOL88 to HOL90." The maturity of a system is not only its technological fitness but also the perception people have of it. On Monday, I saw in horror how Wordperfect (word processing) is still offered as an introductory course at the local community college, despite it being obsolete and the fact that far superior programs for word processing exist.