6 ms·

Formal methods only solve half my problems

69 points by mjb 4y ago

xupybd 4y ago
My work is often little internal tools and a few b2b websites. I hate down time due to bugs. I still get nervous when I install to production. Always taking back up after back up and talking myself through the process of rebuilding from scratch. Just in case this time I have to. Would formal methods help with code at this level? I suspect the cost benefit isn't there. Though I wish it was. I've seen the difference between having tests and not having them. Development time decreases, and my stress levels decrease. Is this the same with formal methods?
- subjectsigma 4y ago
  I work in government contracting with very expensive and heavy pieces of metal that kill people if something goes wrong, and even I can't convince people they need to use formal methods to help write their code. So the easy answer is 'no'. That being said, FM is an enormous spectrum; if you squint a little, writing really good user stories could be considered a 'formal specification'. There's a really good paper from Amazon about model checking (Newcombe 2014 IIRC) where they make the bold statement that "Doing the math didn't help us find that many mistakes, nor did using the model checker; the thing that was most helpful was sitting down and forcing ourselves to come up with really good definitions. Like what does X really mean?" So it doesn't have to be as complicated as you think. So if you want to start as simple as possible, I would recommend something like this: https://www.hillelwayne.com/post/decision-table-patterns/ https://www.hillelwayne.com/post/decision-table-patterns/
  - aeneasmackenzie 4y ago
    Leslie Lamport had an essay about this. Without a spec, even if it's just "Serves the user's homepage", your program is not even wrong.
  - xupybd 4y ago
    Thanks! I'll have a read. Your comment helps clarify the situation.
    - rramadass 4y ago
      You may find https://markusvoelter.medium.com/the-evolution-of-decision-tables-80ce77bf984c https://markusvoelter.medium.com/the-evolution-of-decision-t... helpful. He also has a lot on DSLs which is worth reading. There is also a more powerful version of Decision Tables called Tabular Expressions (from D.L.Parnas) which you can use. A nice succinct reference to Formal Methods is Concise Guide to Formal Methods by Gerard O'Regan. I think simplified versions of Formal Methods can be used profitably for your use-cases. Start with Assertions, Design-by-Contract and Decision Tables.
- quixoticaxolotl 4y ago
  Formal methods will likely not help you - they can only show a _specification_ is sound, but not the _implementation_. That is, formal methods aren't testing the code you write, just the design concept behind it. For the design concepts you are likely to encounter in your situations, you absolutely do not need a formal proof that your stuff works - unless you are inventing (e.g.) a new cryptography suite from scratch or a large distributed system that must handle a massive amount of concurrency, there is zero advantage you would get over following best practices.
  - quixoticaxolotl 4y ago
    If you are afraid of deploys, you need to lean into CI/CD and the whole DevOps movement more. That is the solution to being able to deploy without stressing about it.
  - sangel 4y ago
    You can formally verify all the way to C, C#, Haskell, or even assembly if you use tools like Dafny, Coq, or Vale (for verified assembly). Several projects do this. It’s a lot of work for sure though.
    - quixoticaxolotl 4y ago
      Dafny is a really cool find, thank you!
  - tluyben2 4y ago
    Idris 2 writes pretty quickly and you can prove the parts you want. It’s not blazingly fast but fast enough for many purposes and I definitely have far far less bugs and generally better code. Only for hobby projects so far but it is quite a brilliant. It is verified implementation.
  - InefficientRed 4y ago
    > Formal methods will likely not help you - they can only show a _specification_ is sound, but not the _implementation_. I'm not sure where this idea came from. Are you in hardware? I guess in hardware that makes sense. Anyways, in software, formal methods can absolutely show that an implementation meets a specification. In fact, that has always been one of their canonical use cases in software systems, at least since the 70s or maybe early 80s. Formal methods can also be used with very ad hoc specifications, or with very general specifications, or increasingly without any explicitly specification at all (eg by inferring specifications). > cryptography suite from scratch or a large distributed system... Or aerospace software, or automotive software, or certain financial software, or industrial control systems, or any complex billing/access control, or... > there is zero advantage you would get over following best practices. I wrote a bunch of static analyses that checked for common configuration errors in Django apps which saved us many weekends. YMMV.
- yakshaving_jgt 4y ago
  I don’t think FM methods make economic sense in your case. They might if you were writing a distributed system, but writing some B2B websites probably means you’re best served with a monolithic system with both tests and types.
