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.
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"?
"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 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).
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.
Now you really are being silly. Most content on the internet doesn't have an explicit license. It's in no way legally dubious to look at it. Code is not special in this regard.
No, you're being disingenuous. Why are you looking at code? It isn't prose you read for fun. You are actively working with it. Which means you're working on some form of derivative work, which takes us back to the copyright issue.
If I'm looking at everything else on the internet with the purpose of trying to transform it in some way, that's definitely a potential copyright issue.
I'm not being disingenuous. It's not quite for fun, but sometimes I do read code to learn from it. Lots of stuff on github is just for portfolio purposes.
Your last sentence basically admits that the fundamental legal situation of code and prose, independent of usage, is the same. If your only possible interest in code is to "transform it in some way", that's your problem, not ours.
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?
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. :-)
No, a proof is not a value of the proposition you are proving. That is a very convoluted way of thinking about proofs, and just because you can (using some type theory based logic), doesn't mean you should. It is like saying that 2 is the same as {∅, {∅}}, which is true in some set-theoretic formulations of the natural numbers, but which is not how we usually think about 2.
I'm not seeing how those are at all the same, or how it's convoluted to think of/require a proof to be an actual demonstration of the thing you are setting out to prove.
If you want to prove to me that `A => B`, what other way is there to do so besides giving me logical steps to get from `A` to `B`? If you had a proof-of-A, would that not then be a function that takes your proof-of-A and returns a proof-of-B?
A proof is already logical steps to get from proposition A to proposition B. What you're requesting is that it should be replaced with logical steps to get from a value of type A to a value of type B, where types A and B aren't ordinary object-class types suck as "pencil" or "employee" or "goblin", nor ordinary data-structure types such as "pair(int, list(string))", but (in most cases) some completely abstract labels that you made up in order for this mapping to work. You have a cool demonstration of disjunction elimination, which of course is no simpler than actual disjunction elimination, but how will you prove something non-constructive like "x mod 2 = 0 → not (x mod 4 = 1)" in your system, and how will it not be more complicated than proving it without your system?
You mentioned passing in axioms as extra assumptions, like the law of the excluded middle. In programming terms, the law of the excluded middle is a magical function that, for every type T, returns an Either<T,Not<T>> - Not<T> being one of those made up types that only exist to make the correspondence work and don't actually mean anything. If you're working with Not you presumably also want a function that takes any Not<Not<T>> and returns a T. In programming terms this is completely unimplementable and meaningless so I'm not really sure why you think it would be useful.
They are values though! That's my whole point! These languages are constructed and written about in a way that often obscures that. A lot of them are simple things like tuple(x: int, y: int, h: x<y). Here's a constructive proof of your proposition:
import Mathlib.Data.Nat.ModEq
example (h: x ≡ 0 [MOD 2]): ¬(x≡1[MOD4]) := λ xeq1mod4 ↦ by
have h24 : 2 ∣ 4 := ⟨2,by tauto⟩
have h' := (h.congr (xeq1mod4.of_dvd h24)).mp (by rfl)
contradiction
You can see at one point, I make a proof that 2|4, which is a data structure that needs to remember that 2 is the solution to 2*n=4 as the proof. Then I pass that to a couple functions (lemmas) that require that assumption, and get an Iff, which is a pair of implications (lambda functions) going each direction. I pull out one of them and call it on a trivial proof of `x=x`. This all gives me a proof that 0=1 mod 2. Finally I can ask it to expand that definition until it reaches a contradiction.
The whole thing is a proof that if you give me a proof that x=0 mod2 and x=1 mod4, I can build you a contradiction. Exactly like you'd expect in a proofs class. Since I'm a programmer, I wrote the whole thing as a big lambda function.
Note that Not[T] is also not some arcane thing. It's just Function[T,Void]. Essentially, it's a function you could never possibly call (because the whole point is that you can't get a T to call it), but if you did, it would just crash the program/throw an exception. It has an obvious purpose if you're trying to formally prove a negative.
The use of a reader monad to get a constructive-ish proof of things that need AC or LEM is just what programmers might call dependency injection. It's a normal pattern (in programming). It only "doesn't mean" something if you don't believe in those axioms at all, but even then many proofs don't need the full axiom and will work if you can bring your own choice function (e.g. you already have a basis for your vector space). Just like many (most?) real world programs basically don't need a turing machine, and actually work fine as a DFA with a trivial event loop or something.
Fwiw, you can easily construct a ¬¬T from a t: T: `λ f↦f(t)` (so make a closure that remembers your t:T and passes it into any ¬T someone gives it). LEM essentially says all ¬¬T are of this form, so you can extract the T that's hidden inside. Sort of like how functionals in finite dimensions are all secretly hiding a vector to do a dot product.
Still sounds like a lot of programming that's not useful for programming but rather just adds extra complexity to proving by pretending it is programming. I don't need a function that returns undefined if I pass it an object that's 0 mod 2 and 1 mod 4 at the same time.
You're in a thread about proof assistants. I'm not saying it's useful to prove number theory facts in your business code. I'm saying it's useful to embrace programming and intentionally think like a programmer to do proofs. You're the one who asked about number theory proofs.
It is also useful to think like a mathematician to do programming, and I find that e.g. scala's ecosystem is a lot easier to work with for business problems than others like go or php because things tend to have more structure and predictable design, but that's a separate issue.
I have contributed to proof assistants, and while programming is part of mathematics, it is not all of it. Obviously, a proof assistant is a program, but its concepts don't need to be all about programming. If they are, that is to the detriment of the mathematics done in the proof assistant.
Another comparison you won't like: Insisting to phrase everything in terms of electrical engineering is quite useless for most applications running on a computer.
I didn't say you always need to phrase things in those terms, merely that it can be useful to not try to avoid them (and I wish tutorials wouldn't obscure it). It's like how geometers use d/dx as an element of the tangent space, but they don't treat it as some quirk to ignore. They actually use the fact that it's an operator too. It makes things easier. Obviously you don't need to do that with every vector space you'll ever encounter.
My original reply was to someone who thought proofs are all unit valued, which is the sort of confusion you get when these systems try to shy away from the programming part. The point was that proofs are things that a programmer ought to feel to be concrete, not just some trickery with type aliases of unit.
That is an obscure way of writing it. If you use the normal notation you will have that 2 is {0,1} which makes some sense at least: we often see 2 (albeit often bolded or double struck as U+1D7DA) used to mean "the set with two elements" and those elements are often called 0 and 1.
If you don't like the meaning of equality here, that is exactly my point.
My point is not that you cannot make sense of 2 = {0, 1}. You can, and this is a corner stone of encoding numbers is set theory, and it certainly describes an aspect of numbers (the set theoretic aspect). But it is not how we understand numbers usually.
And the same is true for the "Curry-Howard" way of understanding proofs.
To be more specific, propositions that can be written in the form "some member of X exists" can be proven by specifying such a member. Thanks to the ability to define dummy sets with 0 or 1 element, while keeping them separate with types, this is quite a lot of propositions - surprisingly many. But it's not a useful programming or proving technique.
What propositions cannot be written this way? If your answer is along the lines of "things that use the axiom of choice" or "things that use LEM", then you can instead prove `AC -> P` or `LEM -> P`, which are constructible (assuming no similar missing "magic" axioms, but those can be solved with the same technique). Then we can again look at programming where we have the Reader monad as a way to pretend `AC -> P` is just `P` and use it as if it were (but with the ability to pull `AC` out of a hat when needed). Arguably then, we can only prove `AC -> P` and not `P` itself because `P` is not true (obviously that's a controversial take).
For very practical programming work (like business software), I'd be surprised if there were any useful programs that can't be boiled down to `while True: f(x)` where f(x) is some finite terminating program that you can prove stuff about. When you do a bunch of work in a language/ecosystem like Scala's, you get used to the idea that if your function says it returns an A, then it returns an A; there's generally no failure modes to consider if they're not in the type (ignoring realities like a datacenter catching on fire that are outside of the programming model). Passing a B to a `Function[B,A]` is an actual proof that you now have an `A` in your hand.
Programmers tend to call it something different because the goal is not to prove mathematical propositions but to prove static guarantees of your program.
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.)
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.
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.
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).
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).
