Hacker News Reader

The problem is that the subset of programs which can be proved to be correct (in 2015) is mostly restricted either to uninteresting problems, solved problems, or both.

View on HN

Not always true. For a trivial example, in fortran code, we'd often see people wanting to write code that calls runtime methods directly because it leads to clearer implementations. The language rules were such that we could prove invariants on these runtime calls that were much stronger and farther reaching than the general bitcode optimizer could do, resulting in a class of matrix operations going to n*lg(n) from n^3, and we could also switch the stride direction to make better use of cache because of the algorithm change. This sort of thing was only possible because language knowledge was exploited — generic optimizers will miss this stuff.

I think the future of languages like haskell are bright in terms of performance, because they are so loosey goosey with what gets evaluated when, which gives language-aware optimizers a lot of meat to chew. An aggressive optimizer could turn out versions of the same code that run screaming-fast single-threaded, or that fully exploit massive parallel machines, or even version for all of those.

Don't think of it at the program level.

Think of it at a smaller level.

Even optimizing, say, a single "trivial" function in a widely used library can have large effects overall.

Reply on news.ycombinator.com