A less type-safe language would still be isomorphic to a mathematical proof, but it could contain a wider range of errors compared to a more type-safe language.

A less type-safe language would still be isomorphic to a mathematical proof, but it could contain a wider range of errors compared to a more type-safe language. The language could be either functional or imperative, and still be isomorphic to a proof. A correct (error-free) computer program written in any language (even javascript) would be equivalent to a correct mathematical proof. It's a bit mind-bogglingly profound, but that's the beauty of the Curry-Howard correspondence.