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