A challenge in high-reliability software is that the systems they are running on top of have few reliable properties. Even if you formally verify some code, you have to write vastly more code to deal with the possibility that the invariants suddenly change at runtime due to an idiosyncratic failure of the environment where that formally verified code runs.

This is one of the real limits of formal verification. Defects or subtle inconsistencies in hardware are not that uncommon. This is mitigated to a some extent by using assertions in release builds but this has significant limitations.

▲

pydry 2 days ago | parent | next [-]

yeah, I find when I write most software and am careful with testing that most of the bugs break down like this:

* 49% : specification error - wrong thing built in the right way

* 49% : bug involving something the software integrates with (e.g. 3rd party library, UI, database, API endpoint)

* 2% : code bugs

formal verification won't eliminate that 2%. it might get it down to 1%. there are still two enormous elephants in the room.

this is why everyone talks about it and nobody does it.

	▲	skydhash 2 days ago \| parent [-]
		> * 49% : specification error - wrong thing built in the right way This is why experienced devs says they spent half their time trying to get concrete requirements. You don't need to code something to know that the change request is incomplete and need more details. > * 49% : bug involving something the software integrates with (e.g. 3rd party library, UI, database, API endpoint) That's the reason there's a lot of books written about architecture and the necessity to push the dependencies to the edges of your code. Easy to patch stuff that way. > * 2% : code bugs With good tests, you can get this down quite low.

▲

kodoman 2 days ago | parent | prev [-]

> A challenge in high-reliability software is that the systems they are running on top of have few reliable properties.

I don't dispute this, and is infact related directly to my point, it seems that people are reading my comment as formal verification is a Panacea, I was only trying to point out that are primitives and abstractions provided by operating systems as well as programming languages are one major area that stops one from writing a formal spec.

Real formal verification is very very hard.

You do seem to miss the point that I am saying many of these subtle inconsistencies can be still complex but encoded into a formal model and I was showing how the file system abstraction adds it's own complexities.

Operating systems probably would be one thing that could be a massive project to undertake but would be worth it. We already have a formally verified micro kernel sel4 that proves lots of useful features and as you point out hardware issues an important thing at this level of correctness and sel4 simply assumes certain models for this.

▲

skydhash 2 days ago | parent | next [-]

> Operating systems probably would be one thing that could be a massive project to undertake but would be worth it

I don't think so. Even if you take small embedded project, there's a lot of unreliability that could creep in. You're not really sure what you got from a sensor is good or noise. Which is why you got all those error checking and ack in the protocols. You can make assumptions and try to verify your own code, but that's only if it brings enough benefits (mostly give you a clear sense of how likely something could go wrong). And that holds only for one version of the software.

You can do reliability study on hardware because it stays mostly in one configuration. But all bets are off if you're constantly modifying stuff inside.

	▲	kodoman 2 days ago \| parent [-]
		The example you gave is maybe one of the ones where this is least applicable. For systems with MMU's one would tend to use microkernels (like sel4) and then write driver servers for different components and the driver servers should be where hardware errors are handled. sel4 is only for systems with MMU and it's pointless outside of it.

▲

js8 2 days ago | parent | prev [-]

Regarding formally verified OSes, IIRC an early version of CICS (what we would call application server today) has been formally verified in the 1980s.