4 ms·

I sympathize with you but I always follow develooments in this space because the potential upside is so awesome. Excellent mathematicians are using theorem prov

I sympathize with you but I always follow develooments in this space because the potential upside is so awesome. Excellent mathematicians are using theorem provers to check their logic, and such a system brought to say the compilation of a realtime OS, or a distributed transactional system could provide a real safety net for preventing logical errors introduced by new code.

bayesian_horse 7y ago
I do get that point, but it seems to me that only very advanced programmers are able to work with such languages and systems. The advantage of a "safety net" has a big fight on his hands against the big disadvantage of "who's going to maintain this shit when that rock-star theorem guy is gone?". Or the theorem guys are very expensive in the first place, so it's cheaper or easier to hire multiple people who have to use unit tests like everybody else.
- wwarner 7y ago
  I don't see it this way at all. It's more like using the compiler to write good unit tests. That's the hope anyway.
  - pezo1919 7y ago
    I am dont know so much about that field but I "feel" the same. It would be nice if someone who knows that stuff could reply here if this intuition is right or not. Eventually when we reason about our code "as standard" non-math programmers we are doing math & logic & proofs in our minds aren't we? And we capture the edge cases in forms of tests and hope for the best if we thought about and enumerated all the necessary ones. So eventually if - a language but more importantly - an ecosystem like that will get leverage, every existing ecosystem can slowly fade into that and develop further in this path. At the end (almost all) programmers are going to write proofs, because this is what works in scale. Please correct me if I am wrong!
- UK-Al05 7y ago
  "The advantage of a "safety net" has a big fight on his hands against the big disadvantage of "who's going to maintain this shit when that rock-star theorem guy is gone?". Or the theorem guys are very expensive in the first place, so it's cheaper or easier to hire multiple people who have to use unit tests like everybody else. " - That's because we're an immature field. Something like this will eventually have to come out in order to fix the crisis in software. We're currently the early explorers of a field, mostly composed practices & tips and tricks that we think help but can't be sure. We're like barber-surgeons before it turned into a true profession.
- heavenlyblue 7y ago
  Well, look who’s afraid for their job to be taken by someone else. I believe we have plenty of examples today of “we can’t fire this employee because a few years ago we made a mistake of that hire and now they are the only ones who know how that pile of shit works”. At least with theorem provers the transparent knowledge of the broken systems can be formalized.
- chongli 7y ago
  "who's going to maintain this shit when that rock-star theorem guy is gone?" At this point, I think the rockstar theorem guy would not be working on some proprietary business logic that needs to be maintained wholly in-house. He'd be in charge of more critical infrastructure in widespread use. Kernels, SSL libraries, optimizing compilers; that sort of thing. As for who should hire him? I'd hope one of the big tech companies would want a project like this.
- nesadi 7y ago
  > I do get that point, but it seems to me that only very advanced programmers are able to work with such languages and systems. That's because the field is still in an exploratory and research phase. Unless you're in an industry where correctness is the most important criteria or involved in research into this stuff, your average programmer isn't going to be using any of this. It's still too early, but that doesn't mean it's a waste of time.
  - bayesian_horse 7y ago
    I'm not saying it's a waste of time, I want to understand why it's not.
- hwayne 7y ago
  For most of the cases where formally verifying _code_ is important, "unit tests" aren't enough. If the person who writes the proofs leaves, you hire someone else to write proofs. Otherwise you don't have a business model. For most of the cases where formally verifying _designs_ is important (most of the industry), formal specification languages are 1) not actually that hard to learn, and 2) exist distinct from the code, so you can throw them all out if you really need to and go back to flying blind.

bayesian_horse 7y ago

I do get that point, but it seems to me that only very advanced programmers are able to work with such languages and systems. The advantage of a "safety net" has a big fight on his hands against the big disadvantage of "who's going to maintain this shit when that rock-star theorem guy is gone?". Or the theorem guys are very expensive in the first place, so it's cheaper or easier to hire multiple people who have to use unit tests like everybody else.

wwarner 7y ago
I don't see it this way at all. It's more like using the compiler to write good unit tests. That's the hope anyway.
- pezo1919 7y ago
  I am dont know so much about that field but I "feel" the same. It would be nice if someone who knows that stuff could reply here if this intuition is right or not. Eventually when we reason about our code "as standard" non-math programmers we are doing math & logic & proofs in our minds aren't we? And we capture the edge cases in forms of tests and hope for the best if we thought about and enumerated all the necessary ones. So eventually if - a language but more importantly - an ecosystem like that will get leverage, every existing ecosystem can slowly fade into that and develop further in this path. At the end (almost all) programmers are going to write proofs, because this is what works in scale. Please correct me if I am wrong!
UK-Al05 7y ago
"The advantage of a "safety net" has a big fight on his hands against the big disadvantage of "who's going to maintain this shit when that rock-star theorem guy is gone?". Or the theorem guys are very expensive in the first place, so it's cheaper or easier to hire multiple people who have to use unit tests like everybody else. " - That's because we're an immature field. Something like this will eventually have to come out in order to fix the crisis in software. We're currently the early explorers of a field, mostly composed practices & tips and tricks that we think help but can't be sure. We're like barber-surgeons before it turned into a true profession.
heavenlyblue 7y ago
Well, look who’s afraid for their job to be taken by someone else. I believe we have plenty of examples today of “we can’t fire this employee because a few years ago we made a mistake of that hire and now they are the only ones who know how that pile of shit works”. At least with theorem provers the transparent knowledge of the broken systems can be formalized.
chongli 7y ago
"who's going to maintain this shit when that rock-star theorem guy is gone?" At this point, I think the rockstar theorem guy would not be working on some proprietary business logic that needs to be maintained wholly in-house. He'd be in charge of more critical infrastructure in widespread use. Kernels, SSL libraries, optimizing compilers; that sort of thing. As for who should hire him? I'd hope one of the big tech companies would want a project like this.
nesadi 7y ago
> I do get that point, but it seems to me that only very advanced programmers are able to work with such languages and systems. That's because the field is still in an exploratory and research phase. Unless you're in an industry where correctness is the most important criteria or involved in research into this stuff, your average programmer isn't going to be using any of this. It's still too early, but that doesn't mean it's a waste of time.
- bayesian_horse 7y ago
  I'm not saying it's a waste of time, I want to understand why it's not.
hwayne 7y ago
For most of the cases where formally verifying _code_ is important, "unit tests" aren't enough. If the person who writes the proofs leaves, you hire someone else to write proofs. Otherwise you don't have a business model. For most of the cases where formally verifying _designs_ is important (most of the industry), formal specification languages are 1) not actually that hard to learn, and 2) exist distinct from the code, so you can throw them all out if you really need to and go back to flying blind.