ncmncm 4y ago
Half would be damn good. Better would be solving the hard half.
- dym_sh 4y ago
  shrodinger's hard half – its always the one left unsolved
csours 4y ago
The longer I spend in IT/Software Dev, the more I see a dichotomy between Correctness and Usefulness. You can certainly have both, but different people concentrate on either correctness or usefulness. I think the future of software dev is people who understand both.
- justahuman74 4y ago
  The tools make it very hard to do both at the same time. To pick a topic, is there something I could write shell-style scripts in that leans towards correctness?
  - csours 4y ago
    Correctness needs a specification. Correctness hates side effects. Shell type scripts are all about side effects.
  - pharmakom 4y ago
    Yes! F# scripts Some features: - open-source - cross-platform - quick editing with syntax highlighting, type annotations etc. in VS Code - run in a single command (‘dotnet fsi script.fsx’) - type-safe but with global type inference - grab dependencies using directives in the script (no project manifests or global dependencies) The added safety of a typed language is fantastic for scripting because it’s not worth writing tests for most scripts.
  - simonmic 4y ago
    Haskell (using https://docs.haskellstack.org/en/stable/GUIDE/#script-interpreter https://docs.haskellstack.org/en/stable/GUIDE/#script-interp...). The downside: requires 1. installing stack and 2. waiting for it to install ghc and libs on first run of the script.
SEJeff 4y ago
The architect of AWS and author of Dynamodb has very good thoughts on formal methods. They’re worth a read: https://perspectives.mvdirona.com/2014/07/challenges-in-designing-at-scale-formal-methods-in-building-robust-distributed-systems/ https://perspectives.mvdirona.com/2014/07/challenges-in-desi...
- colmmacc 4y ago
  Oh man, I really can't resist adding to the record a bit here. The author of the article - Marc Brooker - has worked (and led!) on formal methods at AWS and DynamoDB much more than James. The paper James linked to in his post was authored by ... Marc Brooker! so this comment just reads funny to me. Even though I know it wasn't intended that way. James isn't the architect of AWS either, the scale we're at and the way we organize ourselves mean we don't really have any single architects of anything. Also EC2, S3, SQS, and more were in place by the time James joined. But I'm not trying to talk down James, because James has been much more influential and important to AWS success than an architect! His technical and business insights, his vision and drive, and his focus on some really very key levers have been monumental drivers of AWS. I know I've learned a lot from him, and still do. He's so good at it that he's now on the Amazon leadership team, reporting directly to our CEO!
  - SEJeff 4y ago
    Ah well you would know much better than me! I heard someone mention James as the architect of aws and recall him mentioning designing dynamodb. Did he do that, or am I universally wrong sans his love for formal methods? Thanks for the clarification though. This is truly why I enjoy HN so much. The ability to get corrected by the experts is an honor :)
mbrodersen 4y ago
Wow. Any solution that solves 50% of problems is pretty damn good!
westurner 4y ago
From "Discover and Prevent Linux Kernel Zero-Day Exploit Using Formal Verification" https://news.ycombinator.com/item?id=30194993 https://news.ycombinator.com/item?id=30194993 : > Can there still be side channel attacks in formally verified systems? Can e.g. TLA+ help with that at all? Side-channel attack https://en.wikipedia.org/wiki/Side-channel_attack https://en.wikipedia.org/wiki/Side-channel_attack
- _vdpp 4y ago
  Yes, there can still be side-channel and out-of-band attacks in FV systems. For example, pouring water into the server rack. That’s a cheeky example, but things like timing side-channels via speculative execution and cache hits wouldn’t be addressed by FV at the software level. I think there is some ongoing research for verifying software/hardware interactions but I’m not aware of a product in widespread use that checks this. The use of constant-time algorithms for crypto is a way to mitigate things like timing side-channels, and there are other techniques like disabling hyper-threading that can help. The depressing fact is that side channels exist any time there’s a shared computing resource. The question is how noisy the channel is, the data rate, etc.
  - westurner 4y ago
    It might be argued that side channels exist whenever there is a shared channel; which is always, because plenoptic functions, wave function, air gap, ram bus mhz, nonlocal entanglement Category:Side-channel attacks https://en.wikipedia.org/wiki/Category:Side-channel_attacks https://en.wikipedia.org/wiki/Category:Side-channel_attacks
rurban 4y ago
I'm using better model checker tools, and they also only solve half of my problems. but all the tools together solve everything. https://blog.nubix.de/index.php/2022/04/06/testing-baremetal-firmware-at-nubix/ https://blog.nubix.de/index.php/2022/04/06/testing-baremetal...

