I guess it's because the idea of verifying your software in a language that's completely different from the language that you wrote it in seems uncomfortable.

I guess it's because the idea of verifying your software in a language that's completely different from the language that you wrote it in seems uncomfortable. If your language is so good, oughtn't it be suitable for expressing its own properties?