Expansion Factors

• Mail folder: QED
• Next message: Larry Wos: "reactions"
• Previous message: Alan Bundy: "Re: Document -- What's Done and What's to be Done"

From: dam@ai.mit.edu (David McAllester)
Date: Mon, 26 Apr 93 09:46:53 EDT
Message-id: <9304261346.AA02209@spock>
To: qed@mcs.anl.gov
Subject: Expansion Factors
Sender: qed-owner
Precedence: bulk

While I was at Cornell we had many discussions about "expansion
factors" --- how much larger a rigorous informal proof becomes before
it can be machine verified.  As noted, tactical systems seem to make
the measurement more difficult --- parts of the proof can be hidden in
special purpose tactics.  An honest measure of length would count
everything that you have to add to prove the theorem, including all
the new "general purpose" theorems and tactics.  I think one just has
to use one's best judgement when making claims about expansion
factors.  One also has to examine any such claim carefully.  But I do
think that meaningful measurements can be made.  You may have to count
"lines of code" in both proofs and tactics.

As many programmers know, however, lines of code is not always a good
measure of the difficulty of writing a given piece of software (or
proof).

	David