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