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.
That’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?
Comments
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.
That’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?
Introduction to Coq theorem proving using Rust static dispatch equivalency example