Simpler mental model for unsafe

[ia0]

I tried to go around existing discussions about unsafe like the following ones:

• Ambiguity of "unsafe" causes confusion in understanding
• What does `unsafe` mean?
• Unsafe Abstractions

I also tried asking around for discussions I might have missed, including on the wg-formal-methods stream of the rust-lang Zulip chat.

I'm surprised I didn't find anything matching my mental model because it seems pretty intuitive to me and has been my mental model since I learned about Rust in 2013.

The idea is just to add an informal proof system to Rust type system in a way familiar to programmers. Rust developers understand programming-related concepts like function parameter, function result, associated constant, etc. By describing unsafe-related concepts using programming-related concepts, most ambiguities about unsafe should hopefully be lifted.

I wrote Writing down my mental model of unsafe · GitHub with ideally enough details to be understood, but I'll also inline the first (and most important) section here for ease of reading. Please, if anything is still unclear, feel free to ask such that I can improve the document for future readers.

The proof type

Rust doesn't have a formal proof system. Proofs and properties are written in natural language (usually English). In my mental model, Rust provides a way to make those informal proofs and properties more explicit in Rust code and types. This is done using the following type:

/// Mathematical proofs for a given set of properties.
///
/// Proofs have no impact on execution. They only matter for type-checking. In particular, proofs
/// are `Copy`, zero-sized, and do not participate in function ABI.
///
/// The properties are never explicitly written. They are always inferred from the safety section of
/// the documentation of the item in which the type is mentioned.
#[lang = "proof"]
pub struct Proof<Properties> {
    /// A proof of the set of properties.
    ///
    /// This field is never explicitly written. It is always inferred from the safety comment of the
    /// statement in which the struct is mentioned.
    pub proof: Properties,
}

In this example, a proof is taken as argument and a new proof is returned:

/// Combines small numbers into a bigger number.
///
/// # Safety
///
/// The proof parameter properties are:
/// - The absolute value of `x` is smaller than or equal to 100.
/// - The absolute value of `y` is smaller than or equal to 100.
///
/// The proof result property is:
/// - The absolute value of the result is smaller than or equal to 1000.
fn combine(x: i32, y: i32, p: Proof) -> (i32, Proof) {
    let r = 3 * x + 2 * y;
    // SAFETY: By `p`, we know that `x` and `y` are between -100 and 100. By arithmetic, we know
    // that `r` is between -500 and 500. By arithmetic, we conclude that `r` is between -1000 and
    // 1000.
    let q = Proof;
    (r, q)
}

Digression (feel free to skip)

Using documentation and comments instead of types and code is mostly for practical reasons.

It is impractical to write types like Proof<"# Safety\n\nThe absolute value of the result is smaller than or equal to 1000."> and code like Proof { proof: "// SAFETY: We know that arguments are small, so some small linear combination is only slightly bigger." }.

However, a consequence of this choice is that it looks like we get some form of type erasure, but this is only in appearance. Even though the properties are erased from the types, the programmer must know at runtime the properties of all proofs (both parameters and results). For example, having a vector of function pointers like Vec<fn(Proof)> would need the programmer to know for each element, what are the properties expected to hold to call the function, because they may differ from one element to the other.

Vocabulary

I'll call pre-conditions (or requirements), proofs taken as parameter. And I'll call post-conditions (or guarantees), proofs that are returned. In particular, when calling a function, one has to prove the requirements and get back guarantees that can be used to prove future requirements. Note that pre-conditions may refer to code that happens after the function. For example, Pin::get_unchecked_mut() has a pre-condition that the result must not be moved, which is a property about what happens after the function is called. Similarly, a post-condition may refer to data that used to exist before the function was called. For example, slice::is_sorted() has a post-condition that the input is sorted if the result is true (assuming the standard library wishes to expose this post-condition for safety concerns).

I'll call invariants, proofs in any other position (neither parameter nor result of a function type), for example struct fields and associated constants. Invariants on mutable data must be updated at the same time the mutable data they refer to is updated. For proof fields, this is similar to self-referential structs because the proof field references the other fields.

Link with dependent types (feel free to skip)

