54 ms·
The title is a bit misleading: you're not formally verifying rust's opaque types - you're simply proving a intuitionistic logic proposition using Coq. There's n
by agluszak 4y ago
The title is a bit misleading: you're not formally verifying rust's opaque types - you're simply proving a intuitionistic logic proposition using Coq. There's nothing Rust specific in that proof.
- BreakfastB0b 4y agoThat’s totally fair, it does make it sounds like I’m verifying the compiler’s implementation of it. However it is proving that making such a transformation between the two styles of static dispatch is always sound. What would you have titled the blog instead to be less misleading?
- agluszak 4y agoIntroduction to Coq theorem proving using Rust static dispatch equivalency example