3 ms·

Verifying Dynamic Trait Objects in Rust (2022)

• lapcat 3y ago
  (2022)
• 2h 3y ago
  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?
  • kaikalii 3y ago
    trait Namer { fn first(&self) -> String; fn last(&self) -> String; // You can put this here if you want `namer.name()` fn name(&self) -> String { format!("{} {}", self.first(), self.last()) } } fn name(n: &impl Namer) -> String { format!("{} {}", n.first(), n.last()) }
    • 2h 3y ago
      cool much thanks, one more reason to move to Rust hehe - since "let else" was added its looking pretty attractive
      • iknowstuff 3y ago
        let else is a rather minor addition, surprising that that's what's winning you over
• staunton 3y ago
  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.
• enos_feedler 3y ago
  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