各言語、得意分野あるからな。
証明付きでプログラム書けとかなったら、Coqなどの証明支援系の独壇場で、
他言語の入り込む余地がないように思われるが如何？