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.

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