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

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

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)1, 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.