[lhousa]

I know it's just a google away but instead of sieving through all the resources out there can someone just ELI5

- where formal methods is actually used?

- is it a very specialised area of study?

- why is it needed?

- is it worth learning as a normal SWE?

[the-smug-one]

TLA+ has been used at Amazon for proving high-level properties of their distributed systems. Very useful, because a fix in prod for a protocol is very costly. ACL2 was used to prove some floating point architecture that AMD used a couple of decades ago haha. Github recently bought the formal methods company Semmle (something like that) for static analysis of repos.

Formal verification is used in critical software, airplanes and so on.

The most popular form of formal methods are type systems, which I would say a normal SWE should learn about and understand. It's not typically characterised as that, but a type system is a proof inscribed in the program for which we guarantee that some properties hold... Sounds pretty formal methodsy to me :-).

It's a specialised area of study, but isn't that the definition of an area of study performed at a university-level?

[Jhsto]

Having a two year masters degree on the subject, I can give a go:

- FAANG companies, top research universities, spinoffs of top research universities

- Yes and no. Yes because FM orbits around philosophical questions like correctness, soundness, etc., which are not usually thought in your normal web shop. No because it is fundamental CS i.e. generic.

- To prove properties, e.g. that a piece of software is bug-free. Usually this means things like reachability of states, which can be checked with e.g. TLA+. This may be a requirement in a critical system, where your normal support ticket could instead mean a death of someone. Asynchronous, distributed, and multi-core systems, which might be though to wrap your head around, might also be application areas.

- This is super opinionated, but I would say learn about SMT solvers and forget the rest. For me, it clicked with SavileRow. Constraint programming was much more like an AI to me than any actual AI, since I just described the constraints and my programs solved itself. This way, you will get used with propositional logic, which is then easier to extend into TLA+ and some partial formal verification tools which prove state-properties with propositional logic and Hoare-triples from generic software.

[YeGoblynQueenne]

>> Constraint programming was much more like an AI to me than any actual AI, since I just described the constraints and my programs solved itself.

Theorem proving and SAT solving are classic AI subjects, don't forget. If we don't think of them this way today that's the usual "if it works, it's not AI" paradox (it's got a name I think, but I don't remember it).

I'd go as far as to say that theorem proving is honest-to-god AI, much more so than pattern recognition. After all, we know many animals that can recognise sights and sounds, but we only know of one animal that can state and prove theorems.

[sitkack]

https://savilerow.cs.st-andrews.ac.uk/

[hwayne]

Formal Methods is a big field, and there's lots of different pieces with varying usefulness. I'm working on a bigger intro right now, but a couple years back I wrote an overview on why people don't use it: https://www.hillelwayne.com/post/why-dont-people-use-formal-...

Right now, I'd say that it is still a specialized area of study, and most normal SWEs don't need huge swathes of it. Sure, it might help you think better about problems, but lots things do that, too, and some are even directly useful! But there are still useful parts, like specifying abstract distributed systems, where it saves more in preemptive bugfixing than it costs in time spent. Disclaimer, I make money off teaching it, so of course I'm biased ¯\_(ツ)_/¯

[kibleopard]

Provable operating systems such as seL4, etc., used in mission critical scenarios utilize formal methods to effectively prove correctness of the system. Definitely a real-world use case. Worth knowing for a normal SWE? Probably not.

[Recursing]

There was a thread just yesterday with a bunch of practical examples https://news.ycombinator.com/item?id=27027522

[xiaq]

> where formal methods is actually used?

Formal methods are useful where the cost of bugs greatly exceed the cost of formal verification.

Most software systems do not fall into this category, but some do: space launches, transport safety systems, medical equipments and particle colliders are good examples. The LHC has several of its subsystems formally verified, for example.

[kqr]

Worth learning as a normal SWE? Heck yes, at least to some degree.

It makes you a lot better at writing understandable, modular, composable code with sensible abstraction boundaries. Also makes you better at writing tests. At least this was my experience.

[vardhanw]

Also, what, if any, are the pre-requisites of understanding them (formal methods, SAT/SMT solvers, theorem proving)?

[mcguire]

Honestly, the only specific thing I can think of is basic formal logic (predicate calculus, sets, functions, formal proofs, and so forth). (For ex: https://www.logicmatters.net/ifl/)

The specific technique may have something more, but generally any resources start by assuming you know nothing more than formal logic (if that) and build from there.

[mcguire]

Since everyone else is being optimistic, I'll jump in as the bitter, cynical, devil's advocate:

- To a first-order of approximation: nowhere. People mention an Amazon (research?) group using TLA+, there's AdaCore with GNAT, INRIA with Frama-C, various dependently-typed language groups, but in practice I have not heard of any extensive use of formal methods.

For example DO-178C (https://en.wikipedia.org/wiki/DO-178C), "Software Considerations in Airborne Systems and Equipment Certification", allows some formal methods in aviation software in addition to (but not replacing) testing. There's even a supplement, DO-333 (https://www.rtca.org/training/do-333-formal-methods-do-178c-...) for it.

- Yes and no. No, in the sense that I was introduced to it as an (early) undergrad and it forms a good chunk of my intuitions and how I think about some problems. On the other hand, I don't believe anyone still does that kind of thing, and formal methods have become a separate, diverging area of study, particularly if you are experienced and looking to add it to what you already know.

- By and large, it's not needed. The current technological culture does not apply any form of pressure to encourage the extra effort needed in general. There is some such pressure in some areas---like the Amazon TLA network protocol stuff (it's really hard to debug your way out of a bad network protocol :-))---but on the leading edge, innovation is preferred to reliability, and on the trailing edge, low price is. (In a sense, it's "move fast, break things" writ large.) Since the consequences of technical failures don't generally end up on the technical community's doorstep and major failures are management problems, the "need" for formal methods is entirely theoretical.

- By and large, no, in the sense that future earnings provide the value of your education. You would be much better rewarded spending the time learning some particular domain or more popular technologies.

Now, as I said, I grew up with formal methods and they are the base of how I think about things. Plus, they're just plain fun. (No, really, Coq (https://coq.inria.fr/) is the best computer game I've ever seen. And Frama-C is just brilliant, if you can get it working and are living within its constraints.) I've spent a lot of time and effort learning formal methods and I wouldn't do anything differently. But then, I have a lower long-term salary history than many of my peers. For what it's worth...

[dhekir]

A few corrections and counterpoints:

- Frama-C is developed by CEA (French nuclear research agency; Inria participated in the beginning of the project, and is still a partner, but development has always been led by CEA);

- Your first-order of approximation is a bit severe; there are formal methods groups within large companies, such as Airbus using Astrée, Frama-C, and CompCet; Framatome (French nuclear reactor business) using Astrée; EDF (French electrical company) using Frama-C; plus several railway companies using formal methods such as B; and NASA, Thales, Scania... It's peanuts compared to the amount of money being poured into blockchains, AI, and the latest hype, but formal methods are used in some industries.

Overall, I agree with you: it's not the best time investment for many SWEs, but if you like maths, formal methods do provide some satisfaction and long-term hope that we'll stop patching bugs and rewriting things all the time, and build some longer-lasting software.