Since you posted this comment, we've seen a very interesting article on formal languages and 'program proving compilers based on separation logic'. The basis for truly correct, reusable, "eternal code" is in fact to regress to something not unlike ASM but combined with a Rust-like higher level.

Always good to remain mindful that what we assume is 'progress' in one direction may not be progress overall, and that allowing backtracking to older interpretations is actually a more mature scientific stance.

[1] https://news.ycombinator.com/item?id=31543953