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.

The syntax looks better than some languages and frameworks.

Start with:

    import List
    import Nat

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.

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

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.

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"?

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

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

I'm not saying there is. I'm saying there should be. Posting code publicly on github without a licence is entirely pointless

This is similar to saying that posting code anywhere online is useless. Not everyone is trying to start a collaborative project. Sometimes people just use github to showcase code, because it's a convenient platform.

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.

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.

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

Why didn’t you include a copyright license on all your HN comments?

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.

> A proof checker meant for education

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

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.

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

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.

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?

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

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

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

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

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.

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

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

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.

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