Fascinating that a Haskell tool mapped so well to Rust. Might make it easier to do seL4-style developments with Rust given they simultaneously do a Haskell model and C code w/ equivalence proof. A Haskell subset that uses whatever verification & testing tools they have might be extracted to an equivalent Rust program automatically or with manual guidance. The assertions or tests would be extracted for equivalence testing. That might have significant safety and maintenance benefit even without HOL parts.<p>What do the Rust people think of that idea? And how hard would you guess an AutoCorres-style tool be for it vs C in event we wanted HOL parts?