4 ms·

What I really want is an integration of automated proof checking with unsafe code, allowing completely safe rust programs. Additionally, this could be extended

• zozbot234 6y ago
  This requires a formal semantics for Unsafe Rust. It's a hard problem, albeit one that's being worked on.
  • foota 6y ago
    I'm aware that however it's done it'll be hard. Does it really require formal semantics for unsafe rust though? I'm not familiar enough with rust to give an example, but if you imagine there's the unsafe rust level and beneath that the "machine code" (not actually machine code, just at the abstraction level equivalent to it) you should be able to hand write what the rust code is doing, without requiring the compiler to construct the machine level operations. With a formal semantics the proof checker just checks that the written proof (at rust level) matches with the rust code, but requires as you said an understanding of how unsafe rust interacts with the proof, whereas with a proof written at machine level, you don't need to understand the rust semantics, you just need to translate the rust to machine level and then check the proof there. Perhaps the machine level could be some layer in llvm? I'm only a little familiar with compilers, and hardly at all with more complicated compiler theory, but this seems reasonable to me.
    • kd5bjo 6y ago
      > With a proof written at machine level, you don't need to understand the rust semantics, you just need to translate the rust to machine level and then check the proof there. This approach would only be able to verify a particular compilation result as safe. If you want to verify that it will always be safe, you need to be comparing against the behavior of future compilers, which requires some kind of contract about their behavior. “Formal semantics” is the technical term for that contract.
    • bennofs 6y ago
      The problem is that the unsafe-safe boundary needs to be specified. Unsafe code often relies on invariants ensured due to safe rust's checks. Also, there are properties that unsafe code has to satisfy which are special to rust, for example involving rules around special traits like `Drop`. So even if the unsafe code itself could be proven to have no memory corruptions, if it does not satisfy these invariants, it could lead to wrong behaviour in other parts of the program.
  • doonesbury 6y ago
    Any references?
• doonesbury 6y ago
  Amen to that. Integrated formal systems giving the spec working with the programming language on the implementation side is the holy grail.