High-level requirements for a Proof of "Saving to the Database"

Question

This question is about a few sentence description of what a proof would look like (and technologies / logics involved) for a complex api call through many layers. Trying to get a sense of the techniques and key points to watch out for. I understand it would take a lot of work.

In learning about formal proof and verification, I've come across Operational Semantics, Hoare Logic, and Matching Reachability Logic. All of them are pretty low-level and describe how to prove stuff such as a while loop with a few assignment / arithmetic operations, but that's it.

I am wondering what the general / high-level requirements are to prove something like "saving a record through some https API to the database", where it goes through the network (https) and through a bunch of servers finally arriving at an array of replicated databases like MySQL.

In unit testing, you would simply write a test that the method (let's say save()) creates the record. You would make a database query and see if the record matched the record you thought it would be.

I am wondering what it would entail to write a proof of this (at a high level, just a few sentence description is all). What things would need to be proven. If you can't write a proof, then what if you still wanted to at least partially prove the system's correctness. What it would take.

It seems like you could write a Hoare Logic statement such as:

{P}
save({ type: 'asdf', foo: 'bar', a: 'b' })
{fetch('asdf', 'latest') == { type: 'asdf', foo: 'bar', a: 'b' }}

That's at least better than nothing. But I'm not sure if you can write a proof with just that.

Then to know that it actually was in the database and not in some cache in the browser, you would have to know that fetch had a proof that it went through the network to some API, and that API request went to the database, and the database did whatever. That's basically what I'm wondering, if creating a proof for save starts off with the Hoare Logic statement like above, and then progressively you add more detail to the proof. In this way it's almost developed like via TDD. At some point, then, I'm wondering when you could say "it is proven".

Answer 1

The SoftwareEngineering.SE link gives the wrong answer for the right reasons. You can only ever prove anything with respect to a formal model. Verifying that that formal model accurately captures reality (or at least accurately captures the parts you care about for your purposes) is an informal process. In many applications of formal methods, one of the most time consuming and difficult parts is creating and validating the formal model. For example, for the CompCert project they had to make both a formal model for the behavior of C and a formal model for the behavior of the target processor (at least for the instructions they use). Both of these are massive undertakings on their own.

It makes no sense to "add more detail to the proof". Either a statement has a proof or it doesn't. It's proven if it has a proof. All proofs are equivalent for this purpose. What you can add more detail to is the formal model. Except "add more detail to" has the wrong connotations. You generally want the least detailed model that is accurate and for which you can prove your desired properties, e.g. correctness. The only reasons to change to a more detailed model is 1) you can't actually prove what you want with the original model, 2) the original model is wrong in which case your new model is not compatible with it, or 3) which is really a variant of (1), there is a different program that you could write that exploits those details to achieve the same functional behavior but different non-functional properties such as performance or implementation simplicity. In all these cases we need a new proof because we've changed the statement we're proving: either by changing the program or by changing the assumptions.

There are two aspects to the use of a formal model. First, as far as your program is concerned, it doesn't care if the database saves the data or even if the database exists. It only cares that the operations it uses behave as specified with respect to a given formal model. That formal model can be very high-level and abstract with no reference to any notion of "database" or "network" or "HTTP". However, it will likely be quite complicated to soundly capture the realities of the actual underlying systems. Second, at the systems level, you certainly do care whether the data was committed to the database as opposed to just being stored in some local cache. At the level of the program, there is absolutely no way for you to guarantee this. Your program could always be running in a sandbox that mimics any observable behavior. All you can prove at the program level is that your program will invoke some sequence of operations that putatively will lead to data being committed to the database. At some point you just have to accept based on empirical evidence that the chosen real world implementation faithfully implements the formal model. You can provide an implementation of the primitives of a high-level model with respect to a lower-level formal model that has been proven correct if you want to reduce how much you need to accept without (mathematical) proof.

The current state of play is that most programming languages lack publically available, normative (mechanized!) formal models let alone the underlying hardware. Ipso facto, most standard libraries, applications, operating systems, drivers, etc. are not proven correct since they have nothing with respect to prove their correctness. This is both in the sense that there isn't a formal model of what "correct" even means, nor is there a formal model of the implementation language so that you know what the implementations even do. In other words, in most cases we neither know what an implementation does nor what we even want it to do. This is why the artifacts (and tooling) produced by the CompCert projects and its related projects and by the $\mathbb K$ framework folks and several other groups are so important. Without these artifacts, you either use some massively over-simplified and weakly verified formal model that implicitly assumes millions of lines of codes are "correct" (spoiler: they aren't)¹, or you invest man-centuries building a chain of trust. With luck, in the near-ish future some critical mass of formalization will be reached and proving the correctness of your program will become proportional to the complexity of your program and not the entire ecosystem.

¹ While using an oversimplified formal model doesn't provide most of the benefits of "provable correctness", it does, in practice, do an excellent job of improving code quality by revealing mistaken assumptions in the code. Of course, the mistaken assumptions in your formal model have to be detected the old-fashioned way for the most part.