3 ms·

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 i

by 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.
    - Tainnor 1y ago
      > try a few easy leetcode problems in Lean with a proof of correctness This might actually be harder than, say, proving some undergraduate math theorems because reasoning about mutable state (especially when you want it to be performant) is tricky. I might guess that it could be easier to use a model checker such as TLA+ for that (although that can only verify algorithm descriptions and not implementations) because they seem to be more built with these things in my mind, but I lack enough experience with it to be certain.
    - mietek 1y ago
      > …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… Nonsense. Proving things about low-level algorithms that are full of complicated behaviors involving shared mutable state is often more difficult than proving things about high-level domain logic; regardless, people still do it, and if you use any modern CPU, especially from the ARM family, you benefit from their work. A proof serializes just as well as any other kind of program — after all, the first step in checking a proof involves deserializing the proof, or in other words, reading and parsing its source code. As for “fudging”; proofs are guaranteed to be correct up to the correctness of the proof checker, which can be used to recheck the proof at any time. For more information, see Geuvers (2009) “Proof assistants: History, ideas and future”. https://sci-hub.st/https://link.springer.com/article/10.1007/s12046-009-0001-5 https://sci-hub.st/https://link.springer.com/article/10.1007...
immibis 1y ago
This has nothing to do with C-H though.
- jerf 1y ago
  It isn't exactly the same. I believe I said that up front. But it provides a bridge. Both things have "You can assert Property X about all things of type Y" built into them. Trying to jump people straight to C-H without giving any hint whatsoever of why this may be useful in any real code... well, that's a non-trivial percentage of why this approach has completely failed to capture any significant mindspace, though I leave it as an exercise to the reader to determine the exact percentage in their minds.
  - immibis 1y ago
    C-H has nothing to do with "property X is true about all things of type Y". It says "if you can find an object of type Y, you can prove global property Z." For example, the property corresponding to the type "(Either a a) -> a" is "(A or A) implies A" which doesn't tell you any properties of actual objects of the type "(Either a a) -> a" The property corresponding to the type "(Either a b) -> a" is "(A or B) implies A" which is not provable, so you can't find any object of this type.

by jerf 1y ago

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.
  - Tainnor 1y ago
    > try a few easy leetcode problems in Lean with a proof of correctness This might actually be harder than, say, proving some undergraduate math theorems because reasoning about mutable state (especially when you want it to be performant) is tricky. I might guess that it could be easier to use a model checker such as TLA+ for that (although that can only verify algorithm descriptions and not implementations) because they seem to be more built with these things in my mind, but I lack enough experience with it to be certain.
  - mietek 1y ago
    > …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… Nonsense. Proving things about low-level algorithms that are full of complicated behaviors involving shared mutable state is often more difficult than proving things about high-level domain logic; regardless, people still do it, and if you use any modern CPU, especially from the ARM family, you benefit from their work. A proof serializes just as well as any other kind of program — after all, the first step in checking a proof involves deserializing the proof, or in other words, reading and parsing its source code. As for “fudging”; proofs are guaranteed to be correct up to the correctness of the proof checker, which can be used to recheck the proof at any time. For more information, see Geuvers (2009) “Proof assistants: History, ideas and future”. https://sci-hub.st/https://link.springer.com/article/10.1007/s12046-009-0001-5 https://sci-hub.st/https://link.springer.com/article/10.1007...

immibis 1y ago

This has nothing to do with C-H though.

jerf 1y ago
It isn't exactly the same. I believe I said that up front. But it provides a bridge. Both things have "You can assert Property X about all things of type Y" built into them. Trying to jump people straight to C-H without giving any hint whatsoever of why this may be useful in any real code... well, that's a non-trivial percentage of why this approach has completely failed to capture any significant mindspace, though I leave it as an exercise to the reader to determine the exact percentage in their minds.
- immibis 1y ago
  C-H has nothing to do with "property X is true about all things of type Y". It says "if you can find an object of type Y, you can prove global property Z." For example, the property corresponding to the type "(Either a a) -> a" is "(A or A) implies A" which doesn't tell you any properties of actual objects of the type "(Either a a) -> a" The property corresponding to the type "(Either a b) -> a" is "(A or B) implies A" which is not provable, so you can't find any object of this type.