4 ms·

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

by krapht 2y ago

tossandthrow 2y ago
Well, a proven proposition would compile to a unit value. Files with only proofs would Compile to something akin to main = nil
- ndriscoll 2y 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. :-) [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?

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

by krapht 2y ago

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

tossandthrow 2y ago

Well, a proven proposition would compile to a unit value. Files with only proofs would Compile to something akin to main = nil

ndriscoll 2y 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. :-) [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?