I don't think the authors are focused on engineering matters; they're researchers after all. But that's just my guess. Also, there is an obsession with covering

I don't think the authors are focused on engineering matters; they're researchers after all. But that's just my guess. Also, there is an obsession with covering the full λ-calculus, which the abstract algorithm doesn't. A lot of energy has been put in that. I think this is just wrong. Rust has severe limitations on how you can write lambdas. HVM has some, which seldom occur in practice. Regardless, some people did try implementing this in practice, dozens of times, including myself. It just wasn't that fast except for these cases where the asymptotics are superior. A naive implementation just stores graphs/edges on memory, but most of these edges are redundant. For example, a lambda doesn't need to point to its parent. By trying to turn the graph in a tree, I've ended up with SIC [0], which, once implemented efficiently, cut down memory and computation costs significantly. Doing so was tricky, specially because 1. the missing edges complicated the transversal; 2. some upward edges can't disappear (variables); 3. DUP nodes aren't part of expressions, they just "float", which was counter intuitive to get right. Finally, I learned to appreciate the fact that global rewrite rules are better than case-trees for recursive functions, since they greatly reduce the total rewrite count. So, in short, my journey was: 1. Learn the abstract algorithm 2. Implement it naively as a graph 3. Optimize it by making trees whenever possible 4. Favor rewrite equations over case-trees These steps lead to the design of HVM, which does fairly well in practice. [0] https://github.com/VictorTaelin/Symmetric-Interaction-Calculus https://github.com/VictorTaelin/Symmetric-Interaction-Calcul...