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?