This mental model comes from dependent type programming languages like Agda and Coq. If the proof type were formal, it would introduce a dependency from types on runtime values. Dependent types are rather inconvenient to use with the current state of research, so avoiding them is a reasonable decision for programming languages that wish to be widely usable. The proof type being informal, in particular its properties being just informal text, it doesn't formally refer to runtime values thus breaking this problematic dependency. But this informality is the reason why manual proofs and manually checking them is required for the type system to be sound. This can be seen as a usability trade-off: it's easier to write programs but it's harder to check their soundness.

[theme]

I don't think this works. In the case of data structures, as soon as there's an unsafe block in a safe function, the unsafetiness infects the entire module. Analyzing the entire contents of the module is required to ensure that a certain unsafe block is sound.

For example, the unsafe portions of Vec might require the invariant where the size of the vec is no more than its capacity. If we add into that module safe code that modifies private fields to break this invariant, then other unsafe code in that module suddenly become unsound.

[digama0]

@theme

I don't think this works. In the case of data structures, as soon as there's an unsafe block in a safe function, the unsafetiness infects the entire module. Analyzing the entire contents of the module is required to ensure that a certain unsafe block is sound.

This isn't quite right. An unsafe block means that invariants are being passed around in some way, but Rust's syntax doesn't make it explicit where and how. If you have an exact description of which functions have what preconditions and postconditions then you don't need the module boundary at all. What the module boundary helps with is ensuring that private functions/operations which are marked as safe even though they have unsafe preconditions cannot be called outside a bounded number of occurrences, and you have to manually check all the uses of these functions to ensure they have the appropriate safety conditions. If the language had unsafe fields this would mostly not be an issue, since then only syntactically unsafe operations would have unsafe preconditions.

@theme

For example, the unsafe portions of Vec might require the invariant where the size of the vec is no more than its capacity. If we add into that module safe code that modifies private fields to break this invariant, then other unsafe code in that module suddenly become unsound.

In this example, Vec has an invariant which links the size and capacity, making any change to size or capacity unsafe. In the desugaring proposed here, that means you need a Proof whenever you make any edits to these fields, and that Proof is bubbled up in unsafe functions like set_len. Unfortunately Rust does not have the ability to say that changing these fields is unsafe even though it is, so the next best thing is to have it be private and stick safety documentation next to each modification of the field anyway. The module boundary prevents external code from using the mistakenly safe fields without a safety argument, which the compiler cannot otherwise prevent.

[ia0]

Thanks for bringing this up! That's a very good point and I have in response clarified this in revision 8 of the gist. I'll still give an outline here.

