The question is motivated by this surprising sentence from Freek Wiedijk's The QED Manifesto Revisited.
I agree that the QED-like systems that exist today are not good enough to start developing a library as is described in the QED manifesto.
Surprising to me, that is, who had not heard of the QED project before.
(Edited after A. Bauer's answer) OK, time I mopped up.
I was 1st introduced to the Curry-Howard correspondence back in school days long, loooooong ago; I understood it as s/th along the lines of "Any computer program is a constructive proof that inhabitation of its input type entails inhabitation of its output type"; my very next question was, "OK then, if instead of any program we restrict ourselves to programs that model mathematical proofs in classical logic, what would be the proper type system(s) for them?". I guessed it had to be existential types, guarded subtypes (meaning types restricted by any formula; so that you would write e. g. "let x: {r : Real | !(r : Rational)}
" if all you mean is to express that x is irrational), or such like stuff; then I let the matter rest and turned to more pressing ones, to wit, getting a degree.
If I had pressed it further at the time &, instead of the title question, asked "What types are to classical logic as simple types are to constructive logic?", maybe I'd have been answered "There are no such types: there is no need to extend or otherwise modify simple types for classical logic, since it is encompassed in constructive logic. Go get some understanding of type theory, and learn how to do with them. "
If I had asked again at the time the QED manifesto was issued, a plausible answer might have turned to "They're called refinement types. What's wrong with them is, they're a pointless gadget: the problem they solved was not a foundational one, and introducing them did not present type theory with any new challenge. So all the papers they deserve have been written already. "
Returning to it now, it seems to me the natural way to attack the QED challenge would be: 1. to set forth a serious answer to my old question, 2. design the corresponding language, 3. build the proper language tools, including, in the end, a full-fledged proof assistant (probably posing as a type checker), 4. look what happens. In a programming language with refinement types, the C-H correspondence now works as: subprograms returning (refinements of) void model conjectures, their bodies model proof outlines, assertions in the bodies model steps in the proof, Skolem functions arise naturally if handlers for failed assertions are allowed. Then, verified theorems in predicate logic are those subprograms in which the type checker has been able to reduce all assertions to tautologies.
What hopefully would happen if a suitable extension to such a language had become popular is, useful tools could start developing, such as doclets to turn fragments of source code to academic papers; people might get used to writing in it just to convert formulas from .pdf to .ps, or to save themselves the hassle of adjusting to the style guides of every other journal they submit to; later, we might dream of replacing arXiv with a global GitHub repository of their works. This could take place long before any proof assistant worth mentioning existed for the language.
Given Wiedijk's paper though, the real story must have been quite different. It reads like people trying to endow dependent types with refinement soon hit some snag and, instead of developing proof assistants (Edit: read formal languages and tools) for classical logic, they went happily to rewrite classical math for constructive logic. (Edit) With predictable results: mathematicians have been accepting a certain style of proof outline for some time now and non-mathematicians are used to it, so if it is too arcane work to make it understandable by a automated checker, they will rather dispose of the proof checker than of the proof.
Turn away for a minute from what dependent types mean, and look how they would be used in a language purporting to be strongly typed. The user is student X with a major in control systems, a hobby in Java programming, currently at grips with an intro to topological groups. So far, he has managed to translate "pick any dyadic integer " as "let x: Integer(2)
" for proof-checking freeware he downloaded a minute ago, then "consider first the case of a rational integer" to "let x1:Integer(2)*Rational
"; now attacking "pick some irrational number x and consider the fractional parts of the p.x's, p ranging over Z: obviously, blah blah blah". Not understanding a word of type theory, he first looks for a way to say "let x: Real - Rational
", finds none, looks harder, still finds none, then let go & turns back to more pressing matters, to wit, control systems.
Of course, if student X had access to such a language as I sketched, he would have given up long before he got any proof automated. No harm done, though: what he wants is to understand TG's, not that a computer program understand it in his stead, nor to understand type theory. All he needs is to keep his fingers busy while reading, and I advocate giving him a productive way to do just that.
My read of Wiedijk's paper is, if you bar student X from modelling things the way he understands them, he will turn to what he considers more pressing matters, regardless of how pressing your need for computer-checkable proofs, and how deep your understanding of what the modelling language guarantees. It explains how we still lack a free-access, widely-known, low-quality, multi-audience, computer-interpreted codebase of mathematical theories the way we have a free-access, widely-known, low-quality, multi-audience, human-readable textbase of common lore.
Edit Just to clarify: the codebase of mathematical theories in question would still be as far away from being computer-checked, as is WP from auto-generating ontologies for the subject matter of its articles; light-yrs away. The (hopeful) progress lies in the rest of the road being mostly for metamathematicians & software engineers to tread, with the part of "ordinary" mathematicians perceived as non-problematic.
Hence my question: what type systems are the natural ones to express assertions in classical logic? Or maybe I should have titled this post "What types are to dependent types, as refinement types à la Freeman-Pfenning are to simple types?". Anyway, what have they that makes their theory so unsavory?