Just watched the talk. The technique the author's discovered is called "supercompilation" (note: this is distinct from "superoptimisation", mentioned in sibling

Just watched the talk. The technique the author's discovered is called "supercompilation" (note: this is distinct from "superoptimisation", mentioned in sibling comments). The idea is to use an evaluation strategy which works at compile time, reducing statically-known expressions whilst shuffling around unknown values symbolically to preserve the semantics. The result ends up folding constants, inlining, unrolling, etc. automatically, just like the examples in the talk. Whilst supercompilation can be slow, the main criticism is that resulting code is quite large, due to the amount of inlining. The main difference between supercompilers and the technique discussed in the talk is that supercompilation is provably correct: it doesn't rely on testing or placing exhaustiveness requirements on the user. I don't think it's necessary to sacrifice correctness; the speaker mentioned the use of guards in JITs, and how he avoids them for speed, but I think that since we're performing such extensive rewriting of the code anyway, many redundant guards can be supercompiled-away, and those remaining can be shunted to the start of the program, so that no branches appear in the hot path. The allusions to the scientific method seem to be about properties/invariants, and potential counterexamples to them. I'm all for finding and sharing properties of programs, both conjectured and proven, although I don't like the idea of assuming the conjectures are true. I've looked into this in Haskell, and found some great work, including: - QuickSpec (v1 https://hackage.haskell.org/package/quickspec https://hackage.haskell.org/package/quickspec and v2 https://github.com/nick8325/quickspec https://github.com/nick8325/quickspec ) which conjectures equations about functions by testing them on random inputs. - HipSpec ( https://github.com/danr/hipspec https://github.com/danr/hipspec ) which does the same as QuickSpec, but automatically proves the equations so they're guaranteed to hold. - The GHC compiler's rewrite rule system ( https://wiki.haskell.org/GHC/Using_rules https://wiki.haskell.org/GHC/Using_rules ) which allows programs to be optimised by replacing regular definitions with optimised versions in particular cases. This is how "fusion" and "deforestation" optimisations are implemented, e.g. https://donsbot.wordpress.com/2010/02/26/fusion-makes-functional-programming-fun https://donsbot.wordpress.com/2010/02/26/fusion-makes-functi... I think there's definitely some low-hanging fruit there, for finding equivalent expressions, comparing their performance, and generating a list of rewrite rules which the programmer may want to consider adding to their code. A slightly more ambitious project would use equations/properties about the program to generate a specialised supercompiler (maybe using something like a variant of knuth-bendix completion, ordered such that the normal forms are the higher-performing variants).