Furthermore it's undoable in general. Equivalence of lambda terms being undecideable and so on. Point being, at some point functions become sufficiently diffe

Furthermore it's undoable in general. Equivalence of lambda terms being undecideable and so on. Point being, at some point functions become sufficiently different that it's hard to tell. What if you write one md5 function in Erlang, another in whatever that Ruby syntax for Erlang is called. I'm sure the Erlang they both generate, or bytecode, or what-have-you (I don't know how BEAM or HIPE work on the inside) are very different, to the point that checking that they are truly equivalent is going to be near-impossible, even for a very strictly defined program like MD5.