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
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