Good day everyone I have a few questions about Rust.
Does rust support proof-carrying code if so how can I get information on it?
Where can I get information on Rust Operational/Axiomatic/Denotational semantics?
Where can I get information on its language paradigm and the application domain it serves?
I ask for a little help because I am not so versatile in these topics
(This question would probably be better served for users.rust-lang.org; it’s definitely not a language design post.)
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.)
There are also the RFCs in the rust-lang/rfcs repo. You should be careful there because some of them have been superseded by other RFCs or have not been implemented yet.