> With what he proposes, that’s simply not possible There's nothing special about the cache hierarchy. It's just one more thing that can be reasoned about usin

> With what he proposes, that’s simply not possible There's nothing special about the cache hierarchy. It's just one more thing that can be reasoned about using mathematics. If you care about cache locality, you can write down the semantics of an optimizing compiler and prove that this compiler uses the cache hierarchy in an optimal way. Why would that be impossible? Not only is it possible, but it might even be easier in high-level languages. For example, the argument has even been made that the importance of cache locality is really an argument in favor of higher-level functional languages. But again, with respect to TLA+, this is all a red herring and completely misses the point. The more important point re: TLA+ is the GIGO/correctness problem. I don't give a damn how cache-efficient my algorithm is if it's not even computing the correct results!