Coqだって酷いもんだ

こうすればCoqに入門できそうだ （誰も書かないCoq入門以前 5） - 檜山正幸のキマイラ飼育記 :

そして、説明に使う言葉がまた問題です。Coqの説明には、関数型言語、論理、型理論などの言葉が入り混じって登場します。型理論の用語や記号が無茶苦茶のグチャグチャであることは「用語法／記号法／図示法は、ほんっとうーに方言が多い」からリンクされている一連のエントリーを参照してください。Coqでは型理論の用語に加え、論理やラムダ計算の用語、Coq独自の用語も混じるので、さらに輪をかけてグッチャングッチャンです。同意語、多義語、曖昧語がたくさんたくさん使われています。その一例は、「Coqの証明ゲームの表側と裏側 （誰も書かないCoq入門以前 4）」に挙げた「ゴール」という言葉です。混乱を招く用語法や、ミスリーディングな説明の仕方が、伝統や文化として定着してしまっているのでしょうか。