> 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.

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.

There is also my very much related open source product that takes a practical approach, and is inspired by this research. Kind of a modern equivalent for Transaction Processing monitors that mainframes use, based on transactional, hierarchical state machines. It has built-in verification system. Not tested under production use yet.

https://voucha.net

Capsicum was an amazing project. I am not familiar with where it is at the moment and not freeBSD user (though looks more and more tempting) and I thought a lot of it went largely unused, if you have any links on how they built stuff around it I would be very interested.

> OpenBSD pledge+unveil This was one of those things that now seem obvious, and is elegant albeit in that unixy way. From what I can tell one could built something on linux with seccomp or openbsds pledge to implement a runtime that could allow for implementing such structures all in usersapce not just process isolation but creating IPC that allows for determinism and other things. (I think it's more seccomp with filtering syscalls though where this becomes feasible I don't know if anyone has done this before)

My point was that file systems don't lend themselves to being able to easily reason about in such a way. I used to try and illustrate how many considerations have to be made when interacting with these sort of operating system services and when deploying the program you need to make sure the assumptions hold.

The sort of model you suggested does not map every possible state of the file system to a model state structure so one could have various problems with results of the proof.

I guess the difficulty of formal methods depends on how much and what you want to prove, there is no real formal definition as to when something becomes formal methods is a spectrum and includes algo/c type type systems to CoC proofs and extracted programs.

You start by defining a loss function.

for example here was how some design rules got formalized into a checker during a video editing session of several hours: https://github.com/emberian/vidbox/blob/dev/render/drc.py

I mean would you take that spec as something you could deliver? This is not a real problem spec and is incredibly vague, but the first question would be around building a formal model for the drawing part of the application (and is the main aspect of the program) that might be easier then it first seems. There are various ways you could model the draw window depending on if it's a rasterizing program or a vector program either way not challenging, then formalize the operations of the program (various effects will necessary be well defined mathematical functions in the first place) and then prove what ever you feel you have to prove about the system. This is not to say it is easy or especially in this case you should even do it and my point was more about the system aspect of things or things that one would want to be able to reason about.

An example of a spread sheet program might have been more productive example or a http API server or some kind of middle where program. I feel like you picked the most obtuse example possible even though my point was not to cover all possible programs that one might want to write.

Inductively, in which case data labels are the spec and having good data is still the hardest part ;-)

> type systems Indeed types systems are usually the way formal verification is done, I am not denying that. The problem I am claiming is not the tools of formal verification but the domain one has to model and capture.

What I was trying to show is the nightmare of modeling accurately and in a way that matters lots of operating system primitives and further reasoning about when the assumptions have been violated by the program set up.

Indeed this does not effect the stuff outside the interaction of the program with the operating system and my point when it came to modern programming primitives is that not all data structures or methods of programming lend themselves to being able to write formal proofs about them.

You might be able to have a type BigInterfaceTypeThatDoesLotsOfThings<a> but this might be impossible to formalize in any meaningful way and AI is not the panacea and this stuff is not easy and require hard thinking.

Additionally a lot of formally verified programs are done via constructive proofs where you build up the correct program from primitives and extract the program and prove it that way. This requires generally requires a type system that has a complete inference algorithm like ML type-systems and are much harder to work with and you have to set up knowing you want to do this sort of thing.

Capability systems indeed make a lot of sense for operating system level constraints and I agree this is a sensible direction and combined with type systems you can build some very powerful permission systems. But these do not solve formally verifying lots of behaviors and good capability system in my opinion (and something I worked on previous as a side project that is completely unfinished and abandoned.) need mathematical primitives and structures that lend themselves to proofs and being restricted by capabilities.

Note capabilities become a program themselves and types can become programs, so getting your types right has the same issues in the first place when talking about this level of formalization.