5 ms·

If I had complete enough specifications for any interesting program that formal methods would be interesting, I think I would just be easier to hit compile on t

by jgeada 4y ago

If I had complete enough specifications for any interesting program that formal methods would be interesting, I think I would just be easier to hit compile on that spec. Yes, there are a subset of interesting bugs related to edge cases, but the real problematic bugs are when what the software does does not match what was expected, even if nobody really could articulate what was expected in the first place. The art of software engineering isn't the coding, it is asking enough questions to know what the actual problem to be solved is.

drewcoo 4y ago
I think the interesting part isn't in a single component's edge cases at all, but in how complex webs of many, many things interact. I've yet to see a hard debugging problem that didn't boil down to something like, in the best of possible worlds: "component A expected something to meet promise FOO when it calls component B, because that's obvious, right?" combined with "component B just passes requests and routes results, dude, component C is messed up" combined with "component C never promised that behavior and if you look at our spec it even says so!" That's an example of your "does not match what was expected" case. I think most of formal methods is an academic waste of time. Whether they take a more formal or a more practical approach, I see high value in contract tests and data flow analysis because they're more likely to catch the bugs that cross Conway's code/org boundaries.
- im_down_w_otp 4y ago
  This kind of, “Just what the heck in this pile of parts is impacting the other stuff and how is the other stuff impacting this part?” was precisely the angle we took with our V&V tools.
- jgeada 4y ago
  Yes, this! What would be helpful is if formal methods were powerful enough to be able to prove contracts and assertions about expectations and invariants; however, all formal systems I've experienced are not powerful enough to do this at scale in any interesting program, not without spending way more time reconstructing the entire system in the formal world, with the attendant likelihood of introducing spec bugs in that reconstruction. It is entirely different in the world of hardware, where the specification in many cases is the RTL and the thing being proved is the, supposedly identical, physical implementation.
- rsrsrs86 4y ago
  Formal methods have their applications and specific use cases. It all depends on how much is at stake, economically. I suggest checking into Alloy, which is far easier to work with. It feels like writing a SQL schema, but you get bounded model checking and much more.
- guai888 4y ago
  formal methods has value in safety related software. When you are developing software for airplane, rail, automobile and nuclear power station, any tools that might improve safety merit consideration.
- mcguire 4y ago
  That's actually what many formal tools excel at. Of course, you have to do have to define "never promised that behavior" which is extra work that nobody wants to do.
  - Animats 4y ago
    Yes. That's "design by contract", which is extremely useful for determining who's at fault. This came out of aerospace, where it's taken seriously. If A won't interoperate with B, you check the interface spec. If A is out of compliance, A has to be fixed. If B is out of compliance, B has to be fixed. If you can't tell, the interface spec has to be fixed. This is why you can unplug Pratt and Whitney engines from an airplane and plug in Rolls-Royce engines. This worked in the era when the buyer had more clout than the seller. Now, if A won't interoperate with B, it's the problem of whomever is smaller.
    - tomcam 4y ago
      > This is why you can unplug Pratt and Whitney engines from an airplane and plug in Rolls-Royce engines. Wait wut? Are you talking about their embedded software or the hardware itself? Because if you're talking about the hardware, I'm about to be dumbfounded that there are formal verifications of hardware, my mind is about to be blown.
    - mcguire 4y ago
      You could think of many of the formal tools outside of dependently typed programming as design by contract plus a thingy that complains if the contract doesn't work.
miloignis 4y ago
You don't need to prove everything against a complete spec, you can prove that things have particular properties you care about, from higher level behaviors like user data can only be accessed by the user down to there are no out of bounds array accesses. You could prove some complex data-structure to be a correct implementation of some logical data-structure and then prove that your service won't deadlock. There are a ton of interesting, impactful properties to prove that aren't "create a complete specification and prove the implementation refines it", and even that usage I think is more impactful for removing bugs and vulnerabilities than you're giving it credit for - even something as simple as sorting, Java had a bug in their Timsort implementation for a decade which was discovered when trying to verify it with formal methods: http://envisage-project.eu/wp-content/uploads/2015/02/sorting.pdf http://envisage-project.eu/wp-content/uploads/2015/02/sortin... ). Note too that if you compiled the simplest/easiest-to-understand spec for something like sorting you'd get something like bubble sort, not Timsort, though you are much more likely to want the latter.
commandlinefan 4y ago
> I think I would just be easier to hit compile on that spec I have a hard time not being similarly skeptical about formal methods. They promise the ultimate holy grail of software development - release software with zero defects - but demand what appears to be years of study before you actually see results. On the one hand, there's lots of examples of techniques and tactics that promise amazing results if you "put in the work", even outside of software (like fitness and music) - but in over 30 years of software development practice, I've never met anybody who was applying formal methods at all, much less to achieve defect-free software. If it could deliver what it promised even with a "mere" five years of dedicated study, I'd expect it to be more widespread by now.
- deterministic 4y ago
  CompCert, seL4, EverParse, AWS TLA+, Azure infrastructure code proven correct etc. You might already be using proven correct software somewhere in your stack without knowing it. You most certainly will be trusting your life with it flying Airbus.