In today's Rust, modifying a struct invariant doesn't need unsafe (and thus doesn't need a proof), it's only needed when that invariant is used. In particular, the proof when the invariant is used is not only "I have this invariant so what I'm doing is fine", but it's actually "I can prove this invariant by looking at all the places where the struct is modified. Now that I have the invariant, I can conclude that what I'm doing is fine". Usually this "I can prove this invariant by looking at all the places where the struct is modified" is not done at each unsafe block, but instead written somewhere at the top of the safety boundary and referred to by all unsafe blocks that rely on it.

Thanks @digama0 for writing down why the model is expressive enough to encode such invariants. I've also updated the gist accordingly in revision 8 and I refer the reader to the sub-section called "Improving invariants" for more information.

[RalfJung]

Thanks for sharing! I've in the past tried to update the unsafe docs (here and here) to more clearly align with my own mental model, which I think is pretty similar to yours except I am using different terms due to my background. But I didn't want to rewrite everything, and I didn't put "proofs" front-and-center since my expectation is that most people find that concept intimidating. But there can't be too much teaching material for unsafe, and there definitely are many different ways to teach this subject. It's always great to see someone make another attempt at this.

I think you'd be quite interested to read more about the "Curry-Howard isomorphism", if you are not already familiar with it. The basic idea is that "properties" (often called "propositions" in maths and logic -- basically, "things that make sense as truth statements") are the same thing as "types", and an inhabitant of such a type is a proof of the property. Your Proof type makes a difference between "a property" and "the type of proofs of that property", but it turns out it is very useful to consider those to just be the same thing.

On the note of "safety post-conditions", you may also want to consider the case of unsafe code relying on the functional correctness of safe code. This is perfectly legal and yet often causes surprise. It also means that safe code can need associated proofs. Consider, for instance, a crate providing a "sort" function on arrays of integers. (This is a silly example but you get the gist.) This function is safe and implemented entirely using safe code. Now I write some unsafe code, and for a crucial part of my algorithm and need an array to be sorted. If it's not sorted, things are unsound. So I import the "sort" crate and call it to sort my array. Now a bug in the "sort" crate can cause soundness issues, despite that crate not containing any unsafe! In a sense, the "sort" function has a post-condition of producing a sorted array, and then the unsafe code in my own crate elevates this to the status of a safety post-condition. This argument crucially relies on me picking some crate to do the sorting; if I let the user just give me a sorting function then obviously I cannot just assume that it will sort correctly. (EDIT: Looks like you are aware of this. I guess I must have missed this then when reading over your document, sorry.)

Other than that, I think this is a great outline for how one can teach unsafe. Turning it into something properly formal requires going deeper into what a "property" is. Your notes acknowledge this, when they talk about properties that "refer to code that happens later". I think the best framework to make sense of what happens here is Separation Logic, but I am biased since that's the framework I used in my PhD thesis to build a fully formally precise model of what the pre- and postconditions you are talking about might be. Using separation logic, properties can talk about ownership, and ownership can constrain what happens in other parts of the program or in later parts of the code, in a modular way.

[RalfJung]

@RalfJung

On the note of "safety post-conditions",

Ah I think I missed some of your discussion on that topic, sorry for that.

/// Writes a value to a reference and returns the previous value.
///
/// # Safety
///
/// After calling this function:
/// - The result value is the value within the reference before the call.
/// - The value within the reference after the call is the value parameter.
fn replace(ptr: &mut i32, val: i32) -> unsafe i32 {

As one immediate point of feedback, I would not use unsafe here. The returned integer is not unsafe to use, it's very safe to use!

This reminds me of the dual situation that can happen with arguments, which I referred to in the past as "super-safe". E.g. &str has a safety invariant of being valid UTF-8, but actually the validity invariant is just that it's an initialized byte sequence. We could now consider a function fn verysafe(x: &str) that documents that it is safe to call even if the argument is not valid UTF-8. Basically, its precondition is weaker than what the "default" precondition of a safe function is. That makes it "super safe".

Your replace is similar, except that polarities swap in the postcondition: it has a postcondition that is stronger than the default postcondition of a safe function.

So: a safe function has the standard pre/postcondition given by the types in the signature; an unsafe function has stronger preconditions / weaker postconditions; a "super-safe" function has weaker preconditions / stronger postconditions.

[ia0]

Thanks for the feedback! I've updated the document accordingly in revision 11.

But I didn't want to rewrite everything, and I didn't put "proofs" front-and-center since my expectation is that most people find that concept intimidating.

The documents you have written are indeed valuable and match my mental model too. I agree the concept of proofs can be intimidating, but I'm under the impression that the benefits of using this concept outweigh the initial intimidating cost (in particular when I see large projects using cargo-vet to scale manual unsafe reviews). I might be wrong with this impression, but I believe it's worth a try and see if it's indeed a concept too hard to grasp.

I think you'd be quite interested to read more about the "Curry-Howard isomorphism", if you are not already familiar with it.

Yes I'm aware of the Curry-Howard isomorphism I didn't mention it to keep the document as accessible as possible. We have the same background and most of my intuition indeed comes from ideas revolving around those concepts, in particular dependent type programming languages like Agda or Coq where proofs are explicit (and mechanically checked because they are terms).

Your Proof type makes a difference between "a property" and "the type of proofs of that property", but it turns out it is very useful to consider those to just be the same thing.

Yes, I did so because properties and proofs are "erased" in Rust (they are actually moved to documentation and comments). And I want some syntax for them to have explicit presence in types and code. By having Proof be a wrapper type around the properties, it simply becomes some unit type after erasure. And wrapper types and unit types are fairly familiar concepts to Rust programmers.

On the note of "safety post-conditions", you may also want to consider the case of unsafe code relying on the functional correctness of safe code. This is perfectly legal and yet often causes surprise.

I didn't know this was perfectly legal. I'm actually arguing the opposite, because as you say later, this is just a ticking bomb. Those large projects that try to leverage cargo-vet to track unsafe reviews need to know when functions with safety post-conditions are changed such that they get reviewed. If there is an unsafe keyword on those functions, then a review will trigger. In particular, I don't think the concepts of correctness and soundness should conflate. All functions claim to be correct with respect to their documentation, and if they are incorrect that's sound. However, some functions may additionally claim which properties of their correctness can actually be relied upon using a safety section. But that's probably also what you think, I'm just clarifying.

As one immediate point of feedback, I would not use unsafe here. The returned integer is not unsafe to use, it's very safe to use!

I got that feedback in the past and forgot to take it into account. Thanks for bringing it up! I clarified that the unsafe keyword is part of the function type and not part of the result type. And also described the case where it can actually be understood as part of the result type. When the properties are only about the function result value, then a wrapper type could encode those properties, like NonNull or some hypothetical SortedVec.

This reminds me of the dual situation that can happen with arguments, which I referred to in the past as "super-safe".

Oh wow, that's a very interesting concept and I like the name. I'll have to sleep on it to see how to merge it in my document. But the current way I would internalize it right now would be:

• Properties may strengten a type down to bottom and weaken it up to its validity invariant. The default (absence of properties referring to values of that type) is the safety invariant.
• A weakened type is unsafe to use but safe to produce.
• A strengten type is safe to use but unsafe to produce.
• Your function classification can now be deduced using the variance of functions.

Parameter	Result	Classification	Description
default	default	safe	The usual safe functions
stronger	default	unsafe	The usual unsafe functions
default	weaker	unsafe	The weird unsafe functions like Pin::get_unchecked_mut and String::as_mut_vec
stronger	weaker	unsafe	Doubly unsafe functions (both cases above at the same time)
weaker	default	super-safe	Take &str but doesn't need to be UTF-8, or take &mut T and doesn't move it
default	stronger	super-safe	Output is sorted, or output is non-null
weaker	stronger	super-safe	Doubly super-safe functions (both cases above at the same time)
stronger	stronger	bastard	Unsafe to call but super-safe output
weaker	weaker	bastard	Super-safe to call but unsafe output

Typical bastard functions would be identity functions because they preserve the proof. But I'm sure we can find actual examples, in particular for the stronger stronger bastard because relying on correctness without explicit permission is easily done, and I would not be surprised if a non-negligible amount of unsafe functions are actually of the stronger stronger bastard class.

Of course it can actually be even more complicated by having a function take both a stronger parameter and a weaker parameter at the same time, thus increasing the bastard taxonomy. This is why having core concepts that compose well is probably a better approach than classifying functions in coarse categories like safe, unsafe, super-safe, and bastard.

[CAD97]

@ia0

On the note of "safety post-conditions", you may also want to consider the case of unsafe code relying on the functional correctness of safe code. This is perfectly legal and yet often causes surprise.

I didn't know this was perfectly legal. I'm actually arguing the opposite,

This is unfortunately extremely untenable. Taken to the extreme, you're arguing that I can't rely on functions like i32::wrapping_add or ptr::wrapping_offset to be correct. All proofs have and should state their assumptions, and a flood-fill view of all potentially soundness relevant code could be useful (or uselessly highlight everything), but asking unsafe code to only rely on unsafely delivered guarantees needlessly restricts unsafe code from using safe abstractions and expands the domain of when you're expected to use unsafe from "downstream safe API misuse could potentially use this to cause UB" to "downstream unsafe could potentially use this to avoid causing UB."

By relying on upstream safe APIs for your own soundness, you're essentially opting in to considering their relevant correctness issues as your soundness issues. Perhaps think of it like an unsafe fn i_checked_it which attaches a proof to an otherwise safe implementation.

Or, alternatively, there's an implicitly attached proof burden to the unsafe that you don't call the downstream code in a way that causes soundness relevant correctness issues.

Regarding Rust unsafe as an untyped proof assistant, then yes, capturing every single bit of proof logic beyond "the AM primitives are correct" into an unsafe carrier has utility. But the superpower of Rust is zero fanfare "FFI" between safe Rust and unsafe Rust; insisting that safe functionality is rewritten into "proof assistant Rust" before it's usable from unsafe Rust goes against that ideal that all code should be safe if possible.

Unsafe Rust shouldn't rely on complicated invariants of safe code, only simple correctness properties that are unlikely to regress. But this is just good engineering practice, anyway — reduce the soundness relevant complexity surface to make reasoning easier. And utilizing safe API assists in such encapsulation of invariants.

[RalfJung]

@ia0

I didn't know this was perfectly legal. I'm actually arguing the opposite, because as you say later, this is just a ticking bomb.

I didn't say that anything was a "ticking bomb".

As @CAD97 explained, there's no practical alternative to allowing this.

@ia0

I got that feedback in the past and forgot to take it into account. Thanks for bringing it up! I clarified that the unsafe keyword is part of the function type and not part of the result type.

The function isn't unsafe though. It is more safe than a regular fn. It is a super-safe function, not an unsafe one.

@ia0

• Properties may strengten a type down to bottom and weaken it up to its validity invariant. The default (absence of properties referring to values of that type) is the safety invariant.
• A weakened type is unsafe to use but safe to produce.
• A strengten type is safe to use but unsafe to produce.
• Your function classification can now be deduced using the variance of functions.

Yes that sounds right.

[ia0]

This is unfortunately extremely untenable.

It's a trade-off between 2 worlds, both of which are untenable in their own sense:

• Implicit: Unsafe code is allowed to rely on correctness of safe code.
• Explicit: Unsafe code can only rely on correctness of safe code as described in their safety documentation.

In the implicit world, safety comments may look like this:

• They don't even mention the correctness properties they rely on, because it's unconscious (usually because it's so obvious it must be true). For example AsRef and Borrow returning the same result when called multiple times.
• They mention the correctness properties they rely on, but argue that they are relied upon so often that if they're broken everything is broken.
• They mention the correctness properties they rely on, but argue that they are so trivial they can't be or become broken.

Safe functions don't need to do anything, including when unsafe code relies on their correctness. Of course, if they follow good engineering practice (documentation, testing, code review) it's better, but there's nothing formal and no enforcement.

In the explicit world, safe functions may document what properties unsafe code may rely on. By default (i.e. without documentation), it's whatever safe Rust says. This documentation is traceable by tooling, such that when such function is modified, dedicated tooling may trigger a special review to make sure the guarantees still hold. Safety comments can only rely on guarantees described in the safety documentation of safe functions. As I mentioned in the document, this explicit world can already be encoded in today's Rust. Every function is simply the implementation of a trait with a single method. Past and future implementations of this function are simply alternative implementations of this trait. They must all satisfy the same API, the one described in the trait.

Now back to the trade-off. How are each of those worlds untenable?

• The explicit world asks safe functions to document which properties unsafe code may rely on. The safe functions that need to do this is arguably small. Unsafe code usually doesn't rely too much on safe code. Note that the standard library may have a special treatment (tooling is able to distinguish it from other crates).
• The implicit world provides soundness improvement compared to C. This is not perfect because soundness is not traceable: unsafe code may rely on correctness of safe code without any syntax on the safe function.

Note that there will be bugs anyway in both worlds (either because a proof is just wrong, or because something moved under your feet in the implicit world). Also both worlds are not incompatible. It is possible in the explicit world for unsafe code to rely on undocumented correctness of safe code. This would be exactly the same as in the implicit world. Such unsafe code would probably get a lower rating during unsafe review, but it would still compile and run. The opposite is also possible, safe function with explicit correctness could be encoded using unsafe traits, to the cost of some boilerplate. So this is really just a trade-off between: how well can we track unsafe for reviews, how much boilerplate do we need to write, how much work do we need to put in documentation and more importantly API design for safety, etc. So it all depends on your personal opinions, and each project and each company will have differing opinions.

[ia0]

I didn't say that anything was a "ticking bomb".

Right, my interpretation, my bad

The function isn't unsafe though. It is more safe than a regular fn. It is a super-safe function, not an unsafe one.

Indeed, the keyword unsafe doesn't mean "unsafe function" here. It's just a keyword. It's true that we could introduce a new keyword that tooling would need to track in addition to unsafe. For example your "super-safe" idea could be a keyword. Such functions would have type fn(...) -> supersafe i32. [EDIT: Actually, I'll have to sleep on this too. I definitely believe I should incorporate this idea of supersafe as the antonym of unsafe. It might clarify things and avoid confusion.]

[ia0]

Ok, I've slept on it and have a better explanation for super-safe.

Types have 2 disjoint sets of behaviors:

• The safe behaviors that I'll write SAFE. This is defined by the safety invariant.
• The valid (but not safe) behaviors that I'll write VALID. This is defined by the validity invariant (removing the safety invariant which is a subset of it).

Properties may modify the set of behaviors of types in 2 ways:

• Adding behaviors from VALID. I'll call this set UNSAFE.
• Removing behaviors from SAFE. I'll call ROBUST the complement of this set with respect to SAFE.

The final set of behaviors of a type is the disjoint union of ROBUST and UNSAFE. Note how those 2 ways are orthogonal and thus compose. By default, UNSAFE is empty and ROBUST is SAFE.

I define the following adjectives for types:

• A type is unsafe if UNSAFE is not empty.
• A type is robust if ROBUST is a strict subset of SAFE.

By composition a type may be both unsafe and robust. In particular, a type that is only robust is what you call a super-safe type.

By the variance of functions, we deduce that:

• A function is unsafe if a parameter is robust or a result is unsafe.
• A function is robust if a parameter is unsafe or a result is robust.

Of course, function types may also be modified in more complex ways than the parameters and results independently. The most common way is correctness, when relating results to paramaters.

Now that we have this notion of robustness, it is possible to update the confusing fn(Params) -> unsafe Result to robust fn(Params) -> Result making it clearer that it's a function keyword. And due to composition it is possible to have robust unsafe fns, which I believe is less surprising to read than super-safe unsafe fns. But keyword suggestions for robust are welcome (I initially considered tight and sober as alternatives).

I'll have to sleep on this more, in particular to find a way to make this mental model more accessible to Rust programmers, but I believe this should remove some confusion that is still present in my document regarding pre-conditions, post-conditions, requirements, and guarantees. The notion of robustness and unsafeness together with variance should be enough to explain the rest.

[RalfJung]

@ia0

It's a trade-off between 2 worlds, both of which are untenable in their own sense:

The world you call "implicit" is the world we already live in. It seems quite tenable to me.

In my example, the safety comment of my unsafe code should say something like, "here we rely on the sort crate actually sorting the array".

@ia0

The explicit world asks safe functions to document which properties unsafe code may rely on. The safe functions that need to do this is arguably small. Unsafe code usually doesn't rely too much on safe code. Note that the standard library may have a special treatment (tooling is able to distinguish it from other crates).

No that's not what you said above, at least it's not how me (and seemingly @CAD97 ) understood what you said above. You said it should not be legal for unsafe code to rely on functional properties of safe code. No mention of documentation was made, so the statement applies whether those properties are documented or not.

Of course unsafe code should only rely on documented properties of safe code. All code should only rely on documented properties of code it imports. That's not what we were talking about above. Maybe you misunderstood what we were saying.

So to refine my earlier statement: you may also want to consider the case of unsafe code relying on the documented functional properties of safe code. This is perfectly legal and yet often causes surprise. (The bold parts changed. Following common standards, I'd never consider it justified to rely on undocumented functional properties so this went without saying in my earlier post.)

The key point is that, documentation or not, its safe code. There is therefore no "proof" being generated there, since only unsafe code needs proof. But sometimes, producing a proof for some unsafe code can require first producing proof for other safe code. (That basically makes that code "super safe".)

@ia0

Ok, I've slept on it and have a better explanation for super-safe.

Types have 2 disjoint sets of behaviors:

• The safe behaviors that I'll write SAFE. This is defined by the safety invariant.
• The valid (but not safe) behaviors that I'll write VALID. This is defined by the validity invariant (removing the safety invariant which is a subset of it).

I have no idea what you mean by behaviors being "defined by" an invariant. A function has a single set of behaviors -- for each value of the input arguments (and state of memory), it does a thing.

[ia0]

@RalfJung

No that's not what you said above, at least it's not how me (and seemingly @CAD97 ) understood what you said above.

I believe we are discussing with different categories of programmers and projects in mind.

I mentioned large projects using cargo-vet to scale manual unsafe reviews above. That's the category I have in mind, because that's why I wrote down my mental model in the first place since that's when it matters to have a correct mental model. I agree it is a very small fraction of Rust programmers and projects, which is why you and probably @CAD97 had in mind the majority of Rust programmers and projects, which is a very sensible thing to do at first.

As I said at the end of my answer to @CAD97, each Rust programmer or project will have a different opinion on how unsafe reviews (and more generally soundness) should be handled. For most, if it compiles and works on the inputs that matter, then it's all good. That's the C approach and the most pragmatic for most people. However, for others who are already investing colossal efforts doing third-party unsafe reviews, soundness is apparently a more serious business. I am worried about those efforts for many reasons:

• Proving soundness is extremely hard (let alone that it's not always clear what needs to be proven at the moment).
• Proving soundness is impossible unless you fully control the running environment. For example, you can modify your memory in safe Rust on Linux.
• Even if you proved soundness, you may still have soundness bugs.
• For all this work to be tractable and maintenable, you need reliable tooling. That's the point I'm trying to address with my mental model.

However, I find those efforts an interesting experiment. Eventually some of the issues above will have solutions. At that point, all the experience learned from those experiments will pay off, even if they did not bring any value until then.

So I'm not arguing about forcing everybody to be explicit about soundness. I'm arguing about the language providing the means, for those who care about being explicit about soundness, to do so. And I'm also arguing that the language already provides some of the means while it didn't have to, namely unsafe functions and unsafe traits.

@RalfJung

The world you call "implicit" is the world we already live in.

Not really. Today's Rust is neither the implicit world nor the explicit world. For example, I don't think anyone would complain about the following program to be unsound:

fn main() {
    let p = Box::into_raw(Box::new(42));
    println!("{}", unsafe { p.read() });
    drop(unsafe { Box::from_raw(p) });
}

Now, let's assume someone refactors the code by introducing helper functions:

fn alloc(x: i32) -> *mut i32 {
    Box::into_raw(Box::new(x))
}

fn read(x: *mut i32) -> i32 {
    unsafe { x.read() }
}

fn free(x: *mut i32) {
    drop(unsafe { Box::from_raw(x) });
}

fn main() {
    let p = alloc(42);
    println!("{}", read(p));
    free(p);
}

The code is sound. The helper functions are local to the module and file so their invariants don't escape the safety abstraction.

Now, let's assume someone refactors the code by moving those helper functions in a separate module. They could still be safe functions. The safety abstraction is the crate. But now some may argue (some may already have argued on the first refactoring) that it would be better if those functions were marked unsafe. It would help make the code maintenable by avoiding mistakes.

The next step would be to move those helper functions to another crate. Now probably most people would like to know that those functions are unsafe.

Similar concerns exist with traits and solved with unsafe traits.

There is a lot of flexibility in how programmers and projects may organize their code. The language provides 2 optional ways to annotate the code to indicate something is relevant for soundness: unsafe functions and unsafe traits. The language also provides comments and documentation that can be used for a similar effect. The community also came with the convention of using the "safety" keyword within comments and documentation to highlight that they are relevant to soundness. All those things are optional and have no impact on the actual soundness of the code. However, they have an impact on the review and maintenance of the code.

What I'm trying to do, is raise awareness that some aspects of unsafe don't yet have optional annotations, namely those related to the robust keyword. I'm not even suggesting the language to change, that's up to the community. I'm just trying to raise awareness to this problem, and I'm still not able to figure out how to explain it.

@RalfJung

I have no idea what you mean by behaviors being "defined by" an invariant. A function has a single set of behaviors -- for each value of the input arguments (and state of memory), it does a thing.

I'm talking about types in general, not just functions. What I mean is essentially chapter 10 of your thesis. I use behaviors as a broader term for values. A type is thus 2 disjoint sets of values: those that are valid but not safe, and those that are safe. Programmers may create new types by adding unsafe values and/or removing safe values to an existing type. This new type is anonymous and syntactically the same as the original type. This can be either done implicitly or explicitly in some documentation. I'll assume explicit documentation for clarity. For example &mut String may be documented as possibly having unsafe values that are not UTF-8. It may alternatively be documented as not having safe values that are non-ASCII, thus being a robust version of &mut String.

A bit more complex (and I got it wrong on the first attempt), it may also be documented as not having safe values that restrict the prophecy to UTF-8 at the end of the borrow. I suspect prophecies to be contra-variant and denote a set of values too, essentially making mutable borrows look like inverted functions where you get the result and must return the parameter. So &mut T is interpreted as 2 types, the present type which is covariant and the prophetic which is contra-variant.

[RalfJung]

@ia0

I use behaviors as a broader term for values.

Oh... that's very confusing.^^ I would suggest you avoid doing that, as "behavior" already has meaning in PL theory and it's very different from "value". "behavior" is about what a program or function does when executed.

[ia0]

@RalfJung

"behavior" is about what a program or function does when executed.

But those are somehow related (unless I'm mistaken, which might be the case, because all this is pretty old to me). Your different semantics (denotational and operational in particular) should somehow agree. So your behaviors are somehow related to your values, in particular the behavior of a function or program is encoded in its value. But it's true that it's probably better to use a "static term" for denotational semantics: value. And use a "dynamic term" for operational semantics: behavior. If this can avoid confusion. Thanks!

[RalfJung]

Values are inert, they don't have "behavior". That's pretty much their defining feature. So talking about values as "behavior" really makes no sense at all to me. I don't understand what it is you are trying to generalize about "values" in the first place.

Values of function type can be called and that leads to terms that have behavior, true. But that doesn't mean that "behavior" is a generalization of "value". After all, e.g. values of integer type have a prime factorization, and yet we don't say that "prime factorization" is a generalization of "value". It's just something some values have. (So first of all there's a category error here -- some values have behavior when invoked, but no values are behavior. And secondly, the fact that it's only some values is quite relevant as well.)

[ia0]

I think that's fair. I'll probably just mention that values, even though purely inert, may encode things through interpretation, for example functions encode a mapping from input value to output value, and mutable references encode a pair of a current pointed value and a final pointed value predicate.

EDIT: Actually, we could even say that values encode properties about behaviors (even though some may be trivial). In some way they describe what behaviors are possible. But this is indeed jumping one step ahead.

[CAD97]

@ia0

Proving soundness is impossible unless

I think this might be the crux of the disconnect. I don't see Rust as being a language where "proof assistant level" proofs of soundness are an achievable nor desirable goal. Soundness logic should be stronger than just vibes, but the unavoidable shakiness of the proof foundation means that the extra effort to go from "sound" to "provably sound" doesn't yield benefits.

So in the case of

slice.sort();
if !slice.is_sorted() {
    // SAFETY: ???
    unsafe { unreachable_unchecked() }
}

I would describe the safety conditions here as a precondition on this unsafe block that <[_]>::sort and <[_]>::is_sorted behave as described, not postconditions on <[_]>::sort and <[_]>::is_sorted. Given their behavior is dependent on T: PartialOrd, it's actually easier to specify the requirement at the use site than to try to parameterize a guarantee.

In projects going the extra mile to thoroughly track soundness reasoning, it's absolutely a good idea to document and track where/how/why correctness requirements are uplifted to soundness requirements. It's necessary to realize that this is a thing which is done, yes.

But ultimately it's a position that having safety documentation on safe APIs^[1] doesn't really help anyone. The way to reduce "soundness relevant" code isn't repeatedly stating "this correctness may be relied on for soundness," it's refactoring to reduce the amount of code in the soundness boundary of the trusted code, such that the flood fill of unsafe trust hits less code.

And obviously, one should only rely on documented properties. But security critical patch introduced regressions aren't limited to that which flows into unsafe (although unsafe issues are easily the worst offender), so if you're tracking unsafe dependencies so thoroughly, you should probably do so for other security properties as well, and use the same technique to track both. You'll have a much more interesting time arguing for code documenting "security postconditions" than safety postconditions.

---

1. …that aren't directly related to unsafe functionality. E.g. calling out pointer validity bounds in a safety section of the documentation for as_ptr is reasonable. ↩︎

[ia0]

@CAD97

I don't see Rust as being a language where "proof assistant level" proofs of soundness are an achievable nor desirable goal.

Yes, that's my point. I know first hand how unrealistic it is to prove real-life programs correct by typing having played with Agda, Coq, and F-star 10 years ago. But then I see those efforts (please check this and this if you didn't already) and instead of trying to stop them, my first instinct was to try to help them, by providing a mental model that would make apparent potential weaknesses in the system. I'm curious to know your position regarding those efforts. I already told mine (I'm worried for them, but would not complain if they spend resources trying this untenable effort, because we may learn as a whole from those experiments). Note that I'm specifically referring to the soundness concerns. Reviewing third-party code for other aspects (cryptography, security) is better understood.

I'm also curious to know your opinion about me providing a correct mental model for unsafe. So far you seem to be pushing against changing Rust, which I understand, but which is not what I'm trying to do. I'm providing a mental model to raise awareness about concepts that are currently implicit and not necessarily well understood. It's true that it would be nice if they had support to be explicit for education and for those who want to use them (again, without any enforcement whatsoever, there's no enforcement on unsafe anyway, you can just use safe functions/traits instead of unsafe functions/traits), but the immediate intent is to make them conscious. In the new revision of the document, I'm making this explicit from the start by stating goals and non-goals. I hope it will clarify such misunderstandings.