Нина Аркадьевна Ветлугина · старший диспетчер
На доске четыре состояния, и их я проверю глазами. А в новой автоматике два поста, у каждого свой дежурный, свой аппарат и свой семафор, между ними телеграф. Инженеры говорят, что состояний там несколько тысяч. Мне нужна машина, которая обойдёт их все и, если что-то не так, положит на стол ленту с нарушением.
Такая машина называется проверяльщиком моделей. Это одна из немногих идей логики, которая окупилась в промышленности быстрее, чем её успели описать в учебниках. Intel проверяет так блоки процессоров после ошибки в делении Pentium 1994 года, Amazon проверяет протоколы своих хранилищ спецификациями на TLA+, NASA проверяла программы зондов. За неё Кларк, Эмерсон и Сифакис получили премию Тьюринга 2007 года.
Сегодня ты напишешь свой проверяльщик на Haskell и увидишь, где у метода предел.
урок из курса
Урок из курса «Логика и типы». Курс покупается один раз и остаётся навсегда: 500 ₽.
Оплата пока не подключена: премиум и курсы открываются промокодом.