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.
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?
> 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.)
> A proof checker meant for education
What makes it for education? Why can't it be used as a general purpose proof checker?
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.
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.