- cscurmudgeon 4y ago
  I have met tons of folks who have used this in practice. It tends more applied in domains where errors can be costly. E.g., this won't be that much useful in the JS/NodeJS. https://www.amazon.science/publications/how-amazon-web-services-uses-formal-methods https://www.amazon.science/publications/how-amazon-web-servi... https://link.springer.com/chapter/10.1007/978-3-642-34281-3_2 https://link.springer.com/chapter/10.1007/978-3-642-34281-3_... > They promise the ultimate holy grail of software development - release software with zero defects Thats a straw man. It is just another tool.
- noisenotsignal 4y ago
  Years of study are definitely not required to get up and running! I attended a 3 day workshop for TLA+ and spent ~2 weeks modeling a new project that my team was working on. I found lots of potential edge cases that would result in data inconsistencies without even having to write tests or think about how to articulate the issue in the first place, as the model checker is able to output the exact program flow that results in the error. You still need to make sure your implementation matches the spec, but that’s an easier task than squashing concurrency bugs, let alone figuring out how to repro in the first place! The hope is that by writing the spec you avoid a good chunk of errors from the start instead of encountering them one by one.
mcguire 4y ago
One advantage of formal methods is in determining "what was expected" (including all the goofy edge cases) without having to burrow into the details of code. Take a look at Alloy (http://alloytools.org/ http://alloytools.org/) and TLA+ (https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html) for example. (Or even the ancient Z ("Zed") notation (https://www.cs.cmu.edu/~15819/zedbook.pdf https://www.cs.cmu.edu/~15819/zedbook.pdf)).

by jgeada 4y ago

drewcoo 4y ago

I think the interesting part isn't in a single component's edge cases at all, but in how complex webs of many, many things interact. I've yet to see a hard debugging problem that didn't boil down to something like, in the best of possible worlds: "component A expected something to meet promise FOO when it calls component B, because that's obvious, right?" combined with "component B just passes requests and routes results, dude, component C is messed up" combined with "component C never promised that behavior and if you look at our spec it even says so!" That's an example of your "does not match what was expected" case. I think most of formal methods is an academic waste of time. Whether they take a more formal or a more practical approach, I see high value in contract tests and data flow analysis because they're more likely to catch the bugs that cross Conway's code/org boundaries.

im_down_w_otp 4y ago
This kind of, “Just what the heck in this pile of parts is impacting the other stuff and how is the other stuff impacting this part?” was precisely the angle we took with our V&V tools.
jgeada 4y ago
Yes, this! What would be helpful is if formal methods were powerful enough to be able to prove contracts and assertions about expectations and invariants; however, all formal systems I've experienced are not powerful enough to do this at scale in any interesting program, not without spending way more time reconstructing the entire system in the formal world, with the attendant likelihood of introducing spec bugs in that reconstruction. It is entirely different in the world of hardware, where the specification in many cases is the RTL and the thing being proved is the, supposedly identical, physical implementation.
rsrsrs86 4y ago
Formal methods have their applications and specific use cases. It all depends on how much is at stake, economically. I suggest checking into Alloy, which is far easier to work with. It feels like writing a SQL schema, but you get bounded model checking and much more.
guai888 4y ago
formal methods has value in safety related software. When you are developing software for airplane, rail, automobile and nuclear power station, any tools that might improve safety merit consideration.
mcguire 4y ago
That's actually what many formal tools excel at. Of course, you have to do have to define "never promised that behavior" which is extra work that nobody wants to do.
- Animats 4y ago
  Yes. That's "design by contract", which is extremely useful for determining who's at fault. This came out of aerospace, where it's taken seriously. If A won't interoperate with B, you check the interface spec. If A is out of compliance, A has to be fixed. If B is out of compliance, B has to be fixed. If you can't tell, the interface spec has to be fixed. This is why you can unplug Pratt and Whitney engines from an airplane and plug in Rolls-Royce engines. This worked in the era when the buyer had more clout than the seller. Now, if A won't interoperate with B, it's the problem of whomever is smaller.
  - tomcam 4y ago
    > This is why you can unplug Pratt and Whitney engines from an airplane and plug in Rolls-Royce engines. Wait wut? Are you talking about their embedded software or the hardware itself? Because if you're talking about the hardware, I'm about to be dumbfounded that there are formal verifications of hardware, my mind is about to be blown.
  - mcguire 4y ago
    You could think of many of the formal tools outside of dependently typed programming as design by contract plus a thingy that complains if the contract doesn't work.

miloignis 4y ago

You don't need to prove everything against a complete spec, you can prove that things have particular properties you care about, from higher level behaviors like user data can only be accessed by the user down to there are no out of bounds array accesses. You could prove some complex data-structure to be a correct implementation of some logical data-structure and then prove that your service won't deadlock. There are a ton of interesting, impactful properties to prove that aren't "create a complete specification and prove the implementation refines it", and even that usage I think is more impactful for removing bugs and vulnerabilities than you're giving it credit for - even something as simple as sorting, Java had a bug in their Timsort implementation for a decade which was discovered when trying to verify it with formal methods: http://envisage-project.eu/wp-content/uploads/2015/02/sorting.pdf http://envisage-project.eu/wp-content/uploads/2015/02/sortin... ). Note too that if you compiled the simplest/easiest-to-understand spec for something like sorting you'd get something like bubble sort, not Timsort, though you are much more likely to want the latter.

commandlinefan 4y ago

> I think I would just be easier to hit compile on that spec I have a hard time not being similarly skeptical about formal methods. They promise the ultimate holy grail of software development - release software with zero defects - but demand what appears to be years of study before you actually see results. On the one hand, there's lots of examples of techniques and tactics that promise amazing results if you "put in the work", even outside of software (like fitness and music) - but in over 30 years of software development practice, I've never met anybody who was applying formal methods at all, much less to achieve defect-free software. If it could deliver what it promised even with a "mere" five years of dedicated study, I'd expect it to be more widespread by now.

deterministic 4y ago
CompCert, seL4, EverParse, AWS TLA+, Azure infrastructure code proven correct etc. You might already be using proven correct software somewhere in your stack without knowing it. You most certainly will be trusting your life with it flying Airbus.
cscurmudgeon 4y ago
I have met tons of folks who have used this in practice. It tends more applied in domains where errors can be costly. E.g., this won't be that much useful in the JS/NodeJS. https://www.amazon.science/publications/how-amazon-web-services-uses-formal-methods https://www.amazon.science/publications/how-amazon-web-servi... https://link.springer.com/chapter/10.1007/978-3-642-34281-3_2 https://link.springer.com/chapter/10.1007/978-3-642-34281-3_... > They promise the ultimate holy grail of software development - release software with zero defects Thats a straw man. It is just another tool.
noisenotsignal 4y ago
Years of study are definitely not required to get up and running! I attended a 3 day workshop for TLA+ and spent ~2 weeks modeling a new project that my team was working on. I found lots of potential edge cases that would result in data inconsistencies without even having to write tests or think about how to articulate the issue in the first place, as the model checker is able to output the exact program flow that results in the error. You still need to make sure your implementation matches the spec, but that’s an easier task than squashing concurrency bugs, let alone figuring out how to repro in the first place! The hope is that by writing the spec you avoid a good chunk of errors from the start instead of encountering them one by one.

mcguire 4y ago

One advantage of formal methods is in determining "what was expected" (including all the goofy edge cases) without having to burrow into the details of code. Take a look at Alloy (http://alloytools.org/ http://alloytools.org/) and TLA+ (https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html) for example. (Or even the ancient Z ("Zed") notation (https://www.cs.cmu.edu/~15819/zedbook.pdf https://www.cs.cmu.edu/~15819/zedbook.pdf)).