5 ms·

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 bac

by 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.

by xupybd 4y ago

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.