8 ms·

Yep. If you have written production grade software at real companies, you know that the moment you make that new commit (even if 1 liner change), you are now re

Yep. If you have written production grade software at real companies, you know that the moment you make that new commit (even if 1 liner change), you are now ready to accept that it could break something. yes you can do your unit tests, integration test, User Acceptance Tests and what not. But every code change = new possible bug that you may not be able to catch until it occurs to a customer. Whenever I hear a developer say "I never ship buggy code", I am always cautious to dig in more and understand what they mean by that.

Gare 3y ago
How about a formal proof? :) I jest, but that should be the gold standard for anything life-critical and good to have for mission-critical software. Alas, we're not there yet.
- underlipton 3y ago
  Oh, boy, I get to post this again: https://www.fastcompany.com/28121/they-write-right-stuff https://www.fastcompany.com/28121/they-write-right-stuff
- akhosravian 3y ago
  I’m not a CS academic or a mathematician, but don’t Godel’s incompleteness theorems preclude a formal proof of correctness?
  - topaz0 3y ago
    No. There are plenty of things that can be proved, it's just that there exist true statements that cannot be proved.
    - kevindamm 3y ago
      That's closer, but still not quite right. There are well-formed statements that can be proved but which assert that its godelized value represents a non-provable theorem. Therefore, you must accept that it and its contradiction are both provable (leading to an inconsistent system), or not accept it and now there are provable theorems that cannot be expressed in the system. Furthermore, that this can be constructed from anything with base arithmetic and induction over first-order logic (Gödel's original paper included how broadly it could be applied to basically every logical system).
      - kevindamm 3y ago
        The important thing to note is that it doesn't have anything to do with truth or truth-values of propositions. It breaks the fundamental operation of the provability of a statement. And, since many proofs are done by assuming a statement's inverse and trying to prove a contradiction, having a known contradiction in the set of provable statements can effectively allow any statement to be proven. Keeping the contradiction is not actually an option.
  - Veserv 3y ago
    No. It merely prevents you from confirming every arbitrarily complex proof. Incompleteness is more like: I give you a convoluted mess of spaghetti code and claim it computes prime numbers and I demand you try to prove me wrong.
  - Verdex 3y ago
    No. Godel means that we can't have an algorithmic box that we put a program into and out comes a true/false statement of halting. Nothing is stopping you from writing the proof manually for each program that you want to prove properties for. ALSO, you can write sub-turing complete programs. Those are allowed to have automated halting proofs (see idris et al).
    - kevindamm 3y ago
      What you're talking about is actually the Church-Turing thesis and the halting problem. While, yes, computability and provability are very closely related, it's important to get attribution correct. More details on what Gödel's Incompleteness Theorem really said are in a sibling comment so I won't repeat them here.
      - Verdex 3y ago
        > it's important to get attribution correct. Really? Says who? Or perhaps you'll prove it from first principles. Although if turns out to be difficult, that's okay. Somebody mentioned something about systems being either complete or consistent but never both. Some things can be true but not proveably so. Can't quite remember who it was though.
        kevindamm 3y ago
        Fair enough, I was being annoyingly pedantic. [I believe that] it's important to get attribution correct.
        Verdex 3y ago
        To be fair, annoyingly pedantic is the best kind of pedantic. - Futurama (kind of)
        kevindamm 3y ago
        sounds technically correct Gödel's really was a rather unique mind, and the story of his death is kind of sad.. but I wonder if it takes such a severe kind of paranoia to look for how math can break itself, especially during that time when all the greatest mathematicians were in pursuit of formalizing a complete and consistent mathematics.
- cochne 3y ago
  I never really got how proofs are supposed to solve this issue. I think that would just move the bugs from the code into the proof definition. Your code may do what the proof says, but how do you know what the proof says is what you actually want to happen?
  - dgacmu 3y ago
    Not really. Imagine the proof says: "in this protocol, when there are more than 0 participants, exactly one participant holds the lock at any time" It might be wrong, but it's pretty easy to inspect and has a much higher chance of being right than your code does. You then use proof refinement to eventually link this very high level statement down to the code implementing it. That's the vision, at least, and it's sometimes possible to achieve it. See, for example, Ironfleet: https://www.microsoft.com/en-us/research/publication/ironfleet-proving-practical-distributed-systems-correct/ https://www.microsoft.com/en-us/research/publication/ironfle...
  - MaxBarraclough 3y ago
    A formal spec isn't just ordinary source-code by another name, it's at a quite different level of abstraction, and (hopefully) it will be proven that its invariants always hold. (This is a separate step from proving that the model corresponds to the ultimate deliverable of the formal development process, be that source-code or binary.) Bugs in the formal spec aren't impossible, but use of formal methods doesn't prevent you from doing acceptance testing as well. In practice, there's a whole methodology at work, not just blind trust in the formal spec. Software developed using formal methods is generally assured to be free of runtime errors at the level of the target language (divide-by-zero, dereferencing NULL, out-of-bounds array access, etc). This is a pretty significant advantage, and applies even if there's a bug in the spec. Disclaimer: I'm very much not an expert. Interesting reading: * An interesting case-study, albeit from a non-impartial source [PDF] https://www.adacore.com/uploads/downloads/Tokeneer_Report.pdf https://www.adacore.com/uploads/downloads/Tokeneer_Report.pd... * An introduction to the Event-B formal modelling method [PDF] https://www.southampton.ac.uk/~tsh2n14/publications/chapters/eventb-dbook13.pdf https://www.southampton.ac.uk/~tsh2n14/publications/chapters...
