Not True.

Agile Dev (according to me) means you are trying to specify what the customer want as you develop your code and not specify it right in the beginning.

You can make changes to the specs when you are figuring things out. Also, you do verification when you are somewhat confident in your code is doing what the customer wants, so verification should come towards the end of your development phase (or at least end of developing parts of your code base).

You are right in general where the cost of failing is not that high, but consider software on flights, a pacemaker or (the best example everyone in FM quotes) a space mission. The cost of a small bug can cost you huge money/lifes. In these cases companies have an incentive to verify their code.

Hey you don't have to go to these special cases. Amazon, google, Microsoft all do Formal verification (or have started somewhat sophisticated testing) of their critical pieces of code as a bug in them even if it causes an hour of downtime will cost them in millions.

But most software is not on flights, pacemakers or space missions (or equivalent).

It's a cost benefit analysis, if the failure costs you more than verifying it then you will verify it. Since cost of verification is currently high, if you are not losing millions due to failure it doesn't make sense to verify your code.

Look at fuzzing. No one did fuzzing a decade ago. Since fuzzing became cheap (i.e. due to cheap compute and somewhat due to cloud computing) everyone does fuzzing on pieces of code which remotely appear to be critical.

Even testing. When cost of running a program was high people didn't write test cases. They hand checked programs for bugs.

Indeed, under those circumstances, yeah formal and semi-formal methods get used.

But since these circumstance aren't common [goto: very eloquent GP].

I didn't include it in the article because I wasn't 100% confident in saying so, but I'm reasonably sure that medical devices don't use FM. There's not a whole lot of oversight in that area, and most of the standards are (to my knowledge) about software process versus software methods.

Aviation also doesn't really use FM, but that's because they follow DO-178C, and that is a scary scary standard.

It would way cheaper for them to verify their code than to probably follow these standards but bureaucracies are bureaucracies.

Also, a little nitpicking in your write up but you should have also talked about type systems. They carry the spirit of formal methods but rather than being construct then check for correctness, are construction is correct by default. Type systems are widely accepted and show that some of these ideas can gain traction.

I haven't been anywhere near it, but DO-178C is allegedly friendly to formal methods; DO-333 is the formal methods supplement.

Adacore had a white paper, "Testing or Formal Verification: DO-178C Alternatives and Industrial Experience" that naturally I can't link because I'm on mobile.

I don't know how it's used in practice, but aviation companies dump a lot of money into formal methods research because getting their code certified to meet scary specs is very expensive and they don't want to do it for every bug fix.

The solution is to write partial specs.

For example, if your client wants a piece of code which doesn't crash and sends a message over the network. You can write 2 partial specs i.e. 1) it doesn't crash 2) it sends a message over the network.

The partial specs can be individually simple but the program which satisfies all of them will be complex.

This idea of partial specs follow the general SE design practices as well, where we describe fine grain tasks the program has to do (like when I click this button, this should happen).

Another trick is to create domain specific languages to specify certain kinds of specs. There is a DSL to write memory safety constaints and a special DSL to write Distributed coordination between machines. Each of the specs written in the respective DSL is easy to understand but a program written in general purpose language won't be.

Any message? Or a specific one?

I mean, at my work, a lot of our customers don't even know what our program needs to send to some other program until months after the change needs to be live...