> Some things are trivial to specify but hard to code. A hash table, for example. It's easy to specify what a hash table does, but that gives no guidance on how

> Some things are trivial to specify but hard to code. A hash table, for example. It's easy to specify what a hash table does, but that gives no guidance on how to implement one. You might get out something that does a linear search. File systems and databases are similarly not too hard to specify - the specification describes the abstract brute-force approach. One of the next steps for formally proven software development is automated analysis of algorithms. The same procedure to generate a proof of a correct implementation of a hash table could be extended to take an axiom of randomness (which would be an optimization the metaprogrammer could supply, breaking the true worst-case analysis based on their trust of the hash function and potential adversaries) for the hashing function in order to prove the amortized search/insertion time to be O(1) per element assuming the implementation is free to resize and rehash the table as it grows. The synthesizer could further search for implementations that minimize amortized/average cost using the available axioms and predicates, and benchmark them on a particular architecture much like JIT runtimes do now.