5 ms·

> Mathematical proofs of code are not suitable for most systems. It depends what kind of math and what they're doing though. Systems like Coq give you much mor

> Mathematical proofs of code are not suitable for most systems. It depends what kind of math and what they're doing though. Systems like Coq give you much more trustable code to put in your system, and higher degrees of trust for clients. But systems like Idris actually let you write code and use the proof engine to write trustworthy code. Most of that "math", from the perspective of a programmer, is a small subset of graph theory, formal logic, and category theory useful for proving relationships and reflexivity so that the machine can help you. > Even unit tests which don't involve proofs can be a problem sometimes because they lock down API inputs and outputs. This is a much bigger problem than "hand written mocks are bad" (which they are, I agree). 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. What's more, and I really want to push this point so I'll emphasize it: quickly producing broken code helps almost no one. If you're an artist playing with making a synthesizer whine? Maybe okay. If you're writing software intended to face the world and do real work? We can't just keep pretending we're all smart enough to do this without mechanical aid; we're NOT smart enough to do this without mechanical aid anymore. Programs integrate too many libraries and APIs. > I imagine that adding proofs as part of the unit test suite would further increase the productivity cost overhead by a massive factor. With Idris, it makes it so the program can write code for you. I've been learning it over the last 2 weeks and I'm totally fascinated by how much drudgery it takes out of total programming. > In software development, you should avoid treating the code like if it's special or perfect This is precisely what formal methods do! You challenge every piece of code you can and say, "Prove to me that what you've written doesn't have an obvious flaw!" You rewrite until both the human and the proof engine cannot see anymore. It is not sacred at that point (no one believes this), but at least you've acknowledged that you can write errors and started to mitigate them. > There are always downsides, and we're crazy to pretend that every fancy new methodology is a silver bullet. Actually, the entire industry has started to demand that developers do a lot more computation on their ends to make better software. The "prove more of your program and write total code" is just one side of the "do more work on your end" school. Another is, "Your software is in fact the output of this algorithm training from a dataset on 4 GPUs." We probably need a similar step forward for APIs (where APIs are invalid & unusable without a spec that governs them). It is a change, but most commercial software engineers are handling user data that can be leveraged in disastrous every day. As you say, we need the wisdom to realize that it's difficult to guess the use case or security impact of the code we write on a daily basis, and we need to start taking that fact seriously. These heady days of being able to deny responsibility and shove out any software we want without consequence need to end.

crdoconnor 9y ago
>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 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.