69 points by mjb 4y ago

My work is often little internal tools and a few b2b websites. I hate down time due to bugs. I still get nervous when I install to production. Always taking back up after back up and talking myself through the process of rebuilding from scratch. Just in case this time I have to. Would formal methods help with code at this level? I suspect the cost benefit isn't there. Though I wish it was. I've seen the difference between having tests and not having them. Development time decreases, and my stress levels decrease. Is this the same with formal methods?

subjectsigma 4y ago
I work in government contracting with very expensive and heavy pieces of metal that kill people if something goes wrong, and even I can't convince people they need to use formal methods to help write their code. So the easy answer is 'no'. That being said, FM is an enormous spectrum; if you squint a little, writing really good user stories could be considered a 'formal specification'. There's a really good paper from Amazon about model checking (Newcombe 2014 IIRC) where they make the bold statement that "Doing the math didn't help us find that many mistakes, nor did using the model checker; the thing that was most helpful was sitting down and forcing ourselves to come up with really good definitions. Like what does X really mean?" So it doesn't have to be as complicated as you think. So if you want to start as simple as possible, I would recommend something like this: https://www.hillelwayne.com/post/decision-table-patterns/ https://www.hillelwayne.com/post/decision-table-patterns/
- aeneasmackenzie 4y ago
  Leslie Lamport had an essay about this. Without a spec, even if it's just "Serves the user's homepage", your program is not even wrong.
- xupybd 4y ago
  Thanks! I'll have a read. Your comment helps clarify the situation.
  - rramadass 4y ago
    You may find https://markusvoelter.medium.com/the-evolution-of-decision-tables-80ce77bf984c https://markusvoelter.medium.com/the-evolution-of-decision-t... helpful. He also has a lot on DSLs which is worth reading. There is also a more powerful version of Decision Tables called Tabular Expressions (from D.L.Parnas) which you can use. A nice succinct reference to Formal Methods is Concise Guide to Formal Methods by Gerard O'Regan. I think simplified versions of Formal Methods can be used profitably for your use-cases. Start with Assertions, Design-by-Contract and Decision Tables.
quixoticaxolotl 4y ago
Formal methods will likely not help you - they can only show a _specification_ is sound, but not the _implementation_. That is, formal methods aren't testing the code you write, just the design concept behind it. For the design concepts you are likely to encounter in your situations, you absolutely do not need a formal proof that your stuff works - unless you are inventing (e.g.) a new cryptography suite from scratch or a large distributed system that must handle a massive amount of concurrency, there is zero advantage you would get over following best practices.
- quixoticaxolotl 4y ago
  If you are afraid of deploys, you need to lean into CI/CD and the whole DevOps movement more. That is the solution to being able to deploy without stressing about it.
- sangel 4y ago
  You can formally verify all the way to C, C#, Haskell, or even assembly if you use tools like Dafny, Coq, or Vale (for verified assembly). Several projects do this. It’s a lot of work for sure though.
  - quixoticaxolotl 4y ago
    Dafny is a really cool find, thank you!
- tluyben2 4y ago
  Idris 2 writes pretty quickly and you can prove the parts you want. It’s not blazingly fast but fast enough for many purposes and I definitely have far far less bugs and generally better code. Only for hobby projects so far but it is quite a brilliant. It is verified implementation.
- InefficientRed 4y ago
  > Formal methods will likely not help you - they can only show a _specification_ is sound, but not the _implementation_. I'm not sure where this idea came from. Are you in hardware? I guess in hardware that makes sense. Anyways, in software, formal methods can absolutely show that an implementation meets a specification. In fact, that has always been one of their canonical use cases in software systems, at least since the 70s or maybe early 80s. Formal methods can also be used with very ad hoc specifications, or with very general specifications, or increasingly without any explicitly specification at all (eg by inferring specifications). > cryptography suite from scratch or a large distributed system... Or aerospace software, or automotive software, or certain financial software, or industrial control systems, or any complex billing/access control, or... > there is zero advantage you would get over following best practices. I wrote a bunch of static analyses that checked for common configuration errors in Django apps which saved us many weekends. YMMV.
yakshaving_jgt 4y ago
I don’t think FM methods make economic sense in your case. They might if you were writing a distributed system, but writing some B2B websites probably means you’re best served with a monolithic system with both tests and types.

ncmncm 4y ago

Half would be damn good. Better would be solving the hard half.

