The trouble we always encounter is, people *also* want the software to *do* something.

No one has figured out how to make software that always does the right thing, never does the wrong thing, and is still useful enough that people want it.

@stilgherrian

@bob_zim, I would bet money that no system which does something of interest to @stilgherrian has been formally verified to the complete degree you say.

Which is why my description includes the requirement that the software does something people are interested in. Yes, there might exist formally-verified systems with no detectable bugs; but likely that doesn't describe any system we directly use.

@bignose @bob_zim @stilgherrian though it sounds like curl is pretty dang close! (To being bug/vulnerability-free, and ubiquitously used)

Also assumes that the verification/validation process is flawlessly designed and executed to test all positive cases and all possible negative cases, and I’m gonna hazard a guess that that’s happened only on a handful of systems in the history of the world.

@shieldsy05 @bignose @stilgherrian The verification process involves building a mathematical proof that the software has all of the specified behaviors and has no undefined behaviors. It’s concrete proof of exact match. Writing a sufficiently detailed specification is difficult, of course, but there are tools to help.

It’s mostly worthwhile in the embedded space, industrial process control, and in situations where the hardware is exceptionally difficult to access to update (e.g, satellites). These things are widely deployed, though. This message definitely goes through at least four formally-verified OS kernels on its way to you.