That is not the hard part at all of formalizing a program spec on a file system. You just conditionalize your proof based on sane/desired usage of the file system.

The problem is even formalizing a file system at all. It is nearly impossible to even effectively prove something as simple as:

1. Program A creates a file, F, that only program A writes and writes some data.

2. Program B writes file G which correctly modifies untold amounts of arbitrary file system data structures.

3. Program A reads file F and sees the contents are unchanged.

If you could easily prove that for arbitrary programs that follow those very basic rules, then you would be able to formalize like 90% of file system usage.

The weaknesses and difficultys of formal methods are at a far, far lower level than people think.

▲

kodoman 2 days ago | parent [-]

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.

▲

Veserv 2 days ago | parent [-]

The model I suggested is intentionally as simple and trivial as possible to point out how we can not even reasonably solve the simplest and most trivial problems even if we get to just assume that complicated considerations do not apply.

You are doing the metaphorical equivalent of arguing how using antimatter for power is hard because we can not efficiently harness gamma rays when the harder and more immediate problem is that we do not have antimatter.

▲

kodoman 2 days ago | parent [-]

The problem is part of the domain of the program is the file system. It seems you agree with me in your previous point but only say that you don't want to consider it then claim it is fair easier.

My point is exactly file systems are the problem you layout as much, the thing is simpler models would not be. Consider a simple look up table with the key being a name and the content being a resizable array that the program can fork off to other processes by value and not reference (kind of like let binding in common lisp) this is much easier to reason about and simpler.

What you can not do is start with something as complex as a file system and then say 'I am going to draw up simplified model and just assume my program will behave as so' You have to show that your program will treat the more complex thing in a way such that you can draw a mapping between the the state of the file system and the simplified model.

I don't think this is just me being overly pedantic, if I just assume my simplified models apply I scarcely prove anything.

I am also saying the solution is to use something simpler then a file system (from an interface point of view).

▲

Veserv 2 days ago | parent [-]

A “simple” lookup table is also nearly impossible. Any “service” in another process more complex than a array pointing at non-moving data where the client interacts with it exclusively using integer handles is extremely hard and strains the limits of modern proof systems.

▲

kodoman 2 days ago | parent [-]

I am sorry it seems we have been talking past each other, you are talking about using SMT solvers and such, It took me a while to realize. I was speaking of Curry-Howard isomorphism style proofs using Coq and stuff. In the case of SMT solvers my suggestions are pointless but in the case of some kind of program as proof my suggestions are useful.

look up tables are not challenging to formally prove in Coq and they are well behaved monoids with respect to union, you can reason about insertion and deleting or modifying content, this is so much simpler then a file system. It does not matter if it's a hash table or binary tree underneath you can normalize an interface quite simply.

> Any “service” in another process.

Not what I meant by service, I was thinking about either a library implement this data structure and behavior guaranteed by forking, I meant it as in an operating system or runtime implementing a service. My point was just to show something that one can reason about quite easily.

> in another process more complex than a array pointing at non-moving data.

the suggestion was to forks so essentially clones the values of the table, this does not make a reference that was my point hence why I said it was kind of like a let bind. For fork think a simpler version of unix fork with various bits stripped. All I was trying to show is the sort of direction one could go with this sort of thing, this would be too simple to a lot of things but you can see the direction of travel, these primitives are easy to reason about.

I was not really wanting to go into parallelism or IPC (that stuff is more difficult but there exists primitives) rather the point of threads was that one can have a primitive of isolating code in it's own context, I said nothing about communication but you could indeed have many different strategies from the more simple waiting for a child thread to yield allowing you to use Virtual memory and helping you reason about the code and you could allow the thread to 'join' not a normal join but just a well defined function that takes a bit of the yielded threads code and puts it back into the called processes user space in a well defined way. The point is this allows for reasoning about values and passing values in a predictable well defined way.

> extremely hard and strains the limits of modern proof systems.

I realized at that point you where talking about SMT indeed this would not be useful to a developer wanting to use SMT, a program as proof style formal verification would benefit greatly from this sort of thing greatly Idris, Coq, etc. I am sorry I did not realize this earlier I should have realized as the topic of the article was not such proofs I apologize.

Additionally you are absolutely right that working with a SMT is easier then a lot of people think and beneficial.

▲

Veserv 2 days ago | parent [-]

Yes, a dynamic sized hash table is hard to prove unless you just take it axiomatically.

How are you demonstrating that Insert(“Alice”, True) followed by Insert(“John”, True) does not result in memory stores that cause Get(“Alice”) to not return True? Or result in Get(“Blorg”) giving a different value?

How are you proving that you can lift this generically so you can reason about non-interference considering only the abstract interface? So you can generically reason that Insert(x, _) allows you to continue to assume that Get(y) is unchanged if x != y even in the presence of dynamic resizing and copying of the underlying data in a hash table implementation? How are you proving that about the keys the leaf piece of code does not even know about even though it may have changed the memory locations previously used in the Get(unknown y) calculation?

How are you proving that no other operation violates that abstract data model and can thus be ignored for the purposes of your proof? And as a corollary, how do your proofs start failing if a violating operation is added?

Sure, if you just assume you have a magical key-value map that does not interact with the concrete data model, then life is easy because you skipped the hard part. Being able to easily encapsulate a data model into a higher-abstraction data model is the thing that is largely missing. It is why formal proofs generally stop in the low hundreds of lines proving a single data structure and its operations.

Building and proving you implement usable abstractions that can be reasoned about by your proof system at the abstract level is extremely hard with current systems.

	▲	kodoman 2 days ago \| parent [-]
		> Being able to easily encapsulate a data model into a higher-abstraction data model is the thing that is largely missing. True for SMT not true for curry-howard. > unless you just take it axiomatically If you remember that was basically the original point, I was saying that the file system interface (even if assumed correct) there is very little that can be said about it or proved about what you program is doing and you agreed. > a dynamic sized hash table is hard to prove There are two parts to this memory allocation is hard in curry howard but hash tables are not. What is easy in curry-howard is linked data structures so once you prove various features of memory allocation and you can build linked lists and such with it you are good to go. This would be fairly challenging but only has to be done once by the runtime/operating system implementation. > (Paraphrasing) hash tables are hard They are not particularly hard in curry-howard. I can give you a rough idea of how you would do it but their is examples you can find online In Idris or Coq, etc. Once again this could be done prior by the runtime. > this is hard Yes curry-howard proofs are hard and can be even hard to make performant programs, but it can be done and for the case of the operating system service's (features, system calls, drivers, etc) this can be done as a massive project (see sel4 for only a l4 based micro kernel). My only point was that if one wants this sort of proof going beyond what you can do in z3 then this is what you have to do and one of the issues is the abstractions operating system services use, that is not actually a particularly disputed point.