This is exactly the right question to ask. I’ve been talking about this with a few people lately. I actually think it goes both ways. There are two challenges: ensuring the spec specifies a practical implementation, and ensuring the code correctly implements the spec. (1/?)
This was the first spec I’ve written that really encountered the first challenge. I initially modeled some operations in a single step that in the implementation would have been problematic as it would have required a mutex around a database (consensus) call.
So I had to refactor the spec to model the potential for the OS to reorder concurrent operations, and that change was critical as it exposed what would have been significant defects had the spec been implemented without the mutex, as it should (ideally) be.
The second challenge is ever present, and I wish I had a good solution for it. But in most cases I’ve found my implementations do become more complex than my specs because they’re constrained by libraries and semantics, making it more difficult to verify the impl is correct.
For example, this spec requires that cached entries be retained until the database has propagated events up to the entry version (logical time) to avoid reordering reads following an eviction. But the LRU cache library I used in the implementation doesn’t support that behavior.
The implementation uses a separate Go map to store recent entries that need to be retained in addition to the LRU cache for entries that can safely be evicted. These kinds of inevitabilities can make the eyeball test difficult, but the idea of an eyeball test is itself a problem.
In my recent conversations, one strategy I’ve seen for gaining confidence in the impl was doing Jepsen style verification of histories, which is an idea I like. Another suggestion was to simply keep the impl of the spec minimal, perhaps using a direct translation of the steps.
But all of these solutions still make me uneasy. Formal methods can only be used to create correct systems when they have correct implementations. And while we have the tools to gain confidence in a TLA+ spec, it’s not always easy to guarantee the implementation matches the spec.
I’m still in the process of updating the impl with the latest changes in the spec, but given the small size and complexity of the algorithm, I am confident I’ll be able to produce an implementation that’s consistent with the spec even considering the language/library limitations.
So maybe there is something to be said for limiting the scope of the spec and size of the impl. But that’s difficult with more complicated specs. And even with a limited scope, I’m still fallible. Without a verifiable programming language there’s always a risk I make an error.
