10 ms·

In my opinion it's a tragedy there are so few resources in using "Propositions as Types"/"Curry–Howard correspondence"[0] in didactics in tandem with teaching f

In my opinion it's a tragedy there are so few resources in using "Propositions as Types"/"Curry–Howard correspondence"[0] in didactics in tandem with teaching functional programming to teach structured proof-writing. Many students do not feel comfortable with proof-writing and cannot dispatch/discharge implications or quantifications correctly when writing proofs and I believe that a structured approach using the Curry-Howard correspondence could help. [0]: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...

mietek 1y ago
One of the best modern resources is "Programming language foundations in Agda", co-authored by Wen Kokke and the same Philip Wadler, and used for teaching at multiple universities. https://plfa.github.io/ https://plfa.github.io/
jerf 1y ago
While I am first in line to say that programming is math whether you like it or not, it is certainly the case that few programmers are using that sort of math in their heads when they are programming. I suspect that if, oh, about 60-70 years of trying to change that has not had any headway that there is little reason to suspect that's going to change in the next 30. But you can sort of backdoor the idea with something like this: https://jerf.org/iri/post/2025/fp_lessons_types_as_assertions/ https://jerf.org/iri/post/2025/fp_lessons_types_as_assertion... I won't claim it is exactly the same, but it is certainly similar. Tell a programmer, "Hey, you can build a type that carries certain guarantees with it, so that the rest of the program doesn't need to be constantly validating it", a problem any 5+ year dev ought to be very familiar with, and I think you make more progress in the direction of this notion than a paper full of logic diagrams in a notation even most computer scientist undergrads will never encounter. (I'm not even certain if I directly encountered that in my Master's degree. It's been a while. I think I did, but I think it was only one class, and not a huge part of it. I'm not sure because I know I did more with it on my own, so I can't remember if I was formally taught it or if I picked it up entirely myself.)
- skybrian 1y ago
  While I generally agree with defining new types to assert that validation has been done, I think your blog post could have explained more about what kinds of validation are practical to do. For example: > Address that represents a “street address” that has been validated by your street address to exist What does it even mean to verify that a street address exists? Verifying real-world relationships is complex and error-prone. I’m reminded of the genre of articles starting with “Falsehoods programmers believe about names” [1]. In practice, the rules that can be enforced are often imposed by the system itself. It simply doesn’t accept data that isn’t in correct format or isn’t consistent with other data it already has. And we need to be cautious about what harm might be caused by these rejections. Having the validation logic in one place will certainly help when fixing mistakes, but then what do you do about data that’s already been accepted, but is no longer “valid?” This sort of thing makes long-running systems like databases hard to maintain. [1] https://www.kalzumeus.com/2010/06/17/falsehoods-programmers-believe-about-names/ https://www.kalzumeus.com/2010/06/17/falsehoods-programmers-...
  - fmbb 1y ago
    Far too many programmers forget that time passes.
    - daxfohl 1y ago
      Yeah, the issue is that proofs are harder than people think, even for trivial things (try a few easy leetcode problems in Lean with a proof of correctness), and less useful than people think, especially when you get past low level algorithms and into domain logic (your point exactly). They also don't serialize well, so a database or API call with a "proof" field would be susceptible to fudging, or the definition could change between deployments. They're also easy to make incompatible: one library requires bounds proofs for signed ints, but your app uses unsigned ints, so you have to either rewrite your app or rewrite the library, or cast, in which your type system has to handle like a "checked exception" and propagate that possibility throughout your whole type domain and app logic. I'm pretty convinced there's a good reason that while "propositions as types" is cool in theory, it's unlikely we'll ever see it catch on in practice.
mrkeen 1y ago
This may not go over as well as you'd think. I took Haskell in the same uni course with FSAs, Turing machines, Lambda calculus, natural deduction, Hoare logic and structural induction. So I was exposed to the "base case & step case" of structural induction at the same time as learning about it in Haskell. And for whatever reason it didn't leave a good impression. Implementing it formally was harder and more error-prone than shooting from the hip in an IDE. What was the point!? Now I smash out Haskell code daily as the quickest way to end up with little binaries that just-work-if-they-compile. It took me a while to realise that the upside of all this formality/mathiness is that other people did the proofs so that you don't need to. I get to take for granted that a boolean is true or false (and not some brilliant third value!) and that (map f . map g) is (map (f . g)).
- AnimalMuppet 1y ago
  “A man is rich in proportion to the number of things which he can afford to let alone.” ― Henry David Thoreau, Walden or, Life in the Woods If I have to do the proof, then as you say, it's probably harder and (in many cases) more error prone than if I didn't use a proof. If the language can do it for me, and I get the lack of errors without having to do the work (and without the chance of me making the mistakes)? Yeah, now we're talking. (Yes, I am aware that I still have to design the types to fit what the program is doing.) If a tool introduces complexity, it has to make up for it by eliminating at least that much complexity somewhere else. If it doesn't, the tool isn't worth using.
- edef 1y ago
  > I get to take for granted that a boolean is true or false (and not some brilliant third value!) [True, False, undefined] :: [Bool]
  - immibis 1y ago
    The traditional third value is actually FileNotFound: https://thedailywtf.com/articles/what_is_truth_0x3f_ https://thedailywtf.com/articles/what_is_truth_0x3f_ but in Haskell, yes, it's undefined. Which isn't a real value! For example, infinite loops are undefined. Theorists like to call it a value of every type, but in practical terms, it's more like a computation that never produces a value. The builtin "undefined" can be written as an infinite loop ("undefined = undefined") and many other pure infinite loops can also act as undefined values. The runtime is able to catch some and crash instead of hanging, but not others.
talkingtab 1y ago
The connection to intuitionism (see https://en.wikipedia.org/wiki/Intuitionism https://en.wikipedia.org/wiki/Intuitionism) gives this kind of thinking much broader appeal and application. It seems to me we live in a time so dominated by analytical thinking that we completely ignore other useful and effective modes.
- johnnyjeans 1y ago
  Intuitionism in this context just means the proofs have to be constructive. (no proof-by-contradiction, or other half-assed academic hacks)
  - AnimalMuppet 1y ago
    Why do you say that proof-by-contradiction is a "half-assed academic hack"? In particular, if someone isn't already an intuitionist or constructivist, what reason can you give that would be valid in their frame of reference?
    - johnnyjeans 1y ago
      Because they explain nothing and aren't useful for building new insights. It's not a direct verification of the existence or lack-of-existence of a thing with given properties. It relies on rules lawyering in a very specific logic to say something with basically no substance. Allowing it causes more problems for automated proofs than they solve, so long as your domain only deals with finites (which all real-world domains do exclusively.) They're also generally much easier to create than constructive proofs, which makes them a convenient go-to for lazy academics.
      - ndriscoll 1y ago
        Proof by contradiction is fine for lack-of-existence (indeed, ¬P is defined in type theory as P -> false). I think also if I got my types right, you can do def eliminateTripleNot(f: ¬¬¬P): ¬P = {p: P => f({g: ¬P => g(p)})} For a constructive proof of ¬¬¬P => ¬P? So it's really just ¬¬P => P that causes trouble. It's not clear to me though whether LEM is actually okay in the "fast and loose reasoning is morally correct" sense (i.e. if it's okay as long as you don't cheat and do something like use a non-terminating loop or exception to make your ¬¬P) though? Are there cases where you didn't "obviously" cheat where it's "wrong" to use it? In some sense, I see ¬¬P => P as a "cast" from an opaque function type to specifically be a closure {f => f(p)} for some p: P.
ndriscoll 1y ago
I've been thinking the same thing and mentioned it the other day[0]. When I was learning proofs, I saw people struggle with the idea of needing to choose a "generic" element to prove a forall statement, for example. I suspect it might make more sense if you taught things in terms of needing to write a function x=>P(x). I think in some cases, thinking in terms of programming might also change how we think about structuring things. e.g. define a data structure for a "point with error tolerance" (x, epsilon), then continuity says given a toleranced-point y* at f(x), I can find a toleranced-point x* at x such that f(x*) is "compatible" (equal at the base point and within tolerance) with y*. This factoring lets you avoid shocking new students with quantifier soup. Likewise the chain rule is just straightforward composition when you define a "derivative at a point" data structure Df((x,m))=(f(x), m*f'(x)). This is not at all new, but I suppose it's currently a lot to ask students to learn proof mechanics while also unwinding multiple layers of definitions for abstractions. Computers can help do the unwinding (or lifting) automatically to make it easier to make small "quality of life" definitions that otherwise wouldn't be hugely useful when pen-and-paper-proofs would always be unwinding them anyway. Basically, math education could look a lot like software engineering education. The concerns and solution patterns are basically the same. e.g. typeclasses are pretty much how mathematics does polymorphism, and are probably usually the right way to do it in programming too. [0] https://news.ycombinator.com/item?id=43875101 https://news.ycombinator.com/item?id=43875101
- immibis 1y ago
  I don't think the C-H correspondence is necessary for this. It would be a useful way to think even if the C-H correspondence were false.
js8 1y ago
I would recommend https://lean-lang.org/theorem_proving_in_lean4/ https://lean-lang.org/theorem_proving_in_lean4/, especially the first few chapters, if you're willing to use Lean.
ngruhn 1y ago
100% agree. I did not understand induction until I learned Coq. It really shows how mechanical proving can be.
boxfire 1y ago
There's a book that's explicitly about this, "Program = Proof", and though it's not beginner and needs maybe a light version for earlier learners, is an excellent example.

mietek 1y ago

One of the best modern resources is "Programming language foundations in Agda", co-authored by Wen Kokke and the same Philip Wadler, and used for teaching at multiple universities. https://plfa.github.io/ https://plfa.github.io/

jerf 1y ago

While I am first in line to say that programming is math whether you like it or not, it is certainly the case that few programmers are using that sort of math in their heads when they are programming. I suspect that if, oh, about 60-70 years of trying to change that has not had any headway that there is little reason to suspect that's going to change in the next 30. But you can sort of backdoor the idea with something like this: https://jerf.org/iri/post/2025/fp_lessons_types_as_assertions/ https://jerf.org/iri/post/2025/fp_lessons_types_as_assertion... I won't claim it is exactly the same, but it is certainly similar. Tell a programmer, "Hey, you can build a type that carries certain guarantees with it, so that the rest of the program doesn't need to be constantly validating it", a problem any 5+ year dev ought to be very familiar with, and I think you make more progress in the direction of this notion than a paper full of logic diagrams in a notation even most computer scientist undergrads will never encounter. (I'm not even certain if I directly encountered that in my Master's degree. It's been a while. I think I did, but I think it was only one class, and not a huge part of it. I'm not sure because I know I did more with it on my own, so I can't remember if I was formally taught it or if I picked it up entirely myself.)

skybrian 1y ago
While I generally agree with defining new types to assert that validation has been done, I think your blog post could have explained more about what kinds of validation are practical to do. For example: > Address that represents a “street address” that has been validated by your street address to exist What does it even mean to verify that a street address exists? Verifying real-world relationships is complex and error-prone. I’m reminded of the genre of articles starting with “Falsehoods programmers believe about names” [1]. In practice, the rules that can be enforced are often imposed by the system itself. It simply doesn’t accept data that isn’t in correct format or isn’t consistent with other data it already has. And we need to be cautious about what harm might be caused by these rejections. Having the validation logic in one place will certainly help when fixing mistakes, but then what do you do about data that’s already been accepted, but is no longer “valid?” This sort of thing makes long-running systems like databases hard to maintain. [1] https://www.kalzumeus.com/2010/06/17/falsehoods-programmers-believe-about-names/ https://www.kalzumeus.com/2010/06/17/falsehoods-programmers-...
- fmbb 1y ago
  Far too many programmers forget that time passes.
  - daxfohl 1y ago
    Yeah, the issue is that proofs are harder than people think, even for trivial things (try a few easy leetcode problems in Lean with a proof of correctness), and less useful than people think, especially when you get past low level algorithms and into domain logic (your point exactly). They also don't serialize well, so a database or API call with a "proof" field would be susceptible to fudging, or the definition could change between deployments. They're also easy to make incompatible: one library requires bounds proofs for signed ints, but your app uses unsigned ints, so you have to either rewrite your app or rewrite the library, or cast, in which your type system has to handle like a "checked exception" and propagate that possibility throughout your whole type domain and app logic. I'm pretty convinced there's a good reason that while "propositions as types" is cool in theory, it's unlikely we'll ever see it catch on in practice.

mrkeen 1y ago

This may not go over as well as you'd think. I took Haskell in the same uni course with FSAs, Turing machines, Lambda calculus, natural deduction, Hoare logic and structural induction. So I was exposed to the "base case & step case" of structural induction at the same time as learning about it in Haskell. And for whatever reason it didn't leave a good impression. Implementing it formally was harder and more error-prone than shooting from the hip in an IDE. What was the point!? Now I smash out Haskell code daily as the quickest way to end up with little binaries that just-work-if-they-compile. It took me a while to realise that the upside of all this formality/mathiness is that other people did the proofs so that you don't need to. I get to take for granted that a boolean is true or false (and not some brilliant third value!) and that (map f . map g) is (map (f . g)).

AnimalMuppet 1y ago
“A man is rich in proportion to the number of things which he can afford to let alone.” ― Henry David Thoreau, Walden or, Life in the Woods If I have to do the proof, then as you say, it's probably harder and (in many cases) more error prone than if I didn't use a proof. If the language can do it for me, and I get the lack of errors without having to do the work (and without the chance of me making the mistakes)? Yeah, now we're talking. (Yes, I am aware that I still have to design the types to fit what the program is doing.) If a tool introduces complexity, it has to make up for it by eliminating at least that much complexity somewhere else. If it doesn't, the tool isn't worth using.
edef 1y ago
> I get to take for granted that a boolean is true or false (and not some brilliant third value!) [True, False, undefined] :: [Bool]
- immibis 1y ago
  The traditional third value is actually FileNotFound: https://thedailywtf.com/articles/what_is_truth_0x3f_ https://thedailywtf.com/articles/what_is_truth_0x3f_ but in Haskell, yes, it's undefined. Which isn't a real value! For example, infinite loops are undefined. Theorists like to call it a value of every type, but in practical terms, it's more like a computation that never produces a value. The builtin "undefined" can be written as an infinite loop ("undefined = undefined") and many other pure infinite loops can also act as undefined values. The runtime is able to catch some and crash instead of hanging, but not others.

talkingtab 1y ago

The connection to intuitionism (see https://en.wikipedia.org/wiki/Intuitionism https://en.wikipedia.org/wiki/Intuitionism) gives this kind of thinking much broader appeal and application. It seems to me we live in a time so dominated by analytical thinking that we completely ignore other useful and effective modes.

johnnyjeans 1y ago
Intuitionism in this context just means the proofs have to be constructive. (no proof-by-contradiction, or other half-assed academic hacks)
- AnimalMuppet 1y ago
  Why do you say that proof-by-contradiction is a "half-assed academic hack"? In particular, if someone isn't already an intuitionist or constructivist, what reason can you give that would be valid in their frame of reference?
  - johnnyjeans 1y ago
    Because they explain nothing and aren't useful for building new insights. It's not a direct verification of the existence or lack-of-existence of a thing with given properties. It relies on rules lawyering in a very specific logic to say something with basically no substance. Allowing it causes more problems for automated proofs than they solve, so long as your domain only deals with finites (which all real-world domains do exclusively.) They're also generally much easier to create than constructive proofs, which makes them a convenient go-to for lazy academics.
    - ndriscoll 1y ago
      Proof by contradiction is fine for lack-of-existence (indeed, ¬P is defined in type theory as P -> false). I think also if I got my types right, you can do def eliminateTripleNot(f: ¬¬¬P): ¬P = {p: P => f({g: ¬P => g(p)})} For a constructive proof of ¬¬¬P => ¬P? So it's really just ¬¬P => P that causes trouble. It's not clear to me though whether LEM is actually okay in the "fast and loose reasoning is morally correct" sense (i.e. if it's okay as long as you don't cheat and do something like use a non-terminating loop or exception to make your ¬¬P) though? Are there cases where you didn't "obviously" cheat where it's "wrong" to use it? In some sense, I see ¬¬P => P as a "cast" from an opaque function type to specifically be a closure {f => f(p)} for some p: P.

ndriscoll 1y ago

I've been thinking the same thing and mentioned it the other day[0]. When I was learning proofs, I saw people struggle with the idea of needing to choose a "generic" element to prove a forall statement, for example. I suspect it might make more sense if you taught things in terms of needing to write a function x=>P(x). I think in some cases, thinking in terms of programming might also change how we think about structuring things. e.g. define a data structure for a "point with error tolerance" (x, epsilon), then continuity says given a toleranced-point y* at f(x), I can find a toleranced-point x* at x such that f(x*) is "compatible" (equal at the base point and within tolerance) with y*. This factoring lets you avoid shocking new students with quantifier soup. Likewise the chain rule is just straightforward composition when you define a "derivative at a point" data structure Df((x,m))=(f(x), m*f'(x)). This is not at all new, but I suppose it's currently a lot to ask students to learn proof mechanics while also unwinding multiple layers of definitions for abstractions. Computers can help do the unwinding (or lifting) automatically to make it easier to make small "quality of life" definitions that otherwise wouldn't be hugely useful when pen-and-paper-proofs would always be unwinding them anyway. Basically, math education could look a lot like software engineering education. The concerns and solution patterns are basically the same. e.g. typeclasses are pretty much how mathematics does polymorphism, and are probably usually the right way to do it in programming too. [0] https://news.ycombinator.com/item?id=43875101 https://news.ycombinator.com/item?id=43875101

immibis 1y ago
I don't think the C-H correspondence is necessary for this. It would be a useful way to think even if the C-H correspondence were false.

js8 1y ago

I would recommend https://lean-lang.org/theorem_proving_in_lean4/ https://lean-lang.org/theorem_proving_in_lean4/, especially the first few chapters, if you're willing to use Lean.

ngruhn 1y ago

100% agree. I did not understand induction until I learned Coq. It really shows how mechanical proving can be.

boxfire 1y ago

There's a book that's explicitly about this, "Program = Proof", and though it's not beginner and needs maybe a light version for earlier learners, is an excellent example.