Hacker News Reader

Comment by xupybd | Hacker News Reader

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?

View on HN

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/

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.

Thanks! I'll have a read. Your comment helps clarify the situation.

You may find 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.

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.

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.

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.

Dafny is a really cool find, thank you!

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.

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

I'm in software.

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

To be clear, I'm talking about systems that go beyond simple property validation. Presumably, we're both talking about e.g. Ada SPARK, Alloy, TLA+, etc. I would hesitate to call a type system a formal method, for example, unless they use some notion of tactics like Idris, Coq and Lean do.

Now there certainly exist formal methods that can show that a program meets a given specification and conforms to certain desirable properties. However, they cannot show that the program is bug-free, because many properties of a formally-verified system may be relaxed in real environments. When I say "sound", I mean the property of being bug-free.

In OP's case, it would not help the OP reduce the frequency of bugs pushing to production - it would only give them confidence that they meet the spec, which is usually not what people writing internal tools are worried about. For industries where being safety-critical is not necessary, there is simply no meaningful advantage provided by formal methods over regression tests, clean refactoring and validators. While you can certainly use them, the benefits are slim.

> Or aerospace software, or automotive software, or certain financial software, or industrial control systems, or any complex billing/access control, or...

These are safety-critical industries, where things like temporal correctness, multiprocessor safety and other attributes matter - essentially, where you can model your system as process calculi and must demonstrate some invariants hold over the lifetime of the system given a specification. That is absolutely the domain of formal methods and where some formal verification is needed for certification. These industries are also the ones where you can ensure both certified hardware and software, so that formal verification actually does detect correctness bugs beyond what an integration test does.

But OP has not said they are in any of these industries, and I don't think it's incumbent on me to be exhaustive in listing them when it's not core to OP's question. If OP's asking this question online instead of their colleagues, we can safely infer they're likely not in an industry that demands formal certification already.

> Presumably, we're both talking about e.g. Ada SPARK, Alloy, TLA+, etc.

It's quite difficult to look at systems like Dafny or {J,C}BMC, in particular, and say "they can only show a _specification_ is sound, but not the _implementation_.", since those systems are definitely saying something about the implementation.

Regarding "soundness", I think you're confused about terminology. I have no idea what it would mean for a spec to be bug-free; that seems equivalent to saying that a program is bug-free. Specs can have bugs for the same reason that implementations can have bugs.

Anyways, "sound" has a well-understood meaning that is quite different from the one you're imposing. Soundness is a property of the entire system, not of individual formulas (specifications). A formal system/tool is sound if the system only admits proofs of a formula F whenever F is valid in the semantics.

> But OP has not said they are in any of these industries, and I don't think it's incumbent on me to be exhaustive in listing them when it's not core to OP's question.

You're missing the point, which are the ellipses.

OP's question is "are formal methods worth it for me?"

The appropriate answer has NOTHING to do with the type of code that OP is writing or their application domain. AWS components are not safety-critical in the sense of aircraft or automotive software, and they run on commodity hardware. Ditto for financial systems. But formal methods are applied successfully in both contexts.

Again, I've used hand-rolled formal methods for Django apps as part of our deploy process and it's definitely saved us headaches.

The implementation effort took very little time. A weekend and then a bit of ad hoc follow-up work. The rise of amazing parsers, really good implementation languages for this sort of code (scala, F#, ocaml), and fantastic SMT solvers (particularly string constraint solving) means that what used to require a "huge investment" can now be done in a weekend hackathon. Hardware is also making formal methods a cheaper prospect. Lately I've been playing with a small cluster of 64 core processors during off-hours and the amount of brute force search you can do in a weekend is pretty incredible.

Formal Methods are often cheap and easy to implement, but they do have a high up-front human capital cost/learning curve. You need to know how to coalesce a class of bugs into a mathematical description. And then how to check that mathematical description against code by hacking together parsers, AST rewrites, and SMT solvers. The idea that this takes months or years of even weeks of time is pretty dated. A learned hand can get a lot done in a weekend.

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.

Reply on news.ycombinator.com