[infruset]

That's exactly what Tezos [1] is proposing: a strongly typed language whose semantics is currently being formalized in the Coq theorem prover.

[1]: https://tezos.com/pages/tech.html