5 ms·

A proof checker meant for education

145 points by alabhyajindal 2y ago

vitalmixofntrnt 2y ago
Because of the Curry Howard Correspondence, do they have a compiler to compile proofs written in this language to machine code, with optional inline assembly support?
- krapht 2y ago
  That correspondence doesn't automatically mean you get a useful compiler from proofs. Rather, that's the exception instead of the rule.
  - tossandthrow 2y ago
    Well, a proven proposition would compile to a unit value. Files with only proofs would Compile to something akin to main = nil
    - ndriscoll 2y ago
      One of the things I dislike about the way these proof languages are documented (at least in tutorials) is that they tend to obscure the programming connection. A proof is a value of the proposition (type) you are proving, not just unit. e.g. `5` is a proof of the proposition `Int`. For a more complicated example, take this level in the Lean Set Theory Game[0]: the proposition A,B,C: Set U, (A∩B)∩C=A∩(B∩C). Here's a possible proof: ext exact ⟨ λ p ↦ ⟨p.left.left, p.left.right, p.right⟩, λ p ↦ ⟨⟨p.left, p.right.left⟩, p.right.right⟩ ⟩ It's kind of weird because the game puts you into tactic mode by default, but the proof here is an actual value: a pair of lambda functions (an "if"/implication is a function, so an "if and only if" is a pair of functions for the two implications). You can actually call those functions within other proofs! Or a maybe simpler example, for this level[1], you can use `exact λ _ xBComp xA ↦ xBComp (h1 xA)` as a one-liner. The proof here is a lambda function. It's an actual value, not unit. Moreover, within that proof, you use e.g. h1: A⊆B as a function that you can call on xA: x∈A to get a proof of x∈B. Proofs are tangible values that you can build, pull apart, pass around, and (often) call. A lot of the set theory levels can be solved with one-liners by thinking about what the proposition actually means as a programming language construct, and then making some clever use of λ and ∘ (compose). e.g. [2] is starting to get into a complicated statement, but has a short proof where you build a pair of lambdas that each require 3 function calls. To some extent, you can even figure it out without knowing about sets and intersections by just "following the types": exact ⟨ λ hASubIntF s hsF a haA ↦ hASubIntF haA s hsF, λ hASubsF a haA s hsF ↦ hASubsF s hsF haA ⟩ Treating proofs as programs and thinking like a programmer is so powerful that it almost feels like cheating in a game about math. Especially when the rules never tell you that constructs like λ exist, and you have to go find it in the language docs. :-) [0] https://adam.math.hhu.de/#/g/djvelleman/stg4/world/Intersection/level/8 https://adam.math.hhu.de/#/g/djvelleman/stg4/world/Intersect... [1] https://adam.math.hhu.de/#/g/djvelleman/stg4/world/Complement/level/3 https://adam.math.hhu.de/#/g/djvelleman/stg4/world/Complemen... [2] https://adam.math.hhu.de/#/g/djvelleman/stg4/world/FamInter/level/5 https://adam.math.hhu.de/#/g/djvelleman/stg4/world/FamInter/...
      - tossandthrow 2y ago
        Idris, F*, etc.? Programmers tend to call it something different because the goal is not to prove mathematical propositions but to prove static guarantees of your program.
      - auggierose 2y ago
        No, a proof is not a value of the proposition you are proving. That is a very convoluted way of thinking about proofs, and just because you can (using some type theory based logic), doesn't mean you should. It is like saying that 2 is the same as {∅, {∅}}, which is true in some set-theoretic formulations of the natural numbers, but which is not how we usually think about 2.
        milesrout 2y ago
        That is an obscure way of writing it. If you use the normal notation you will have that 2 is {0,1} which makes some sense at least: we often see 2 (albeit often bolded or double struck as U+1D7DA) used to mean "the set with two elements" and those elements are often called 0 and 1.
        auggierose 2y ago
        It is not an obscure way of writing it, it means exactly the same as {0, 1}, via Successor(n) = {n} ∪ n, starting with 0 = ∅: 0 = ∅ 1 = Successor(0) = {0} ∪ 0 = {∅} 2 = Successor(1) = {1} ∪ 1 = {{∅}} ∪ {∅} = {{∅}, ∅} = {1, 0} If you don't like the meaning of equality here, that is exactly my point. My point is not that you cannot make sense of 2 = {0, 1}. You can, and this is a corner stone of encoding numbers is set theory, and it certainly describes an aspect of numbers (the set theoretic aspect). But it is not how we understand numbers usually. And the same is true for the "Curry-Howard" way of understanding proofs.
        ndriscoll 2y ago
        I'm not seeing how those are at all the same, or how it's convoluted to think of/require a proof to be an actual demonstration of the thing you are setting out to prove. If you want to prove to me that `A => B`, what other way is there to do so besides giving me logical steps to get from `A` to `B`? If you had a proof-of-A, would that not then be a function that takes your proof-of-A and returns a proof-of-B?
