Believe me, I see the appeal, but it's kind of like demanding your house have all perfect right angles and completely level surfaces. Living with manageable imperfection is far more realistic.
You don't have to make sure all the angles of your house are perfect right angles, but there's probably a couple that really have to be. Formally verify those and live with manageable imperfection for the rest.
Here's one example:
developer: adding proposed feature A to API B may result in displaying inconsistent data to the customer, in this kind of situation <details>
team owning service of API B, some weeks later: thank you for flagging that. we have thought about this, and propose a slightly different API design B'. let's meet to discuss.
product owner: the scenario that would trigger that situation requires a combination of unusual events: it has to coincide with a scheduled batch process, and the customer would need have unusual characteristics that are rather different from the distribution we observe. When the defect happens, the impact to the customer and our business is not so bad.
developer: That's fair. given how the feature works there are many other ways it can show inaccurate data to the customer as well.
engineering manager: how about we don't fix it, does anyone disagree?
everyone agrees not to fix it
A more interesting question is to ask "in which business situations does it make sense for formal verification to be used?". If you want to get paid to play with formal verification in the day job, you'd best find a business context where it is business critical to identify and remove design and implementation defects early, and it is worth spending a lot of money trying complementary techniques for doing so.
For my above example:
- the defect is not related to a core capability of the product. if it occurs, the defect does not cause a huge impact to the customer or the business. it may mildly annoy the customer.
- how the feature works is fairly ill-defined anyway, there are many things that influence it, and it's job isn't to preserve customer data, so data integrity isn't a huge priority
- if the defect did start causing substantial problems in future, it would be possible to change this decision and decide to fix it. the cost of fixing it later might be 5x fixing it now, but it wouldn't e.g. require a product recall or risk bankrupting the company.
There's a mental unburdening when you can just say "situation X won't happen".
tangentially, re: organising things to reduce cognitive load, there is an interesting discussion with the authors of the book "team topologies" who characterise the purpose of platform teams as existing to _reduce the cognitive load of stream-aligned teams_ (who have the goal of providing a user-facing service or product, say). https://www.infoq.com/podcasts/software-architecture-team-to...
Do you have any reason to believe that all the rest of the verification theory is completely impractical when every piece that was packaged in a usable context became a hit?
Full formal verification is (probably?) still a long way off, depending on your definition of "full". (My definition would be one where Knuth's observation that "it's amazing how many bugs there can be in a formally verified program" is no longer true.)
I have no reason why any of them could not be successful. I don't expect all of them to be, but anyone that gets there is already a huge advance.
Yes indeed. That is insightful.
Is there a name for this process?
We're probably never going to cure cancer - that is, have some treatment that conquers all cancers. Instead, we get "for this specific type of cancer, for these specific conditions, this treatment has a higher survival rate than the ones we had before". Over time, that adds up to a lot of people living out their days rather than dying early.
And maybe software verification is the same. Enough ways of verifying specific aspects of software, and bugs have fewer places to hide. It won't find all bugs, but we'll still get better software.
But "X can never succeed" isn't a very catchy phrase. Can anyone coin a better one? (Or, is there already a better one that I don't know about?)
While I am by no means have enough knowledge to claim such, but let’s just add that ordinary types are a so-called “trivial property”. Many, actually interesting properties can’t be proved as per Rice’s theorem in every case.
This tool does the former, leaving the latter up to humans.
I suspect eventually there will be a big lawsuit where the blame can be laid on negligence in the software development and the incentives might change somewhat.
You might be inclined to suggest that that could have been prevented if only they'd used formal methods. Perhaps that's true. It's something that could have been prevented in many different ways, though. Yet it still happened.
And yet, there almost certainly were lawsuits. So maybe you found evidence that perfectly counters my theory. It changed software, but only a little bit. Very little, given the magnitude of what happened.
There seems to have been something akin to an "accident chain", where a large number of things went wrong. Had any one of these things not happened, there might have been much less harm caused, or even no harm at all.
I will admit to being peevish about stuff like this. Some of the failures with Therac-25 were systems failures that had nothing to do with software per se (I'm not counting "software hubris" as a software problem). They were failures of process, problems with hardware interlocks, and even UI bugs that made the software confusing to operators.
I have nothing against formal methods, but they're no substitute for a deep and abiding paranoia.
I'd argue that, if there was going to be a needle-mover lawsuit, it would have happened by now. Until there is evidence that it will happen, we can continue assuming that it won't.
"Perceived"?
It's very rare that shipping later because of $quality-concerns is profitable. In most cases, that "later" never arrives anyway.
It may already be. Where's the research? It may not be happening just because of quarterly cycles, other misaligned incentives, culture or all kinds of other reasons.
> Believe me, I see the appeal, but it's kind of like demanding your house have all perfect right angles and completely level surfaces. Living with manageable imperfection is far more realistic.
The difference is that those things are all within tolerances and serve their purposes and function correctly. Software often doesn't.
And yet the world keeps turning, tech companies keep profiting, and customers are generally happy with the value provided, all without formally provable code bases. How does "provably correct" improve on this without extending timelines and costing more?
Obviously the answer is that they could profit more and be happier.
Ever heard of this thing called ransomware, for example? Identity theft? And you must know, this stuff is only the beginning... Just wait until the day everyone's private Facebook chats are available on torrent.
Software can still be provably correct and have security holes resulting from an insecure definition of "correct." Formal verification does not solve security.
>Obviously the answer is that they could profit more and be happier.
Please explain how a company could profit more if formal verification does not bring more revenue than it costs? You seem to be assuming that revenue will appear that is greater than the costs. Where is this revenue coming from, exactly?
Nirvana fallacy. The point is that it can be much better and eliminate ALL non-design bugs.
> Please explain how a company could profit more if formal verification does not bring more revenue than it costs? You seem to be assuming that revenue will appear that is greater than the costs. Where is this revenue coming from, exactly?
The revenue could come from savings on fixing bugs, paying for ransomed assets and all other costs that come from bugs. You're just assuming that doesn't add up and that there's no other reason that we don't do formal verification. That's just stupid. Show me the studies. Your claim is just as strong as the claim you think I'm making, but you missed my point entirely.
Serious question: do you really believe that?
> That's just stupid. Show me the studies.
There is a kind of HAL-9000 quality to many of these arguments. Formal verification is perfect by definition. The fact that it hasn't had very much impact in the real world is all the more evidence of the world being full of wicked people.
I mean it's a fact, so yes. You can prove programs are correct. The only possible flaw they can have is the specification is wrong.
> The fact that it hasn't had very much impact in the real world is all the more evidence of the world being full of wicked people.
That's very much not what I said. There may be many reasons. Assuming some conclusion without actual research is braindead. Cost-benefit analysis is not the only reason things do/don't happen in businesses and we have no idea whether that's the reason here. It's an empirical question that requires actual research, not a priori jacking off.
So specifications are kind of like programs?
Have you heard of logical positivism?
> That's very much not what I said. There may be many reasons.
My point was that it always seems to be some external factor. That strikes me as being very convenient.
> Assuming some conclusion without actual research is braindead.
I didn't think I assumed anything. Like anybody else, I have many things that I need to assess in my day to day life, and often deal with considerable uncertainty.
Formal verification shines in two situations: complicated optimized algorithms with a naive reference implementation you want to confirm equivalent, and high-level behavioral invariants of complex systems (like seL4's capability system, or a cluster database's consistency during literally all possible failover scenarios).
I'm guessing you know this but in type theories like Agda you can just specify that the input and output to an algorithm has the desired properties, rather than needing to specify any reference algorithms. For example, you can just state that an implementation takes a list of X and that it outputs a sorted list of X. Nothing more is necessary in cases like that in such a system, no code, just the single type.
And the reference for "sorting" could likely be a deterministic bogosort and certainly a primitive bubblesort.
Even if you're just looking at sorting stability, you're past what your simple "sorted" type would cover.
Most things are far less trivial than "sorted list", including (almost?) all interesting practical applications of formal verification in the life of a "normal" software engineer.
Don't confuse resignation and ignorance with happiness. People are used to computer systems just breaking and being the root of various problems (e.g., identity theft, privacy leaks, systems that just don't work some days for no apparent reason, and so on). The fact that they accept this flaky and unreliable state as the status quo doesn't mean they're happy with it - they just don't understand that better is actually possible.
I work in the security and assurance world. The biggest obstacle we face isn't technical - it's social. Developers want the route of least effort and least time to get products to market, and end users are largely ignorant of the fact that the world doesn't have to be full of garbage software. At this point, I'm rooting for a massive change in the legal landscape to start treating software defects the way we do engineering defects in physical systems. Developers and businesses aren't going to do the right thing by choice, so a giant hammer in the form of the legal system is likely to be the only thing to force change. I am fully aware of the consequences of that (e.g., it will likely severely chill open source, and will likely slow many business sectors down) - and I accept this. I'd take those consequences for the safety/security/assurance outcomes, even if they cause havoc on the revenue/business side and make "10x" python hackers grumpy. People will likely take formal assurance methods more seriously when there are actual consequences to deploying unsafe/insecure systems.