Asking for Information on Rust

[GreatBowen]

Good day everyone I have a few questions about Rust.

1. Does rust support proof-carrying code if so how can I get information on it?
2. Where can I get information on Rust Operational/Axiomatic/Denotational semantics?
3. 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

[nakacristo]

Hello there.

Regarding item 1. This question suggests me that you come from some proof assistant environment, e.g. Coq, where functions can return and/or accept as argument proofs. Although Rust has some similarities with Coq, this proof-processing cannot be done in current Rust. I think the biggest impediments are

• There is a special type ! in Rust similar to False in Coq. And you can make a function Fn()->! by using panics, infinite loops, or infinite recursion. In proof territory this would mean a proof of False. Hence, to have a consistent logic, we would require to limit the potential (Turing-completeness) of the involved functions. One could think about some annotation meaning the function always terminates. I remember discussing something related, although perhaps it was on the internals forum.
• There are not dependent types nor functions returning types. This makes impossible to write things like (x=y) -> (forall P:T->Prop, P x -> P y). Which would correspond in some theoretical extension of Rust to something as Fn(proof:(x=y))->(Fn(P:(Fn(T)->bool),P(x))->P(y)). In Rust you cannot use one argument variable in the type of the following arguments.

I feel the information about item 2 to be a little diluted in the manuals. One option is to check the grammar itself.

The item 3 should be clear upon inspection of the main page of rust-lang. They highlight performance, reliability and productivity.

It would help if you were able to make more specific questions. Are you planning on use it for some project? Is it just theoretical interest?

EDIT: Perhaps I have misunderstood you in item 1. The result of Rust is correct by construction so for practical things you do not require a proof. It is just true that there are not memory violations.

[notriddle]

For the semantics of the language, there’s also the reference. It has warnings written all over it about it being incomplete, which it is, but it’s the most complete specification of Rust that exists. For anything that the reference doesn’t explicitly say, you can just assume it’s the same as C and you’ll probably be right.

As for Rust being proof-carrying, it’s not a general proof language. It’s definitely not intended to replace Coq, and SPARK-but-for-Rust doesn’t exist yet.

[GreatBowen]

Thank you I need the information for my University project I am very grateful

[GreatBowen]

I will start reading right now thank you

[CAD97]

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.)

[GreatBowen]

Thanks again