ia0

Writing down my mental model of unsafe

DEPRECATION WARNING: This document is now deprecated. The new version is available here.

TLDR: All language constructs regarding unsafe Rust (including those that do not exist yet) can be explained by a single concept: the proof type (see first section). Understanding this concept is enough to understand unsafe.

I always assumed the content of this document to be obvious, but came to realize while discussing

ia0

mod graph {
    use flux_rs::*;

    #[opaque]
    #[refined_by(len: int)]
    // Invariants (trusted):
    // - There are len elements
    // - The i-th element has type [Edge(i); 2]
    pub struct Graph(Vec<[Edge; 2]>);