"one should program the most abysmally slow correct thing first and then use algebraic theories to transform it along obviously correct paths to something highl

"one should program the most abysmally slow correct thing first and then use algebraic theories to transform it along obviously correct paths to something highly performant." Except that the syntactic variance problem [1] makes this impossible to do in theory. Unfortunately so long we use Turing-equivalent computers there will be a need for "performance programmers" and low-level programming because we cannot automate their job by formal transformations from high-level, "obviously correct" programs (theory proves so). [1] http://dx.doi.org/10.1145/502175.502181 http://dx.doi.org/10.1145/502175.502181