dym_sh 4y ago
shrodinger's hard half – its always the one left unsolved

csours 4y ago

The longer I spend in IT/Software Dev, the more I see a dichotomy between Correctness and Usefulness. You can certainly have both, but different people concentrate on either correctness or usefulness. I think the future of software dev is people who understand both.

justahuman74 4y ago
The tools make it very hard to do both at the same time. To pick a topic, is there something I could write shell-style scripts in that leans towards correctness?
- csours 4y ago
  Correctness needs a specification. Correctness hates side effects. Shell type scripts are all about side effects.
- pharmakom 4y ago
  Yes! F# scripts Some features: - open-source - cross-platform - quick editing with syntax highlighting, type annotations etc. in VS Code - run in a single command (‘dotnet fsi script.fsx’) - type-safe but with global type inference - grab dependencies using directives in the script (no project manifests or global dependencies) The added safety of a typed language is fantastic for scripting because it’s not worth writing tests for most scripts.
- simonmic 4y ago
  Haskell (using https://docs.haskellstack.org/en/stable/GUIDE/#script-interpreter https://docs.haskellstack.org/en/stable/GUIDE/#script-interp...). The downside: requires 1. installing stack and 2. waiting for it to install ghc and libs on first run of the script.

SEJeff 4y ago

The architect of AWS and author of Dynamodb has very good thoughts on formal methods. They’re worth a read: https://perspectives.mvdirona.com/2014/07/challenges-in-designing-at-scale-formal-methods-in-building-robust-distributed-systems/ https://perspectives.mvdirona.com/2014/07/challenges-in-desi...

colmmacc 4y ago
Oh man, I really can't resist adding to the record a bit here. The author of the article - Marc Brooker - has worked (and led!) on formal methods at AWS and DynamoDB much more than James. The paper James linked to in his post was authored by ... Marc Brooker! so this comment just reads funny to me. Even though I know it wasn't intended that way. James isn't the architect of AWS either, the scale we're at and the way we organize ourselves mean we don't really have any single architects of anything. Also EC2, S3, SQS, and more were in place by the time James joined. But I'm not trying to talk down James, because James has been much more influential and important to AWS success than an architect! His technical and business insights, his vision and drive, and his focus on some really very key levers have been monumental drivers of AWS. I know I've learned a lot from him, and still do. He's so good at it that he's now on the Amazon leadership team, reporting directly to our CEO!
- SEJeff 4y ago
  Ah well you would know much better than me! I heard someone mention James as the architect of aws and recall him mentioning designing dynamodb. Did he do that, or am I universally wrong sans his love for formal methods? Thanks for the clarification though. This is truly why I enjoy HN so much. The ability to get corrected by the experts is an honor :)

mbrodersen 4y ago

Wow. Any solution that solves 50% of problems is pretty damn good!

westurner 4y ago

From "Discover and Prevent Linux Kernel Zero-Day Exploit Using Formal Verification" https://news.ycombinator.com/item?id=30194993 https://news.ycombinator.com/item?id=30194993 : > Can there still be side channel attacks in formally verified systems? Can e.g. TLA+ help with that at all? Side-channel attack https://en.wikipedia.org/wiki/Side-channel_attack https://en.wikipedia.org/wiki/Side-channel_attack

_vdpp 4y ago
Yes, there can still be side-channel and out-of-band attacks in FV systems. For example, pouring water into the server rack. That’s a cheeky example, but things like timing side-channels via speculative execution and cache hits wouldn’t be addressed by FV at the software level. I think there is some ongoing research for verifying software/hardware interactions but I’m not aware of a product in widespread use that checks this. The use of constant-time algorithms for crypto is a way to mitigate things like timing side-channels, and there are other techniques like disabling hyper-threading that can help. The depressing fact is that side channels exist any time there’s a shared computing resource. The question is how noisy the channel is, the data rate, etc.
- westurner 4y ago
  It might be argued that side channels exist whenever there is a shared channel; which is always, because plenoptic functions, wave function, air gap, ram bus mhz, nonlocal entanglement Category:Side-channel attacks https://en.wikipedia.org/wiki/Category:Side-channel_attacks https://en.wikipedia.org/wiki/Category:Side-channel_attacks

rurban 4y ago

I'm using better model checker tools, and they also only solve half of my problems. but all the tools together solve everything. https://blog.nubix.de/index.php/2022/04/06/testing-baremetal-firmware-at-nubix/ https://blog.nubix.de/index.php/2022/04/06/testing-baremetal...