A proof checker meant for education

iNic

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

Start with:

    import List
    import Nat

neverokay

The syntax looks better than some languages and frameworks.

angelaguilera

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.

ameliaquining

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).

fc417fc802

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

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

GitHub should allow arbitrary files in nhe repo, but all repo should require a licence tag

krick

> 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.)

ratmice

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.

vitalmixofntrnt

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

That correspondence doesn't automatically mean you get a useful compiler from proofs. Rather, that's the exception instead of the rule.

tossandthrow

Well, a proven proposition would compile to a unit value.

Files with only proofs would Compile to something akin to main = nil

ndriscoll

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/Intersect...

[1] https://adam.math.hhu.de/#/g/djvelleman/stg4/world/Complemen...

[2] https://adam.math.hhu.de/#/g/djvelleman/stg4/world/FamInter/...

wpollock

I had some correspondence saved from him, but all it says is "Nyuk-nyuk-nyuk!"

amw-zero

Not all proofs have proof terms, so not all proof can be compiled to existing languages.

rendaw

> A proof checker meant for education

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

proof_by_vibes

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

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.

Jtsummers

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).

YetAnotherNick

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).

null

[deleted]

Q6T46nT668w6i3m

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

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

HN

A proof checker meant for education

A proof checker meant for education