Без заголовка

Это очень интересный вопрос: легкость верификации или ее трудность в зависимости от выбранного языка (в том числе верифицировать-то по идее не помодульно нужно, а весь код в совокупности!). Ибо идея с типами все меньше и меньше находит понимание в массах, а верификацию заменяют тестированием и юнит-тестами. Затраты же времени и сравнение по эффективности невозможны, ибо разные люди имеют производительность в кодировании на разных языках на порядки разные (т.е. мы измерим тем самым разницу интеллектов людей, а не производительность метода верификации/тестирования). Печаль, но все равно процесс потихоньку идет в массы -- хардвер уж точно верифицируется по самое не балуйся, всякие программы в истребителях, как видим, следущие на очереди. Хотя я не поверю, что выбор языка программирования для истребителя будет зависеть от выбранного способа верификации.