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

Хоар как раз и говорит, что одни эвристики по доказательству сменяются другими менее эвристиками -- все как раз идет к бОльшей классической доказательности. Он радуется, что правильно определил, что 20 лет внедрения в промышленность этих методов не будет, по факту, говорит, что даже 30 лет не было прогресса -- только-только сейчас начинается. Мне кажется, прогресс в формальном доказательстве программ происходит ровно в той же мере, в каком происходит прогресс в автоматическом написании программ (автоматическом написании чего бы то ни было: составлении чертежей, музыкальной композиции, сочинительства приличных стихов, рисовании картин и т.д.).