Proof and program are twins. Formalized theorems can be incompatible for exactly the same reasons that programming APIs can be incompatible.