- wpollock 2y ago
  I had some correspondence saved from him, but all it says is "Nyuk-nyuk-nyuk!"
- amw-zero 2y ago
  Not all proofs have proof terms, so not all proof can be compiled to existing languages.
angelaguilera 2y ago
Which kind of software license uses Deduce? The web says it's open source, but I couldn't find the license in the github repository.
- fc417fc802 2y ago
  Wow. It looks like they forgot to add one. I'm a bit surprised that GitHub permits creating new public repos without explicitly tagging a license file.
  - falcor84 2y ago
    You're surprised that GitHub allows people to host arbitrary repos?! Do you really prefer that GitHub would go "I'm sorry Dave, I'm afraid I can't let you do that"?
    - 3836293648 2y ago
      GitHub should allow arbitrary files in nhe repo, but all repo should require a licence tag
      - dymk 2y ago
        Why didn’t you include a copyright license on all your HN comments?
        3836293648 2y ago
        Because I agreed to a TOS that lets HN use my comments and reproduce them. On Github I don't just want to give that permission to github, but to everyone who clones my repo.
        immibis 2y ago
        I am not HN and I don't know if you think I should be allowed to quote your comments. If you included a copyright license, I'd know.
deleted 2y ago
[deleted]
ratmice 2y ago
I've really liked educational proof checkers going back to the tutch proof checker. One thing I didn't see here is the ability to header-like file which declares the type of proofs... the syntax of deduce looks very nice though.
iNic 2y ago
This syntax looks much more friendly than Lean! Could be really great. Complaint about their Live Code environment. I tried running the code on their front-page in the live environment and it gave me `input.pf:2.9-2.12: undefined variable: Nat` which immediately makes me bounce off.
- fn-mote 2y ago
  Start with: import List import Nat
- neverokay 2y ago
  The syntax looks better than some languages and frameworks.
Q6T46nT668w6i3m 2y ago
I’m excited to take a look. I like and usually recommend Daniel Velleman’s “Proof Designer” but I’ve heard from some it’s too obtuse for beginners.
- fn-mote 2y ago
  The vocabulary requirements for "Proof Designer" are certainly higher. This repo is closer to an intro to automated theorem proving than "Proof Designer" is (imo). Less math, more programming. Note: Proof Designer has an excellent list of problems to try to prove. [1] [1]: https://djvelleman.github.io/pd/help/Problems.html https://djvelleman.github.io/pd/help/Problems.html
rendaw 2y ago
> A proof checker meant for education What makes it for education? Why can't it be used as a general purpose proof checker?
- Jtsummers 2y ago
  It doesn't seem as full-featured as other systems at this point. For instance, there doesn't seem to be code generation to go from the proven code to another language (like Rocq, formerly Coq, and others can do).
- proof_by_vibes 2y ago
  I would argue there is merit in keeping a platform separate for the purpose of education. Humans shape their tools that in turn shape themselves. In a general purpose theorem proving environment, such as with Lean, there is a different attitude about what level of abstraction to expose by default. It's less intuitive to a child to have a tutor need to explain what it means for a function to be `unsafe` than it is to explain what it means to `print` an expression. By creating a separate platform, you can set these defaults to curate different kinds of engagement with users. Take the `processing` language as an example. While it's Java under the hood, the careful curation of the programming environment incentivizes learners to play with it like a toy, increasing creative expression and fault-less experimentation.
  - fc417fc802 2y ago
    I agree but it's interesting to observe that occasionally a work can morph. Racket is a good example. Initially an academic toy, these days it performs quite well and has an expansive ecosystem.
