Feedback on De Millo et al Paper

Hypotheses: 

	De Millo, Lipton and Perlis advance many hypotheses, but there is
one major one which is:

	Mathematical proof involves an essential social process,
	but such social processes are impossible in formal
	verifications because of their huge size and
	uninteresting nature.

Evidence: 

	The authors advance informal arguments based on their experience
of mathematics and formal verification. They exhibit one short
example of a conjecture from formal verification to illustrate
their claim about its lack of simplicity.

	Most of you identified this hypothesis and the evidence
for it, although many of you broke it into smaller chunks and
added some of the subsidiary hypotheses. Many of you accepted the
argument uncritically, so I'll focus below on some of the
criticisms that you might have made. I'll also point up some of
the more common errors made in the critiques.

Possible Criticisms: 

	Although you should always review these papers from the viewpoint
of their times, it is also useful to look ahead at some of the
developments since then, since these may help identify gaps or
errors. Currently, we can see that formal verification has had
some significant successes. For instance, model checking, which is
logic-based, black-box proof of the kind that the authors thought
would be useless, is in widespread use, especially for
hardware verification. Also, we have tactic-based, interactive
theorem provers and proofs of properties, such as exception
freedom, which stop short of full functional verification. These
all suggest some possible gaps. On the other hand, we now know
that the paper caused a huge controversy and was influential in
the way that formal verification developed. Their prediction was
correct in that full functional correctness of complete,
industrial-strength programs has never become routine.

* It could be (and has been) argued that a full, logical proof
was the ideal, even for mathematicians, but that its
unattainability for non-trivial proofs, at least without a
computer, had led to the development of the social process as an
imperfect substitute. This would turn the authors' argument on its
head. Since they rehearsed their argument to hostile audiences
before publication, they would certainly have heard this
counter-argument, so it is surprising that they do not even
discuss it, let alone argue against it. 

* It is crucial to their argument that formal verification proofs
defy readability. However, with the aid of tactic-based provers,
long proofs can be chunked, with long, routine passages hidden
from the reader. By doing this hierarchically, even very long
proofs can be abstracted to resemble human proofs. Also, such a
high-level proof account can sometimes be unpacked in different
ways, e.g. one way to verify the original program and another
way to verify a modified version. Thus, there is reason to
believe that verifying a modified program is easier than
verifying the original, in contradiction to the claim at the
bottom of p278.

* Their argument refers to full, functional proofs, i.e. that a
program's outputs have some mathematical relation to its
inputs. However, it is possible to prove simpler properties with
correspondingly simpler proofs. For instance, exception freedom
proofs ensure that a program will not produce a runtime error and
just stop, even if they produce the wrong output or
behaviour. Such proofs are important, for instance, for
fly-buy-wire aircraft. These proofs may be more understandable. 

* Similarly, formal verification can be applied, not to the whole
of a program, but to some part that is especially critical,
e.g. for safety or security reasons. This also simplifies the
verification proof. 

* They point out, correctly, that a verifier is much more likely to
fail than to succeed. However, they fail to mention that such
verification failures can be accompanied by a counter-example,
that can then be used to locate a bug. Model-checkers, for
instance, are mostly used in this way to find bugs, rather than
to prove correctness. Finding bugs is useful even if the failed,
partial proof is totally opaque.

* Their Fig 1 is a straw man. I've never known a formal
verification expert draw this analogy. They all use the analogy
in Fig 2, which the authors claim, incorrectly, as a novel
contribution. 


Common Errors:

* Informal argument, perhaps appealing to analysis of case
studies, is a common and legitimate form of evidence for a
hypothesis. Sometimes it is the only kind of evidence that can be
feasibly provided. Of course, it is especially prone to error, so
care must be taken to consider all counter-arguments and
non-supporting case studies. 

* "One step ahead of the pack" is a poor summary of the originality
of this work, which was novel and not subsequently duplicated. In
fact, none of the summaries offered in the ERA drop-down menu is
appropriate. [This is one of the many deficiencies of ERA. Is any
MSc student interested in improving it for their project?]

* This paper does not really describe a new problem as much as
advance a hypothesis. Nor is it a literature survey in the normal
understanding of that term.