[johnday]

It would massively simplify the job of proving the upper language more correct. It may also be possible to proxy the type system in order to make use of existing tooling.