The code in this file is pretty different from most of Iris, using a lot more automation and Ltac. If and when we are happy with the overall idea of merging an interpreter then we can figure out the naming and code style issues I'm sure this file has.
Much credit for the interpreter and proof strategy goes to Sydney Gibson, who wrote an interpreter for GooseLang that I basically back-ported to HeapLang.