For the first thing you're talking about check out bend.

https://github.com/bendlang/bend

Bend is a formal language, but its use is quite different (also, Bend is much too narrow for Maxwell's use case...).

We need proofs of equivalence (including for code with side effects!) between original code, and new code, possibly in some other language. Say Python and a raw SIMD implementation. To do this we have a full 'embedding' of said languages in the same formal framework. It also requires modeling exactly what 'state' means in dynamic high level languages.

Thanks!