5 ms·

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.

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/Intersection/level/8 https://adam.math.hhu.de/#/g/djvelleman/stg4/world/Intersect... [1] https://adam.math.hhu.de/#/g/djvelleman/stg4/world/Complement/level/3 https://adam.math.hhu.de/#/g/djvelleman/stg4/world/Complemen... [2] https://adam.math.hhu.de/#/g/djvelleman/stg4/world/FamInter/level/5 https://adam.math.hhu.de/#/g/djvelleman/stg4/world/FamInter/...

tossandthrow 2y ago
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.
auggierose 2y ago
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.
- milesrout 2y ago
  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.
  - auggierose 2y ago
    It is not an obscure way of writing it, it means exactly the same as {0, 1}, via Successor(n) = {n} ∪ n, starting with 0 = ∅: 0 = ∅ 1 = Successor(0) = {0} ∪ 0 = {∅} 2 = Successor(1) = {1} ∪ 1 = {{∅}} ∪ {∅} = {{∅}, ∅} = {1, 0} 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.
- ndriscoll 2y ago
  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?
  - immibis 2y ago
    Nobody else is seeing how it is not convoluted. 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. It seems like you might be suffering from fuckarounditis: https://news.ycombinator.com/item?id=43466252 https://news.ycombinator.com/item?id=43466252
immibis 2y ago
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.
- ndriscoll 2y ago
  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). I don't know what strategies they're using, but mathlib in Lean has formalizations for measure theory for example: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/MeasureTheory/Measure/MeasureSpace.lean https://github.com/leanprover-community/mathlib4/blob/master... 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.

tossandthrow 2y ago

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.

auggierose 2y ago

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.

milesrout 2y ago
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.
- auggierose 2y ago
  It is not an obscure way of writing it, it means exactly the same as {0, 1}, via Successor(n) = {n} ∪ n, starting with 0 = ∅: 0 = ∅ 1 = Successor(0) = {0} ∪ 0 = {∅} 2 = Successor(1) = {1} ∪ 1 = {{∅}} ∪ {∅} = {{∅}, ∅} = {1, 0} 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.
ndriscoll 2y ago
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?
- immibis 2y ago
  Nobody else is seeing how it is not convoluted. 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. It seems like you might be suffering from fuckarounditis: https://news.ycombinator.com/item?id=43466252 https://news.ycombinator.com/item?id=43466252

immibis 2y ago

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.

ndriscoll 2y ago
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). I don't know what strategies they're using, but mathlib in Lean has formalizations for measure theory for example: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/MeasureTheory/Measure/MeasureSpace.lean https://github.com/leanprover-community/mathlib4/blob/master... 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.