> A caveat of this technique for reducing lambdas is that it doesn't exactly match the behavior of the normal lambda calculus. While it might reduce the same as the normal lambda calculus in many cases, it doesn't always. And that's totally fine, it doesn't need to match perfectly to be useful in it's own right.<p>This seems like a serious problem for something trying to be so foundational... I'm kind of surprused the author doesn't go into more detail about it. Why is this fine? If not for evaluating arbitrary programs, what is HVM useful for?