- YetAnotherNick 2y ago
  Having worked a little bit in Lean and Agda(which is also educational-ish), Lean has all sorts of magical convenience features. For educational proof checker, I think it would be good to be more clear about things and being more mechanical, have a smaller kernel with lower expressivity of types(have strong normalization, don't have universe polymorphism, Large elimination etc).
krick 2y ago
> for education Is there any standard curriculum course for... this? (Actually, I don't know if it's a good idea to use this for learning, instead of learning Lean, because I imagine that 95% of learning Lean would be Learning its library anyway. But I never actually tried to use these kind of tools for anything.)

145 points by alabhyajindal 2y ago

Because of the Curry Howard Correspondence, do they have a compiler to compile proofs written in this language to machine code, with optional inline assembly support?

krapht 2y ago
That correspondence doesn't automatically mean you get a useful compiler from proofs. Rather, that's the exception instead of the rule.
- tossandthrow 2y ago
  Well, a proven proposition would compile to a unit value. Files with only proofs would Compile to something akin to main = nil
  - ndriscoll 2y ago
    One of the things I dislike about the way these proof languages are documented (at least in tutorials) is that they tend to obscure the programming connection. A proof is a value of the proposition (type) you are proving, not just unit. e.g. `5` is a proof of the proposition `Int`. For a more complicated example, take this level in the Lean Set Theory Game[0]: the proposition A,B,C: Set U, (A∩B)∩C=A∩(B∩C). Here's a possible proof: ext exact ⟨ λ p ↦ ⟨p.left.left, p.left.right, p.right⟩, λ p ↦ ⟨⟨p.left, p.right.left⟩, p.right.right⟩ ⟩ It's kind of weird because the game puts you into tactic mode by default, but the proof here is an actual value: a pair of lambda functions (an "if"/implication is a function, so an "if and only if" is a pair of functions for the two implications). You can actually call those functions within other proofs! Or a maybe simpler example, for this level[1], you can use `exact λ _ xBComp xA ↦ xBComp (h1 xA)` as a one-liner. The proof here is a lambda function. It's an actual value, not unit. Moreover, within that proof, you use e.g. h1: A⊆B as a function that you can call on xA: x∈A to get a proof of x∈B. Proofs are tangible values that you can build, pull apart, pass around, and (often) call. A lot of the set theory levels can be solved with one-liners by thinking about what the proposition actually means as a programming language construct, and then making some clever use of λ and ∘ (compose). e.g. [2] is starting to get into a complicated statement, but has a short proof where you build a pair of lambdas that each require 3 function calls. To some extent, you can even figure it out without knowing about sets and intersections by just "following the types": exact ⟨ λ hASubIntF s hsF a haA ↦ hASubIntF haA s hsF, λ hASubsF a haA s hsF ↦ hASubsF s hsF haA ⟩ Treating proofs as programs and thinking like a programmer is so powerful that it almost feels like cheating in a game about math. Especially when the rules never tell you that constructs like λ exist, and you have to go find it in the language docs. :-) [0] https://adam.math.hhu.de/#/g/djvelleman/stg4/world/Intersection/level/8 https://adam.math.hhu.de/#/g/djvelleman/stg4/world/Intersect... [1] https://adam.math.hhu.de/#/g/djvelleman/stg4/world/Complement/level/3 https://adam.math.hhu.de/#/g/djvelleman/stg4/world/Complemen... [2] https://adam.math.hhu.de/#/g/djvelleman/stg4/world/FamInter/level/5 https://adam.math.hhu.de/#/g/djvelleman/stg4/world/FamInter/...
    - tossandthrow 2y ago
      Idris, F*, etc.? Programmers tend to call it something different because the goal is not to prove mathematical propositions but to prove static guarantees of your program.
    - auggierose 2y ago
      No, a proof is not a value of the proposition you are proving. That is a very convoluted way of thinking about proofs, and just because you can (using some type theory based logic), doesn't mean you should. It is like saying that 2 is the same as {∅, {∅}}, which is true in some set-theoretic formulations of the natural numbers, but which is not how we usually think about 2.
      - milesrout 2y ago
        That is an obscure way of writing it. If you use the normal notation you will have that 2 is {0,1} which makes some sense at least: we often see 2 (albeit often bolded or double struck as U+1D7DA) used to mean "the set with two elements" and those elements are often called 0 and 1.
        auggierose 2y ago
        It is not an obscure way of writing it, it means exactly the same as {0, 1}, via Successor(n) = {n} ∪ n, starting with 0 = ∅: 0 = ∅ 1 = Successor(0) = {0} ∪ 0 = {∅} 2 = Successor(1) = {1} ∪ 1 = {{∅}} ∪ {∅} = {{∅}, ∅} = {1, 0} If you don't like the meaning of equality here, that is exactly my point. My point is not that you cannot make sense of 2 = {0, 1}. You can, and this is a corner stone of encoding numbers is set theory, and it certainly describes an aspect of numbers (the set theoretic aspect). But it is not how we understand numbers usually. And the same is true for the "Curry-Howard" way of understanding proofs.
      - ndriscoll 2y ago
        I'm not seeing how those are at all the same, or how it's convoluted to think of/require a proof to be an actual demonstration of the thing you are setting out to prove. If you want to prove to me that `A => B`, what other way is there to do so besides giving me logical steps to get from `A` to `B`? If you had a proof-of-A, would that not then be a function that takes your proof-of-A and returns a proof-of-B?
wpollock 2y ago
I had some correspondence saved from him, but all it says is "Nyuk-nyuk-nyuk!"
amw-zero 2y ago
Not all proofs have proof terms, so not all proof can be compiled to existing languages.

angelaguilera 2y ago

Which kind of software license uses Deduce? The web says it's open source, but I couldn't find the license in the github repository.

fc417fc802 2y ago
Wow. It looks like they forgot to add one. I'm a bit surprised that GitHub permits creating new public repos without explicitly tagging a license file.
- falcor84 2y ago
  You're surprised that GitHub allows people to host arbitrary repos?! Do you really prefer that GitHub would go "I'm sorry Dave, I'm afraid I can't let you do that"?
  - 3836293648 2y ago
    GitHub should allow arbitrary files in nhe repo, but all repo should require a licence tag
    - dymk 2y ago
      Why didn’t you include a copyright license on all your HN comments?
      - 3836293648 2y ago
        Because I agreed to a TOS that lets HN use my comments and reproduce them. On Github I don't just want to give that permission to github, but to everyone who clones my repo.
        immibis 2y ago
        I am not HN and I don't know if you think I should be allowed to quote your comments. If you included a copyright license, I'd know.

deleted 2y ago

[deleted]

ratmice 2y ago

I've really liked educational proof checkers going back to the tutch proof checker. One thing I didn't see here is the ability to header-like file which declares the type of proofs... the syntax of deduce looks very nice though.

iNic 2y ago

This syntax looks much more friendly than Lean! Could be really great. Complaint about their Live Code environment. I tried running the code on their front-page in the live environment and it gave me `input.pf:2.9-2.12: undefined variable: Nat` which immediately makes me bounce off.

fn-mote 2y ago
Start with: import List import Nat
neverokay 2y ago
The syntax looks better than some languages and frameworks.

Q6T46nT668w6i3m 2y ago

I’m excited to take a look. I like and usually recommend Daniel Velleman’s “Proof Designer” but I’ve heard from some it’s too obtuse for beginners.

fn-mote 2y ago
The vocabulary requirements for "Proof Designer" are certainly higher. This repo is closer to an intro to automated theorem proving than "Proof Designer" is (imo). Less math, more programming. Note: Proof Designer has an excellent list of problems to try to prove. [1] [1]: https://djvelleman.github.io/pd/help/Problems.html https://djvelleman.github.io/pd/help/Problems.html

rendaw 2y ago

> A proof checker meant for education What makes it for education? Why can't it be used as a general purpose proof checker?

Jtsummers 2y ago
It doesn't seem as full-featured as other systems at this point. For instance, there doesn't seem to be code generation to go from the proven code to another language (like Rocq, formerly Coq, and others can do).
proof_by_vibes 2y ago
I would argue there is merit in keeping a platform separate for the purpose of education. Humans shape their tools that in turn shape themselves. In a general purpose theorem proving environment, such as with Lean, there is a different attitude about what level of abstraction to expose by default. It's less intuitive to a child to have a tutor need to explain what it means for a function to be `unsafe` than it is to explain what it means to `print` an expression. By creating a separate platform, you can set these defaults to curate different kinds of engagement with users. Take the `processing` language as an example. While it's Java under the hood, the careful curation of the programming environment incentivizes learners to play with it like a toy, increasing creative expression and fault-less experimentation.
- fc417fc802 2y ago
  I agree but it's interesting to observe that occasionally a work can morph. Racket is a good example. Initially an academic toy, these days it performs quite well and has an expansive ecosystem.
YetAnotherNick 2y ago
Having worked a little bit in Lean and Agda(which is also educational-ish), Lean has all sorts of magical convenience features. For educational proof checker, I think it would be good to be more clear about things and being more mechanical, have a smaller kernel with lower expressivity of types(have strong normalization, don't have universe polymorphism, Large elimination etc).

krick 2y ago

> for education Is there any standard curriculum course for... this? (Actually, I don't know if it's a good idea to use this for learning, instead of learning Lean, because I imagine that 95% of learning Lean would be Learning its library anyway. But I never actually tried to use these kind of tools for anything.)