Copying over what I said over on irlo for posterity:
1: No, and probably not for a while (unless someone pays people to make a macro attribute based system).
2: Unfortunately I’m not sure what this is asking. If my posit is correct and it’s related to a formal model/definition of the language, there doesn’t exist anything yet but we’re working on that. It’s far off but the groundwork is being laid as we consider the requisite hard questions as a community. For now, Rust is “what rustc does”, and everything else is non-normative.
3: This should be answered on the main website https://www.rust-lang.org. But Rust is an imperative language with functional leanings developed as a “systems language” but can be used effectively in any application domain, especially (but not in any way limited to) the 2018 “featured” areas of Command Line, WebAssembly, Networking, and Embedded.
Though I suppose it should be noted that
unsafe is in itself the developer taking on a proof burden. The Rust type system is strong, and
unsafe allows operations that the compiler can’t guarantee don’t break the type system and various other guarantees the compiler (and developer) rely on in safe code. Instead, the developer takes on the proof burden that
unsafe doesn’t cause memory safety or UB, and the compiler proves it for you in purely safe code. (Modulo compiler bugs because no software is perfect.)