[HN Gopher] Verifying Dynamic Trait Objects in Rust (2022)
       ___________________________________________________________________
        
       Verifying Dynamic Trait Objects in Rust (2022)
        
       Author : luu
       Score  : 18 points
       Date   : 2023-05-16 00:12 UTC (22 hours ago)
        
 (HTM) web link (dl.acm.org)
 (TXT) w3m dump (dl.acm.org)
        
       | lapcat wrote:
       | (2022)
        
       | staunton wrote:
       | 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.
        
       | 2h wrote:
       | 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 wrote:
         | 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 wrote:
           | cool much thanks, one more reason to move to Rust hehe -
           | since "let else" was added its looking pretty attractive
        
       ___________________________________________________________________
       (page generated 2023-05-16 23:01 UTC)