- roenxi 3y ago
  As always, the branding of formal methods sucks. As other commentators point out, it isn't technically possible to provide a formal proof that software is correct. And that is fine, because formal software methods don't do that. But right from the outset the approach is doomed to fail because its proponents write like they don't know what they are talking about and think they can write bug-free software. It really should be "write software with a formal spec". Once people start talking about "proof" in practice it sounds dishonest. It isn't possible to prove software and the focus really needs to be on the spec.
  - hnfong 3y ago
    > It really should be "write software with a formal spec". The code is already a formal spec. Unless there are bugs in the language/compiler/interpreter, what the code is essentially formally well defined. As programming languages get better at enabling programmers to communicate intention as opposed to being a way to generate computer instructions, there's really no need for a separate "spec". Any so called "spec" that is not a programming language is likely not "formal" in the sense that the behavior is unambiguously well defined. Of course, you might be able to write the "spec" using a formal language that cannot be transformed into machine code, but assuming that the "spec" is actually well defined, then it's just that "compiling" the spec into machine code is too expensive in some way (eg. nobody has written a compiler, it's too computationally hard to deduce the actual intention even though it's well defined, etc.). But in essence it is still a "programming language", just one without a compiler/interpreter.
- AnimalMuppet 3y ago
  Formal proof of what? That it has no bugs? Ha! You can formally prove that it doesn't have certain kinds of bugs. And that's good! But it also is an enormous amount of work. And so, even for life-critical software, the vast majority is not formally proven, because we want more software than we can afford to formally prove.
  - Verdex 3y ago
    This is an interesting point that I think a lot of programming can miss. Proving that the program has no bugs is akin to proving that the program won't make you feel sad. Like ... I'm not sure we have the math. One of the more important jobs of the software engineer is to look deep into your customer's dreams and determine how those dreams will ultimately make your customer sad unless there's some sort of intervention before you finish the implementation.
  - makapuf 3y ago
    Yeah, if you can have a formally proven compiler from slides, poorly written user stories and clarification phone calls to x86_64 binary then alright.
  - BoiledCabbage 3y ago
    Exactly, it's fundamentally impossible. Formal proofs can help with parts of the process, but it can guarantee no bugs in the product. These are the steps of software, and their transitions. It's fundamentally a game of telephone with errors at each step along the way. What actually would solve the customer's problem -> What the customer thinks they want -> What they communicate that they want -> What the requirements collector hears -> What the requirements collector documents -> How the implementor interprets the requirements -> What the implementor designs/plans -> What the implementor implements. Formal proofs can help with the last 3 steps. But again that's assuming the implementor can formalize every requirement they interpreted. And that's impossible as well, there will always be implicit assumptions about the running environment, performance, scale, the behavior of dependent processes/APIs. It helps with a small set of possible problems. If those problems are mission-critical then absolutely tackle them, but there will never be a situation where it can help with the first 5 steps of the problem, or with the implicit items in the 6th step above.
- bluGill 3y ago
  Even formally proved code can have bugs. If your requirement is wrong is the obvious thing. I don't work with formal proofs (I want to, I just don't know how), but I'm given to understand they have other real world limits that make them sometimes have other bugs.
- radicalcentrist 3y ago
  To quote Donald Knuth, "Beware of bugs in the above code; I have only proved it correct, not tried it."
- kaba0 3y ago
  Well, if your product is on the hello world complexity, you might make it bug-free by just yourself simply through chance. Formal proving doesn’t really scale much further, definitely not to “enterprise” product scale.
wvenable 3y ago
It's always amazing when I get a bug report from a product that's been running bug free in production for years with minimal changes but some user did some combination of things that had never been done and it blows up. Usually it's something extremely simple to fix too.
- codegeek 3y ago
  This happens a lot more than one may think especially with products that have lot of features. Some features are used sparingly and the moment a customer uses that feature a bit more in depth, boom. Something is broken.
  - tylerchurch 3y ago
    > especially with products that have lot of features No kidding. I'm 2 or 3 years into working on a SaaS app started in ~2013 and I still get bug reports from users that make me say "what!? we have that feature!?"

