Примечание : Этот ответ более точно не отражает то, что я думаю по этому вопросу. Мне не нравится его чрезмерно драматический, несколько противный тон. Кроме того, я не настолько уверен, что поиск правильного программного обеспечения оказался настолько бесполезным, как мне казалось тогда. Я оставляю этот ответ, потому что он принят, и за него проголосовали, и чтобы отредактировать его во что-то, что я в настоящее время считаю, в значительной степени разрушило бы его.
Я наконец дошел до чтения газеты. С чего начать?
Автор поет старую песню, которая звучит примерно так: «Если вы не можете доказать, что программа верна, мы все обречены!» Звучит лучше, когда громко кричали в сопровождении перемодулированных электрических гитар и быстрого барабанного удара. Академики начали петь эту песню, когда информатика была в области математики, в мире, где, если у вас нет доказательств, у вас ничего нет. Даже после того, как первый отдел информатики был отделен от математического факультета, они продолжали петь эту песню. Они поют эту песню сегодня, и никто не слушает. Зачем? Поскольку остальные из нас заняты созданием полезных вещей, хороших вещей из программного обеспечения, которые нельзя доказать правильными.
Наличие потоков затрудняет проверку правильности программы, но кого это волнует? Даже без потоков, только самые тривиальные программы могут быть подтверждены. Почему меня волнует, что моя нетривиальная программа, которая не может быть доказана правильной, становится еще более недоказуемой после использования потоков? Я не знаю.
Если вы не были уверены, что автор жил в академическом мире грез, вы можете быть уверены в этом после того, как он утверждает, что язык координации, который он предлагает в качестве альтернативы потокам, лучше всего можно выразить с помощью «визуального синтаксиса» (рисование графики на экране). Я никогда не слышал этого предложения раньше, кроме каждого года моей карьеры. Язык, которым можно манипулировать только с помощью графического интерфейса и который не работает ни с одним из обычных инструментов программиста, не является улучшением. Далее автор цитирует UML в качестве яркого примера визуального синтаксиса, который «обычно сочетается с C ++ и Java». Обычно в каком мире?
В то же время я и многие другие программисты продолжаем использовать потоки без особых проблем. Как правильно и безопасно использовать потоки - это в значительной степени решенная проблема, если только вы не зацикливаетесь на доказуемости.
Посмотрите. Потоки - это игрушка для большого ребенка, и вам нужно знать некоторые теории и схемы использования, чтобы хорошо их использовать. Как и в случае с базами данных, распределенной обработкой или другими устройствами, не относящимися к начальной школе, которые программисты успешно используют каждый день. Но то, что вы не можете доказать это правильно, не означает, что это неправильно.