George Necula has an impressive list of papers mainly on one important aspect of the subject. One of his papers involved a great deal of notation, some of it broadly known only among logicians and some of it even restricted to those studying computer proofs. I do not complain about this in an academic paper but I do note that there are nearly 100 references an the end, mostly not online, with no guidance as to where these notations were introduced. I presume that they were introduced somewhere in those papers. I have heard Necula talk and I believe that he knows what he is talking about and has a sense for the need for simplicity. Here he gives a clear outline of his ideas that I think are feasible. If the papers are obscure due to pressures of academic publishing, such as not revisiting preceding work, then this may be a serious impediment to the flow of ideas from academia in the world of real computers.
In particular I reject the notion implicit in the style of these papers, that just a few people need to understand these proof mechanisms and that others should merely trust those who do. This is an adequate model in many technical areas but not in regards to proofs. It seems clear to me that people will need to aid in the production of proofs for real programs and this will require of them a fair grasp of proof theory, but perhaps no more than gained in a good classic geometry course.
I have in mind a careful description of the syntax and semantics of the proof language; I do not have in mind a social engineering pamphlet describing why you should trust the inventors of these systems. As Einstein said: A theory must be as simple as possible, but no simpler!
I claim that is it possible and necessary to provide a theory of proof in a self-contained reference work. The work should bridge the gap between intuition and formal proof concept so that the careful reader can begin to understand why a proof checking program should be believed. There are fairly slim volumes on symbolic logic that do a very good job of introducing proof theory and they would not be twice as long if they provided sufficient information on a proof checker.
The Mizar project seems to have similar aims regarding a registry of machine checked proofs in several areas of fundamental mathematics. There is a short syntax for the proof input language, but I have found no clear semantics for the language. Perhaps I have not looked long enough. Then again perhaps it is not there.
This site looks promising. Too much here to grok.
Note that modus ponens and the axioms for first order predicate logic are extremely simple to understand; they are typically introduced in the first few weeks of the first course in symbolic logic. That is sufficient mathematical background for proof theory. Natural deduction as mentioned below can be seen to be equivalent to the axioms plus modus ponens by a short simple meta proof. Sometimes natural deduction is introduced as a formal system instead of axioms.
I highly recommend this book by Fitch.
A side issue is whether one should trust proofs too long for a person to read. This issue now confronts mathematicians, who seem now to be gradually and grudgingly admitting computer proofs into their world, such as for Kepler’s conjecture. (recent news) Computer people are likely to trust computer checked proofs somewhat as they would trust a computer to add a billion integers without error. The program to add the integers is likely to be small indeed and the proof checker should be as lucid (and small) as possible. There will be those who need to be convinced of program correctness who are neither computer people nor mathematicians. For those a priesthood is perhaps necessary, but a broader priesthood will fare better.
There are these worries:
[Fitch 1952] Frederic Brenton Fitch, Symbolic Logic, the Ronald Press Company, New York, 1952.Here is at least a pretty good online introduction to Fitch’s proof style.
My skimpy notes on proofs.
Tracking down obscure symbols.
I hope I find time to study this thesis.