This recent blog post by Kevin Buzzard in my reading mixes up type theories in general with type theories based on propositions-as-types: https://xenaproject.wordpress.com/2020/06/20/mathematics-in-type-theory/
Key quote:
Unifying the concept of a number and a proof — thinking of them both as terms — enables you to think of proofs as functions. Lean is a functional programming language, and in particular it is designed with functions at its heart. This, I believe, is why theorem provers such as Lean, Coq and Isabelle/HOL, which use type theory, are now moving ahead of provers such as Metamath and Mizar, which use set theory.
To my knowledge, no informed Isabelle/HOL user (or type theorist using Church's simple theory of types) would think of writing proofs in HOL as writing functions (at least, as functions in any way like HOL functions). But perhaps someone with more type theory background could weigh in?
I have no clue about these details -- I am a mathematician and am essentially completely uninformed about type theory. What I say bears some sort of resemblance to what is going on in Lean. My audience is mathematicians; my goal is to tempt them into trying these computer proof systems. I tried earlier on to write super-precise posts, asking computer scientists to read through them and debug them etc -- but after a while I made a "design decision" to concentrate on getting material out there.
Another change in my approach was that earlier on I would only talk about Lean; I would try to sell it as "the one true theorem prover". Going to conferences and talking to people who do know things about this area, and in particular to users of other systems, made it clear to me that it was not at all the case that Lean was obviously the answer; furthermore, the idea began to crystallise in my mind that perhaps the point was not to get mathematicians using Lean, it was to get mathematicians using any theorem prover at all. I am also very much aware of the fact that I upset a bunch of Coq users with some uninformed comments last year, and this was not my intention; I am not out to cause trouble -- I am out to change the world by getting mathematicians into this area. So I am now much more careful to namecheck other theorem provers, but of course the disadvantage of this approach, as you're now seeing, is that whilst I could be regarded as a competent Lean user, I have had far far less experience with all of the other provers. I could go back to "Lean does this, this is how Lean works, Lean Lean Lean, forget the others it's all Lean" but I think this would be a step backwards.
Currently one of my main goals is to get an undergraduate pure mathematics curriculum into Lean. I think that this is a trick which all these systems have missed; it somehow seems to be regarded as unimportant by computer scientists. I think it will turn mathematicians' heads. But more than that, I think it will teach computer scientists what mathematicians actually want from these systems.
I am sorry for my crappy ignorant blog posts. My target audience are the people I know best -- undergraduate mathematicians. They don't have a clue about functional programming languages or the difference between HOL and DTT. I want them to see that there's a new way of thinking about mathematics. I want to create a paradigm shift. I am sick of talking to the staff, the researchers -- they can't see any problems with the old pencil and paper way. My posts are not supposed to be read by experts and I'm sure that I write a lot of rubbish when I'm talking about CS. What I want to argue is that by just throwing myself into this area I am ultimately doing more good than harm.
@Kevin Buzzard thanks for explaining the approach, all I was hoping for here was someone expert to confirm my reading. I think it's good in general that type theory is discussed by mathematicians, and your approach is reasonable to me. The differences between Isabelle/HOL/Lean/Coq and their theories are often discussed in the Coq community, e.g., I made an attempt to summarize the foundational differences between HOL Light and Coq here.
Dependent type theory would be a closer approximation, but even then DTT does not strictly imply propositions as types
An example would be something like dependent haskell
Kevin Buzzard said:
I want them to see that there's a new way of thinking about mathematics. I want to create a paradigm shift. I am sick of talking to the staff, the researchers -- they can't see any problems with the old pencil and paper way.
This is a different discussion, but for the record, I completely support this goal. I personally work on techniques&tools that usually work for most/all proof assistants. (E.g., lemma naming suggestion technique we did for Coq could likely be adapted to Lean 4.)
What do you people call "propositions as types"? I am a bit confused by the claims in this thread...
there are computational interpretations of HOL, even with Hilbert's epsilon and classical logic
and what do you call DTT? The mere ability to have the corner corresponding to λΠ in PTS?
my personal take on this is that the huge gap between CIC and both HOL/λΠ comes from dependent elimination
without it, the λΠ part of a language can be erased (e.g F + Π is essentially equivalent to F)
and you can't even phrase dependent elimination in HOL, so...
Pierre-Marie Pédrot said:
What do you people call "propositions as types"? I am a bit confused by the claims in this thread...
Quoting for example Harper:
The great idea of constructive type theory is that there is no distinction between programs and proofs: the code embodies the reasoning [that] justifies it, and the reasoning is just a form of code. This is the propositions as types principle (sometimes grandly called the “Curry-Howard isomorphism”, the small problem being that neither Curry nor Howard invented it, nor is it an isomorphism). Theorems are types (specifications), and proofs are programs.
My point was essentially that someone working in HOL (via Isabelle/HOL, HOL4, HOL Light, etc.) doesn't necessarily think of proofs as programs in this sense. There is no obvious way in these tools to think of, e.g., a HOL proof of A ==> B
as a function that takes a term of type A and produces a term of type B (HOL proofs are typically just lists of Gentzen-style sequents).
Hence, it seems far from obvious to me that "The proof of Fermat’s Last Theorem [will be] a function" (last section of the blog post).
@Pierre-Marie Pédrot so what's your type theorist take, can/should a HOL proof be viewed as a program?
It's even hard to take HOL _functions_ as programs, since function "definitions" need not fix their behavior uniquely.
(see fromSome
in https://www.joachim-breitner.de/blog/732-Isabelle_functions__Always_total%2C_sometimes_undefined)
good point, this also becomes painfully obvious to anyone using CakeML's synthesis tooling (which translates HOL abstract functions to computable SML-style functions, and often fails at this)
HOL "functions" correspond to Coq functional relations, so it's not surprising that it's hard to extract it directly to a functional language
if you accept to do this identification, HOL proof terms are definitely some kind of programs, at least much more than anything like a proof in ZF
(the typical setting for HOL computational content would be some kind of classical realizability)
Last updated: Dec 07 2023 at 06:38 UTC