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.
neverokay [3 hidden]5 mins ago
The syntax looks better than some languages and frameworks.
fn-mote [3 hidden]5 mins ago
Start with:
import List
import Nat
angelaguilera [3 hidden]5 mins 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.
ameliaquining [3 hidden]5 mins ago
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 [3 hidden]5 mins 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 [3 hidden]5 mins 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 [3 hidden]5 mins ago
GitHub should allow arbitrary files in nhe repo, but all repo should require a licence tag
"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."
3836293648 [3 hidden]5 mins ago
I'm not saying there is. I'm saying there should be. Posting code publicly on github without a licence is entirely pointless
andrewflnr [3 hidden]5 mins ago
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.
laGrenouille [3 hidden]5 mins ago
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.
fc417fc802 [3 hidden]5 mins ago
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 [3 hidden]5 mins ago
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).
dymk [3 hidden]5 mins ago
Why didn’t you include a copyright license on all your HN comments?
3836293648 [3 hidden]5 mins 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.
rendaw [3 hidden]5 mins ago
> 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 [3 hidden]5 mins 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.
Jtsummers [3 hidden]5 mins 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).
ratmice [3 hidden]5 mins 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.
vitalmixofntrnt [3 hidden]5 mins 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 [3 hidden]5 mins ago
That correspondence doesn't automatically mean you get a useful compiler from proofs. Rather, that's the exception instead of the rule.
tossandthrow [3 hidden]5 mins ago
Well, a proven proposition would compile to a unit value.
Files with only proofs would Compile to something akin to main = nil
ndriscoll [3 hidden]5 mins 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. :-)
Programmers tend to call it something different because the goal is not to prove mathematical propositions but to prove static guarantees of your program.
amw-zero [3 hidden]5 mins ago
Not all proofs have proof terms, so not all proof can be compiled to existing languages.
wpollock [3 hidden]5 mins ago
I had some correspondence saved from him, but all it says is "Nyuk-nyuk-nyuk!"
Q6T46nT668w6i3m [3 hidden]5 mins 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 [3 hidden]5 mins 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]
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."
On Github I don't just want to give that permission to github, but to everyone who clones my repo.
What makes it for education? Why can't it be used as a general purpose proof checker?
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.
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.
Files with only proofs would Compile to something akin to main = nil
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":
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/...
Programmers tend to call it something different because the goal is not to prove mathematical propositions but to prove static guarantees of your program.
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