>間違える余地が在ることが問題

完全無欠な言語以外は認められないと？

>型Aと書いたものが実際にはAでないという可能性が生じた時点であらゆるコードが信頼性を失い

どういう場合にそのようなことが起きるかがわかってないんだろうね。結局使いこなしの問題。