> I think it's fair to consider the entire binary a fair target.

Yes, it's still very much a bug. But it has nothing to do with your program being formally verified or not. Formal verification can do nothing about any unverified code you rely on. You would really need a formal verification of every piece of hardware, the operating system, the runtime, and your application code. Short of that, nobody should expect formal verification to ensure there are no bugs.

▲

appplication 4 hours ago | parent [-]

I read it as that’s also the point. Adding formal verification is not a strict defense against bugs. It is in a way similar to having 100% test coverage and finding bugs in your untested edge cases.

I don’t think the author is attempting to decry formal verification, but I think it a good message in the article everyone should keep in mind that safety is a larger, whole system process and bugs live in the cracks and interfaces.

▲

quantummagic 3 hours ago | parent [-]

You're right. It just seems as though it should be self-evident. Especially to those sophisticated enough to understand and employ formal verification.

▲

gopiandcode 2 hours ago | parent [-]

It does seem that way doesn't it? But as software bugs are becoming easier to find and exploit, I'm expecting more and more people, including those not "sophisticated enough" to understand and employ formal verification to start using it

	▲	quantummagic an hour ago \| parent [-]
		> I'm expecting more and more people Then it would help to not introduce any confusion into the ecosystem by using a click-baity title that implies you found a bug which violated the formal specification.