6 ms·

>But it's quite out of scope to complain that because API endpoints are often sloppily deployed without versioning or introspectability, that all formal methods

>But it's quite out of scope to complain that because API endpoints are often sloppily deployed without versioning or introspectability, that all formal methods are wrong. It's not so much that they're "all wrong", but when the majority of bugs you face are not logical or algorithmic in nature but driven by incorrect specifications or problems dealing with the outside world (including but not limited to sloppy APIs), then formal methods will impose a stupidly high cost for almost no benefit. To take the famous Mars Climate Orbiter bug as an example - had the software been formally proven then it still would have gone down in a ball of fire because the software was built upon a faulty presumption. An integration test that exercised both the data and the code in a realistic environment would have saved it though, as would better spec communication between the two teams (e.g. some form of BDD). The chief investigator, Arthur Stephenson, even explicitly called out the lack of sufficient end to end testing. I'm sure formal methods are great for proving that, e.g. a particular sorting algorithm always works, but frankly, sorting algos are the type of thing I import and just assume works and I've yet to see a bug in the wild that invalidates that assumption, whereas a faulty interaction between two poorly specified modules is a problem I see in teams on a near daily basis.

KirinDave 9y ago
> It's not so much that they're "all wrong", but when the majority of bugs you face are not logical or algorithmic in nature but driven by incorrect specifications But automation could verify this. Unit tests don't do anything if they aren't run. Specifications don't do anything if they aren't checked. Do you have CI/CD? Use it! > then formal methods will impose a stupidly high cost for almost no benefit. Except that lots of business logic errors, resource handling errors, and mathematical errors still exist in modern code at all levels. And you're also assuming the "cost" is "stupidly high" which people in this thread are telling you is false. Finally, please forgive me for being so blunt... If you're delivering code you haven't tested to hit a timetable, you're part of a scam. People don't want broken code. People aren't buying security holes. People aren't asking for things that almost work but then dump user data by the score. No one wants this, but developers like us keep insisting it's fine because they're not personally responsible. I wish that you or I could be fined if we didn't show due diligence. It'd be good for the industry. > To take the famous Mars Climate Orbiter bug as an example - had the two individual modules of software been formally proven then it still would have gone down in a ball of fire. An integration test that exercised both modules would have saved it though, as would better spec communication between the two teams (dare I say it? BDD). > To take the famous Mars Climate Orbiter bug as an example - had the two individual modules of software been formally proven then it still would have gone down in a ball of fire. Cool, except that the module integrating these, if validated, would have caught this. Which brings me to my second point: > An integration test that exercised both modules would have saved it though, I'm not sure why you think using a computer to write proofs about your software somehow magically excludes integration tests. Excluding integration testing is something humans already do well. If anything, running a type checker and using pre-existing proofs on an new module that integrates them is much more than most people do. > as would better spec communication between the two teams (dare I say it? BDD). The irony here: BDD is a less formal but similar technique to writing proofs. BDD could be integrated directly into the development piepline (as it is with Idris) and the compiler could tell you when you missed a spot, or forgot to handle something. It seems you only dislike it when the compiler does it. > I'm sure formal methods are great for proving that, e.g. a particular sorting algorithm always works, but frankly, sorting algos are the type of thing I import and just assume works What is the difference between checking if a program properly closes a socket or if a sorting algorithm works? From a proof checker's perspective: it's very little. > sorting algos are the type of thing I import and just assume works And this is and example of the mentality that ensures that despite the fact that we've seen the O(n log n) speed limit for sorting shattered, no one knows or cares. > whereas a faulty interaction between two poorly specified modules is a problem I see in teams on a near daily basis. Why don't you want to make it easier to write better modules, and make it easier to verify the integration of modules? "It's hard so I won't even try," seems to be your reasoning here despite several people saying it's possible.
- crdoconnor 9y ago
  >But automation could verify this. Yes, that's what I was arguing. >Except that lots of business logic errors, resource handling errors, and mathematical errors still exist in modern code at all levels. And you're also assuming the "cost" is "stupidly high" which people in this thread are telling you is false. My experience with formal proofs is it imposes a high cost. I don't think that there are people in this thread who believe that you can impose formal proofs on a system without incurring a significant cognitive overhead (and possibly other costs too). If they exist, they are simply wrong. >I'm not sure why you think using a computer to write proofs about your software somehow magically excludes integration tests. I'm not saying that it does. I'm saying that the kinds of bugs unveiled by formal methods are, in most applications, rare and obscure and the bugs unveiled by integration tests are, in most applications, common and important. When I have limited resources (everybody has limited resources), I tend to take the approach that has the best ROI in finding bugs. For most applications, that isn't formal proofs. >Cool, except that the module integrating these, if validated, would have caught this. You still aren't getting it. The module was built upon faulty presumptions. Peter Norvig himself said that no language, no matter how type strict, would have enforced this convention. >The irony here: BDD is a less formal but similar technique to writing proofs. I'm sorry, but writing user stories on the back of a napkin (yes, that's BDD too) isn't a similar technique to formal proofs in any way, shape or form. BDD is simply a means of communicating example driven specs that may or may not be turned into executable user stories. Automated tests (a common side effect of BDD) are not really similar to proofs either. >What is the difference between checking if a program properly closes a socket or if a sorting algorithm works? The likelihood of bugs in the definition are significantly higher the less abstract your code gets. To wit: maybe your presumption that the socket needs to be closed is wrong. >Why don't you want to make it easier to write better modules, and make it easier to verify the integration of modules? I absolutely do, that's why I use the right tool for the job.
  - KirinDave 9y ago
    > My experience with formal proofs is it imposes a high cost. What is that experience within the last 5 years. Does it include Idris, Agda, and Coq? > I don't think that there are people in this thread who believe that you can impose formal proofs on a system without incurring a significant cognitive overhead The idea is that by asking humans to make small proofs, the remainder of the majority of additional cognitive overhead can be assumed by the machine. This conversation has a curious pre-assumption that this cognitive load is "new". In fact, it's not. It's an alternative approach to working with the complexity already apparent in our domain. > You still aren't getting it. The module was built upon faulty presumptions. Peter Norvig himself said that no language, no matter how type strict, would have enforced this convention. Why is Peter's comment relevant here? > I'm sorry, but writing user stories on the back of a napkin (yes, that's BDD too) isn't a similar technique to formal proofs in any way, shape or form. It is if you care about the results. A lot of modern BDD process has humans as verifiers. And no one's saying that has to go away. But we might need it LESS for certain parts of the system. Certainly in my user-facing fintech applications I have wished for tools that could do this. Sadly a lot of my work in that field predates the usability of a lot of these tools. > I absolutely do, that's why I use the right tool for the job. And the right tool for the job is evidently not a computer? What I think you're missing is that these formal proof systems come with an implicit power: the ability to extend the a more generic type system at build time to reason about your domain. This application is as radical in nature as it is classical. Everyone in every domain has suggested for half a century that we work to bring our code closer to our domain and further from the minutiae of machine implementation. Modern systems seek to do this by creating stable abstractions to build upon. This takes 2 shapes: trained by data (classifiers, regressions, and statistical methods) or refined by logic (proofs, dependent types, type inference and verification). The line between these types is somewhat transient, and over time it's almost certain it will blur. Already we see F# using "Type Providers" that let you use samples derived directly from an API (or specs, or both). These can be obtained as part of the build process, and then the program can be checked against the spec. There is only one real downside to this approach: it makes development require even more computational power. But given that we're solving a much harder problem than the users of our software, the asymmetry seems reasonable. I think you and I agree in the general strokes but you don't like the word "proof", if I'm being honest. I don't know why that word bothers you so much. Did you watch the video? Have you tried Agda, Coq and Idris?

KirinDave 9y ago

> It's not so much that they're "all wrong", but when the majority of bugs you face are not logical or algorithmic in nature but driven by incorrect specifications But automation could verify this. Unit tests don't do anything if they aren't run. Specifications don't do anything if they aren't checked. Do you have CI/CD? Use it! > then formal methods will impose a stupidly high cost for almost no benefit. Except that lots of business logic errors, resource handling errors, and mathematical errors still exist in modern code at all levels. And you're also assuming the "cost" is "stupidly high" which people in this thread are telling you is false. Finally, please forgive me for being so blunt... If you're delivering code you haven't tested to hit a timetable, you're part of a scam. People don't want broken code. People aren't buying security holes. People aren't asking for things that almost work but then dump user data by the score. No one wants this, but developers like us keep insisting it's fine because they're not personally responsible. I wish that you or I could be fined if we didn't show due diligence. It'd be good for the industry. > To take the famous Mars Climate Orbiter bug as an example - had the two individual modules of software been formally proven then it still would have gone down in a ball of fire. An integration test that exercised both modules would have saved it though, as would better spec communication between the two teams (dare I say it? BDD). > To take the famous Mars Climate Orbiter bug as an example - had the two individual modules of software been formally proven then it still would have gone down in a ball of fire. Cool, except that the module integrating these, if validated, would have caught this. Which brings me to my second point: > An integration test that exercised both modules would have saved it though, I'm not sure why you think using a computer to write proofs about your software somehow magically excludes integration tests. Excluding integration testing is something humans already do well. If anything, running a type checker and using pre-existing proofs on an new module that integrates them is much more than most people do. > as would better spec communication between the two teams (dare I say it? BDD). The irony here: BDD is a less formal but similar technique to writing proofs. BDD could be integrated directly into the development piepline (as it is with Idris) and the compiler could tell you when you missed a spot, or forgot to handle something. It seems you only dislike it when the compiler does it. > I'm sure formal methods are great for proving that, e.g. a particular sorting algorithm always works, but frankly, sorting algos are the type of thing I import and just assume works What is the difference between checking if a program properly closes a socket or if a sorting algorithm works? From a proof checker's perspective: it's very little. > sorting algos are the type of thing I import and just assume works And this is and example of the mentality that ensures that despite the fact that we've seen the O(n log n) speed limit for sorting shattered, no one knows or cares. > whereas a faulty interaction between two poorly specified modules is a problem I see in teams on a near daily basis. Why don't you want to make it easier to write better modules, and make it easier to verify the integration of modules? "It's hard so I won't even try," seems to be your reasoning here despite several people saying it's possible.

crdoconnor 9y ago
>But automation could verify this. Yes, that's what I was arguing. >Except that lots of business logic errors, resource handling errors, and mathematical errors still exist in modern code at all levels. And you're also assuming the "cost" is "stupidly high" which people in this thread are telling you is false. My experience with formal proofs is it imposes a high cost. I don't think that there are people in this thread who believe that you can impose formal proofs on a system without incurring a significant cognitive overhead (and possibly other costs too). If they exist, they are simply wrong. >I'm not sure why you think using a computer to write proofs about your software somehow magically excludes integration tests. I'm not saying that it does. I'm saying that the kinds of bugs unveiled by formal methods are, in most applications, rare and obscure and the bugs unveiled by integration tests are, in most applications, common and important. When I have limited resources (everybody has limited resources), I tend to take the approach that has the best ROI in finding bugs. For most applications, that isn't formal proofs. >Cool, except that the module integrating these, if validated, would have caught this. You still aren't getting it. The module was built upon faulty presumptions. Peter Norvig himself said that no language, no matter how type strict, would have enforced this convention. >The irony here: BDD is a less formal but similar technique to writing proofs. I'm sorry, but writing user stories on the back of a napkin (yes, that's BDD too) isn't a similar technique to formal proofs in any way, shape or form. BDD is simply a means of communicating example driven specs that may or may not be turned into executable user stories. Automated tests (a common side effect of BDD) are not really similar to proofs either. >What is the difference between checking if a program properly closes a socket or if a sorting algorithm works? The likelihood of bugs in the definition are significantly higher the less abstract your code gets. To wit: maybe your presumption that the socket needs to be closed is wrong. >Why don't you want to make it easier to write better modules, and make it easier to verify the integration of modules? I absolutely do, that's why I use the right tool for the job.
- KirinDave 9y ago
  > My experience with formal proofs is it imposes a high cost. What is that experience within the last 5 years. Does it include Idris, Agda, and Coq? > I don't think that there are people in this thread who believe that you can impose formal proofs on a system without incurring a significant cognitive overhead The idea is that by asking humans to make small proofs, the remainder of the majority of additional cognitive overhead can be assumed by the machine. This conversation has a curious pre-assumption that this cognitive load is "new". In fact, it's not. It's an alternative approach to working with the complexity already apparent in our domain. > You still aren't getting it. The module was built upon faulty presumptions. Peter Norvig himself said that no language, no matter how type strict, would have enforced this convention. Why is Peter's comment relevant here? > I'm sorry, but writing user stories on the back of a napkin (yes, that's BDD too) isn't a similar technique to formal proofs in any way, shape or form. It is if you care about the results. A lot of modern BDD process has humans as verifiers. And no one's saying that has to go away. But we might need it LESS for certain parts of the system. Certainly in my user-facing fintech applications I have wished for tools that could do this. Sadly a lot of my work in that field predates the usability of a lot of these tools. > I absolutely do, that's why I use the right tool for the job. And the right tool for the job is evidently not a computer? What I think you're missing is that these formal proof systems come with an implicit power: the ability to extend the a more generic type system at build time to reason about your domain. This application is as radical in nature as it is classical. Everyone in every domain has suggested for half a century that we work to bring our code closer to our domain and further from the minutiae of machine implementation. Modern systems seek to do this by creating stable abstractions to build upon. This takes 2 shapes: trained by data (classifiers, regressions, and statistical methods) or refined by logic (proofs, dependent types, type inference and verification). The line between these types is somewhat transient, and over time it's almost certain it will blur. Already we see F# using "Type Providers" that let you use samples derived directly from an API (or specs, or both). These can be obtained as part of the build process, and then the program can be checked against the spec. There is only one real downside to this approach: it makes development require even more computational power. But given that we're solving a much harder problem than the users of our software, the asymmetry seems reasonable. I think you and I agree in the general strokes but you don't like the word "proof", if I'm being honest. I don't know why that word bothers you so much. Did you watch the video? Have you tried Agda, Coq and Idris?