Marc Schütz:
(How formal do we need to go?)
It's not just a matter of how much formal to go, but also a matter of how much D to formalize to avoid unwanted interactions (surprises) later.
But before going formal, you need to wait for comments from Walter & Andrei; and possibly also comments from a good Rust core developer, because they have discussed such topics in detail for lot of time :-)
Bye, bearophile
