Karl Palmskog (Jun 21 2020 at 11:34): Karl Palmskog (Jun 21 2020 at 11:34):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?
Kevin Buzzard (Jun 21 2020 at 12:58):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.
Karl Palmskog (Jun 21 2020 at 13:03):@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.
Mario Carneiro (Jun 21 2020 at 13:05):Dependent type theory would be a closer approximation, but even then DTT does not strictly imply propositions as types
Mario Carneiro (Jun 21 2020 at 13:06):An example would be something like dependent haskell
Karl Palmskog (Jun 21 2020 at 13:16):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.)
Pierre-Marie Pédrot (Jun 21 2020 at 15:18):What do you people call "propositions as types"? I am a bit confused by the claims in this thread...
Pierre-Marie Pédrot (Jun 21 2020 at 15:19):there are computational interpretations of HOL, even with Hilbert's epsilon and classical logic
Pierre-Marie Pédrot (Jun 21 2020 at 15:20):and what do you call DTT? The mere ability to have the corner corresponding to λΠ in PTS?
Pierre-Marie Pédrot (Jun 21 2020 at 15:21):my personal take on this is that the huge gap between CIC and both HOL/λΠ comes from dependent elimination
Pierre-Marie Pédrot (Jun 21 2020 at 15:22):without it, the λΠ part of a language can be erased (e.g F + Π is essentially equivalent to F)
Pierre-Marie Pédrot (Jun 21 2020 at 15:22):and you can't even phrase dependent elimination in HOL, so...
Karl Palmskog (Jun 21 2020 at 18:52):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).
Karl Palmskog (Jun 21 2020 at 19:17):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).
Karl Palmskog (Jun 22 2020 at 15:21):@Pierre-Marie Pédrot so what's your type theorist take, can/should a HOL proof be viewed as a program?
Paolo Giarrusso (Jun 22 2020 at 18:36):It's even hard to take HOL _functions_ as programs, since function "definitions" need not fix their behavior uniquely.
Paolo Giarrusso (Jun 22 2020 at 18:38):(see fromSome in https://www.joachim-breitner.de/blog/732-Isabelle_functions__Always_total%2C_sometimes_undefined)
Karl Palmskog (Jun 22 2020 at 19:50):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)
Pierre-Marie Pédrot (Jun 22 2020 at 20:54):HOL "functions" correspond to Coq functional relations, so it's not surprising that it's hard to extract it directly to a functional language
Pierre-Marie Pédrot (Jun 22 2020 at 20:56):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
Pierre-Marie Pédrot (Jun 22 2020 at 20:56):(the typical setting for HOL computational content would be some kind of classical realizability)
Last updated: Apr 19 2024 at 00:02 UTC