3 ms·

> In order to really make good use of your hardware you need to understand your hardware and code accordingly Understanding your hardware is only half the stor

> In order to really make good use of your hardware you need to understand your hardware and code accordingly Understanding your hardware is only half the story. To use the hardware effectively, you also need to have mathemaitcal insights into your problem. A rather extreme proof of this fact is bubble_sort.c vs. quick_sort.java. I think it's clear which of those is using the machine more effectively... > I doubt you can achieve great performance on a language that focuses entirely on mathematical representations without considering the hardware. Plenty of very high level languages have extremely effective compilers. SQL query engines come to mind. > So yeah... you end up with a beautiful mathematical expression ... but runs way slower than an "ugly" equivalent in c code. TLA+ et al. are about primarily about correctness and designed for situations where correctness is hard to get. Beauty is relevant only in-so-far as it helps one the path to correctness. But yes, hand-craft code will get you your GIGO much faster :)

rixarn 8y ago
I agree, you need mathematical insight too you can have that and still code as we do now without sacrificing a way to express solutions that consider things such as cache locality. With what he proposes, that’s simply not possible. There’s a very interesting talk by scott meyers about how important cache locallity is to the point where, in practice, for some problems, big oh analysis breaks because of cache misses. So an algorithm that is faster by those standars gets its ass kicked by a “slower” one just because of cache misses.
- thrmsforbfast 8y ago
  > 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!

rixarn 8y ago

I agree, you need mathematical insight too you can have that and still code as we do now without sacrificing a way to express solutions that consider things such as cache locality. With what he proposes, that’s simply not possible. There’s a very interesting talk by scott meyers about how important cache locallity is to the point where, in practice, for some problems, big oh analysis breaks because of cache misses. So an algorithm that is faster by those standars gets its ass kicked by a “slower” one just because of cache misses.

thrmsforbfast 8y ago
> 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!