[HN Gopher] A proof checker meant for education
___________________________________________________________________
A proof checker meant for education
Author : alabhyajindal
Score : 114 points
Date : 2025-03-21 11:47 UTC (3 days ago)
(HTM) web link (jsiek.github.io)
(TXT) w3m dump (jsiek.github.io)
| vitalmixofntrnt wrote:
| 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 wrote:
| That correspondence doesn't automatically mean you get a useful
| compiler from proofs. Rather, that's the exception instead of
| the rule.
| tossandthrow wrote:
| Well, a proven proposition would compile to a unit value.
|
| Files with only proofs would Compile to something akin to
| main = nil
| ndriscoll wrote:
| 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 < l p - <p.left.left,
| p.left.right, p.right> , l 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 l _ 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 l 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 <
| l hASubIntF s hsF a haA - hASubIntF haA s hsF, l
| 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 l exist, and you have to go find it in the
| language docs. :-)
|
| [0] https://adam.math.hhu.de/#/g/djvelleman/stg4/world/Inte
| rsect...
|
| [1] https://adam.math.hhu.de/#/g/djvelleman/stg4/world/Comp
| lemen...
|
| [2] https://adam.math.hhu.de/#/g/djvelleman/stg4/world/FamI
| nter/...
| tossandthrow wrote:
| 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.
| wpollock wrote:
| I had some correspondence saved from him, but all it says is
| "Nyuk-nyuk-nyuk!"
| angelaguilera wrote:
| 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 wrote:
| 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 wrote:
| 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 wrote:
| GitHub should allow arbitrary files in nhe repo, but all
| repo should require a licence tag
| roflmaostc wrote:
| Why? There is no legal requirement for a LICENSE
|
| https://docs.github.com/en/repositories/managing-your-
| reposi...
|
| "You're under no obligation to choose a license. However,
| without a license, the default copyright laws apply,
| meaning that you retain all rights to your source code
| and no one may reproduce, distribute, or create
| derivative works from your work."
| fc417fc802 wrote:
| Because that use case feels pretty far from the typical
| one for a public GitHub repo. Even when it was intended,
| having reliable metadata indicating that fact would be
| nice.
| falcor84 wrote:
| Absolutely agreed, but there's a vast difference between
| "would be nice" and "should require". I for one strongly
| prefer to avoid putting up any additional barriers to
| sharing, even at the cost of the default value being all
| rights reserved (which is a sensible default).
| laGrenouille wrote:
| I have read the quoted GitHub docs page before and also
| found it somewhat odd. Not because it shouldn't be
| allowed to post public code without a LICENSE (or with a
| restrictive one), but because GitHub has a "Fork" button
| on every repository. It's strange to me that GitHub has a
| one-click button that can violate the default terms of
| code uploaded to the site.
| dymk wrote:
| Why didn't you include a copyright license on all your HN
| comments?
| ameliaquining wrote:
| They've now added a LICENSE file. Seems they went with the
| Boost Software License (a fairly simple permissive license
| similar to the MIT License).
| ratmice wrote:
| 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 wrote:
| 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 wrote:
| Start with: import List import Nat
| neverokay wrote:
| The syntax looks better than some languages and frameworks.
| Q6T46nT668w6i3m wrote:
| 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 wrote:
| 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
| rendaw wrote:
| > A proof checker meant for education
|
| What makes it for education? Why can't it be used as a general
| purpose proof checker?
| Jtsummers wrote:
| 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 wrote:
| 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.
___________________________________________________________________
(page generated 2025-03-24 23:01 UTC)