Gare 3y ago

How about a formal proof? :) I jest, but that should be the gold standard for anything life-critical and good to have for mission-critical software. Alas, we're not there yet.

underlipton 3y ago
Oh, boy, I get to post this again: https://www.fastcompany.com/28121/they-write-right-stuff https://www.fastcompany.com/28121/they-write-right-stuff
akhosravian 3y ago
I’m not a CS academic or a mathematician, but don’t Godel’s incompleteness theorems preclude a formal proof of correctness?
- topaz0 3y ago
  No. There are plenty of things that can be proved, it's just that there exist true statements that cannot be proved.
  - kevindamm 3y ago
    That's closer, but still not quite right. There are well-formed statements that can be proved but which assert that its godelized value represents a non-provable theorem. Therefore, you must accept that it and its contradiction are both provable (leading to an inconsistent system), or not accept it and now there are provable theorems that cannot be expressed in the system. Furthermore, that this can be constructed from anything with base arithmetic and induction over first-order logic (Gödel's original paper included how broadly it could be applied to basically every logical system).
    - kevindamm 3y ago
      The important thing to note is that it doesn't have anything to do with truth or truth-values of propositions. It breaks the fundamental operation of the provability of a statement. And, since many proofs are done by assuming a statement's inverse and trying to prove a contradiction, having a known contradiction in the set of provable statements can effectively allow any statement to be proven. Keeping the contradiction is not actually an option.
- Veserv 3y ago
  No. It merely prevents you from confirming every arbitrarily complex proof. Incompleteness is more like: I give you a convoluted mess of spaghetti code and claim it computes prime numbers and I demand you try to prove me wrong.
- Verdex 3y ago
  No. Godel means that we can't have an algorithmic box that we put a program into and out comes a true/false statement of halting. Nothing is stopping you from writing the proof manually for each program that you want to prove properties for. ALSO, you can write sub-turing complete programs. Those are allowed to have automated halting proofs (see idris et al).
  - kevindamm 3y ago
    What you're talking about is actually the Church-Turing thesis and the halting problem. While, yes, computability and provability are very closely related, it's important to get attribution correct. More details on what Gödel's Incompleteness Theorem really said are in a sibling comment so I won't repeat them here.
    - Verdex 3y ago
      > it's important to get attribution correct. Really? Says who? Or perhaps you'll prove it from first principles. Although if turns out to be difficult, that's okay. Somebody mentioned something about systems being either complete or consistent but never both. Some things can be true but not proveably so. Can't quite remember who it was though.
      - kevindamm 3y ago
        Fair enough, I was being annoyingly pedantic. [I believe that] it's important to get attribution correct.
        Verdex 3y ago
        To be fair, annoyingly pedantic is the best kind of pedantic. - Futurama (kind of)
        kevindamm 3y ago
        sounds technically correct Gödel's really was a rather unique mind, and the story of his death is kind of sad.. but I wonder if it takes such a severe kind of paranoia to look for how math can break itself, especially during that time when all the greatest mathematicians were in pursuit of formalizing a complete and consistent mathematics.
cochne 3y ago
I never really got how proofs are supposed to solve this issue. I think that would just move the bugs from the code into the proof definition. Your code may do what the proof says, but how do you know what the proof says is what you actually want to happen?
- dgacmu 3y ago
  Not really. Imagine the proof says: "in this protocol, when there are more than 0 participants, exactly one participant holds the lock at any time" It might be wrong, but it's pretty easy to inspect and has a much higher chance of being right than your code does. You then use proof refinement to eventually link this very high level statement down to the code implementing it. That's the vision, at least, and it's sometimes possible to achieve it. See, for example, Ironfleet: https://www.microsoft.com/en-us/research/publication/ironfleet-proving-practical-distributed-systems-correct/ https://www.microsoft.com/en-us/research/publication/ironfle...
