Большинство программ, с которыми я сталкиваюсь, занимаются простой и нудной работой с ОС, железом и другим софтом и не нуждается в строгой верификации кода (и даже в строгой типизации ЯП). Интересно, существуют ли задачи, в которых необходимость формальной верификации существенна из тех, к которым есть доступ обычного программиста, а не работника научных организаций. Необходимо чтоб у задачи было четкое условие, метод решения был точным (непонятно как доказывать свойства рандомизированных решений) и по возможности длинным в реализации, чтобы была большая вероятность понаделать труднообраружимых ошибок.
Пока что придумалось только 2 направления: компиляторы/оптимизаторы и решатели математических задач. Какие у кого есть соображения по этому поводу?
