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