- MaxBarraclough 3y ago
  A formal spec isn't just ordinary source-code by another name, it's at a quite different level of abstraction, and (hopefully) it will be proven that its invariants always hold. (This is a separate step from proving that the model corresponds to the ultimate deliverable of the formal development process, be that source-code or binary.) Bugs in the formal spec aren't impossible, but use of formal methods doesn't prevent you from doing acceptance testing as well. In practice, there's a whole methodology at work, not just blind trust in the formal spec. Software developed using formal methods is generally assured to be free of runtime errors at the level of the target language (divide-by-zero, dereferencing NULL, out-of-bounds array access, etc). This is a pretty significant advantage, and applies even if there's a bug in the spec. Disclaimer: I'm very much not an expert. Interesting reading: * An interesting case-study, albeit from a non-impartial source [PDF] https://www.adacore.com/uploads/downloads/Tokeneer_Report.pdf https://www.adacore.com/uploads/downloads/Tokeneer_Report.pd... * An introduction to the Event-B formal modelling method [PDF] https://www.southampton.ac.uk/~tsh2n14/publications/chapters/eventb-dbook13.pdf https://www.southampton.ac.uk/~tsh2n14/publications/chapters...
roenxi 3y ago
As always, the branding of formal methods sucks. As other commentators point out, it isn't technically possible to provide a formal proof that software is correct. And that is fine, because formal software methods don't do that. But right from the outset the approach is doomed to fail because its proponents write like they don't know what they are talking about and think they can write bug-free software. It really should be "write software with a formal spec". Once people start talking about "proof" in practice it sounds dishonest. It isn't possible to prove software and the focus really needs to be on the spec.
- hnfong 3y ago
  > It really should be "write software with a formal spec". The code is already a formal spec. Unless there are bugs in the language/compiler/interpreter, what the code is essentially formally well defined. As programming languages get better at enabling programmers to communicate intention as opposed to being a way to generate computer instructions, there's really no need for a separate "spec". Any so called "spec" that is not a programming language is likely not "formal" in the sense that the behavior is unambiguously well defined. Of course, you might be able to write the "spec" using a formal language that cannot be transformed into machine code, but assuming that the "spec" is actually well defined, then it's just that "compiling" the spec into machine code is too expensive in some way (eg. nobody has written a compiler, it's too computationally hard to deduce the actual intention even though it's well defined, etc.). But in essence it is still a "programming language", just one without a compiler/interpreter.
AnimalMuppet 3y ago
Formal proof of what? That it has no bugs? Ha! You can formally prove that it doesn't have certain kinds of bugs. And that's good! But it also is an enormous amount of work. And so, even for life-critical software, the vast majority is not formally proven, because we want more software than we can afford to formally prove.
- Verdex 3y ago
  This is an interesting point that I think a lot of programming can miss. Proving that the program has no bugs is akin to proving that the program won't make you feel sad. Like ... I'm not sure we have the math. One of the more important jobs of the software engineer is to look deep into your customer's dreams and determine how those dreams will ultimately make your customer sad unless there's some sort of intervention before you finish the implementation.
- makapuf 3y ago
  Yeah, if you can have a formally proven compiler from slides, poorly written user stories and clarification phone calls to x86_64 binary then alright.
- BoiledCabbage 3y ago
  Exactly, it's fundamentally impossible. Formal proofs can help with parts of the process, but it can guarantee no bugs in the product. These are the steps of software, and their transitions. It's fundamentally a game of telephone with errors at each step along the way. What actually would solve the customer's problem -> What the customer thinks they want -> What they communicate that they want -> What the requirements collector hears -> What the requirements collector documents -> How the implementor interprets the requirements -> What the implementor designs/plans -> What the implementor implements. Formal proofs can help with the last 3 steps. But again that's assuming the implementor can formalize every requirement they interpreted. And that's impossible as well, there will always be implicit assumptions about the running environment, performance, scale, the behavior of dependent processes/APIs. It helps with a small set of possible problems. If those problems are mission-critical then absolutely tackle them, but there will never be a situation where it can help with the first 5 steps of the problem, or with the implicit items in the 6th step above.
bluGill 3y ago
Even formally proved code can have bugs. If your requirement is wrong is the obvious thing. I don't work with formal proofs (I want to, I just don't know how), but I'm given to understand they have other real world limits that make them sometimes have other bugs.
radicalcentrist 3y ago
To quote Donald Knuth, "Beware of bugs in the above code; I have only proved it correct, not tried it."
kaba0 3y ago
Well, if your product is on the hello world complexity, you might make it bug-free by just yourself simply through chance. Formal proving doesn’t really scale much further, definitely not to “enterprise” product scale.

wvenable 3y ago

It's always amazing when I get a bug report from a product that's been running bug free in production for years with minimal changes but some user did some combination of things that had never been done and it blows up. Usually it's something extremely simple to fix too.

codegeek 3y ago
This happens a lot more than one may think especially with products that have lot of features. Some features are used sparingly and the moment a customer uses that feature a bit more in depth, boom. Something is broken.
- tylerchurch 3y ago
  > especially with products that have lot of features No kidding. I'm 2 or 3 years into working on a SaaS app started in ~2013 and I still get bug reports from users that make me say "what!? we have that feature!?"