Verifying Dynamic Trait Objects in Rust (2022)

I love how the approach detailed in the paper seems to be headed towards a unified framework that can reason about not only Rust but also e.g. C/C++ (and all LLVM) programs. This might be another part of the small miracle that LLVM seems to immensely accelerate compiler/language development despite not introducing any fundamentally new concepts, just making existing ones much more accessible and usable by third parties.

I don't know how practical this system is but the practical prospect of semi-formally reasoning about critical parts of programs seems very exciting to me, especially with AI possibly revolutionizing software development on the horizon.

Very cool to see my dorm mate Daniel from 20 years ago (!) as co-author on this paper. Wow. Really smart dude and proud to see his work

question for all you Rust people. does Rust have a way to use interfaces like Go? For example with Go I can do this:

    package hello
    
    type namer interface {
       first() string
       last() string
    }
    
    func name(n namer) string {
       return n.first() + " " + n.last()
    }

I think I saw on a blog post that Rust can only do this with some hacks, is that true?

(2022)