[FOM] What are Proofs?

[Steve Stevenson]

> [DeMillo et al.] We believe that, in the end, it is a social process
> that determines whether mathematicians feel confident about a
> theorem....

1. By way of some background, here are some references to start from. The
concept of program proofs was introduced by Robert Floyd.

@article{floyd,
  author =	 {R. W. Floyd},
  title =	 {Assigning Meanings to Programs},
  series =	 {Mathmematical Aspects of Computer Science},
  editor =	 {J. Schwartz},
  journal =	 {Proceedings of Symposia in Applied Mathematics},
  volume =	 {19},
  city =	 {Providence, RI},
  publisher =	 {Amer. Math. Soc},
  year =	 {1967},
  pages =	 {19-32}
}

David Gries and Edsger Dijkstra led a movement for "axiomatic"
semantics of programming languages.

@Article{dijkstra75:_guard,
  author = 	 {Edsger W. Dijkstra},
  title = 	 {Guarded commands, nondeterminacy and formal
                 derivation of programs}, 
  journal = 	 {Communications of the ACM},
  year = 	 1975,
  volume =	 18,
  number =	 8,
  pages =	 {453--457}
}

The other pole is "denotational" semantics based on the lambda
calculus and category theory. I like to use Glynn Winskel.

@Book{winskel,
  author =	 {Glynn Winskel},
  title =	 {The Formal Semantics of Programming Languages},
  publisher =	 {MIT Press},
  year =	 1993
}

Dijkstra and James Fetzer each had an article in the Communications of
the ACM relevant to the program proof issue. Dikjstra wrote "On the
cruelty of really teaching computer science" [Communications of the
ACM 32(12), 1989] and Fetzer wrote "Program Verification - The Very
Idea." [31(9), 1988]. Dijkstra held out for more proving of
programs. Fetzer's article is the more interesting. Fetzer holds "The
notion of program verification appears to trade upon an
equivocation. Algorithms, as logical structures, are appropriate
subjects for deductive verification. Programs, as causal models of
those structures, are not." I tried to pull this together in a talk at
Stanford in 1990: ``1001 Reasons for Not Proving Your Programs
Correct: a survey,''. 5th Conf. in Philosophy and Computer Science,
8-12 Aug., 1990, Stanford University. [paper available]

2. Program Proving as a Social Process.
Intuitionists probably would accept the social aspect. The Stanford
Encyclopedia of Philosophy contains the following quote concening
Brouwer:

"Intuitionism views mathematics as a free activity of the mind,
independent of any language or Platonic realm of objects, and
therefore bases mathematics on a philosophy of mind." So a proof must
exist in at least two minds: that of the prover and that of the
reader. Program proofs are certainly *not* independent of language ---
they're not even independent of compiler version number.

Charles Silvers wrote on 26 January that a proof has a metaphysical
and an epistemic role. But the road to the proof may have several
"non-theorem" versions --- recall Wiles' work on Fermat's Last
Theorem. So during development there is a sociological portion and a
psychological portion. [Nonaka's SECI theory is interesting in this
context. Ikujiro Nonaka, Noboru Konno, The concept of "Ba": Building
foundation for Knowledge Creation. California Management Review Vol
40, No.3 Spring 1998. They present a  system of explaining the
internal (psychology) and external (sociological) use of knowledge in
creative companies].

I conclude that DeMillo et al. are correct about development but not
necessarily about the final product. Theorem proving and proofs of
correctness have been fruitfully used in program specifications and
formal methods models. (http://www.fmeurope.org/). Logic programming
adherents see a program as a proof; any developer in any language
can tell you that getting programs right is no easier than getting
proofs right. For the most part, program development takes place in a
social setting, despite what people think about programmers.


Steve
--------
D. E. Stevenson, School of Computing
Director, Institute for Modeling and Simulation Applications
Clemson University, Clemson, SC
http://www.cs.clemson.edu/~steve