I've been practicing a bit TLA+ and one idea I've encountered—which I agree with— is: if we can't even get the idea to work, can we ever hope to get a working i

I've been practicing a bit TLA+ and one idea I've encountered—which I agree with— is: if we can't even get the idea to work, can we ever hope to get a working implementation? And similarly: if we have a good idea about how the idea works, then perhaps it is easy to end up with a good implementation. But the situation is of course completely different when you already have an implementation and you want to get "the simple idea" of how it works. And a lot of things you're going to interact with are those existing implementations, not just ideas of them.