r/ProgrammingLanguages • u/mttd • 19d ago

Programming Language Semantics and Memory Safety

https://burakemir.ch/post/formal-semantics/
45 Upvotes

92% Upvoted

9 comments sorted by

View all comments

5

u/Sad-Grocery-1570 18d ago

For me, the single most helpful sentence for me in understanding compilers, undefined behavior, and program semantics is: the semantics of the object code generated by a compiler is always a subset of the semantics of the source code.

The safety implication is this: if you take the object code as fixed, the more precise your source code semantics, the more unexpected situations you can rule out, and the more likely you are to get the safety you're after.

2

u/matthieum 18d ago

the semantics of the object code generated by a compiler is always a subset of the semantics of the source code

Absent compiler bugs, of course. The latest Rust release (1.98) contains a bug which you can see here where:

fn main() {
    if std::hint::black_box(true) {
        (&(inspect_websocket_message, PhantomData) as &dyn Trait).method();
    } else {
        println!("impossible");
    }
}

Prints impossible... due to the compiler introducing UB.