comments

"Richard Schroeppel" <rcs@cs.arizona.edu>

Mail folder: QED
Next message: David McAllester: "the base logic"
Previous message: Gene Rackow: "manifest"

Date: Tue, 13 Apr 1993 11:56:17 MST
From: "Richard Schroeppel" <rcs@cs.arizona.edu>
Message-id: <199304131856.AA23651@leibniz.cs.arizona.edu>
To: qed@mcs.anl.gov
Subject: comments
Sender: qed-owner
Precedence: bulk

This manifesto should be signed.
You didn't provide any contact information!
I'd suggest posting the "who" list now, and annually.

Could some knowledgable person provide a capsule review of
work already done?  No sense starting in a vacuum.  There
may be public domain work available that's worth using,
or existing proofs worth converting.  If the existing work
is proprietary, perhaps the owners could be persuaded to
donate portions.  We need to know what's worked, and what hasn't.

My personal language preferences are (1) editor of your choice for
proof creation, including Emacs & WordPerfect (2) Lisp for turning
that proof into a checkable file (3) C for checking the low-level
proof, based on matching character strings.  The low-level checker
should be simple enough that it can be easily implemented in several
languages, including C & Fortran, and perhaps even assembly code.
(This, on the theory that the less complex software you believe,
the better.)  The spec for the checker should be unambiguous, so that
anyone can implement a checker from the spec, and expect it to work.
Ideally, the low-level checker is only a few pages of code; it's
required that it be totally understandable in detail by a single person.
The low-level data files should be human readable, and include comments
with the high-level proof.  The working character set should be emailable.

Rich Schroeppel  rcs@cs.arizona.edu