Как бы, типа, Вирт - это вчерашняя звезда. За последние 20 лет он ничего интересного не придумал и, наверное, уже не придумает.
А вот Гуревич - это звезда сегодняшняя. Из вступления к его лекции: родился в Челябинске, учился в Свердловске, в 28 лет защитил докторскую. Занимался какой-то алгеброй, вроде теории групп. В 1974 г. уехал в Израиль, оттуда - в США. В университете Мичигана заинтересовался информатикой, и как и положено чистому математику, задался вопросом: что представляют собой объекты информатики как науки?
На протяжении всей своей американской карьеры он развивает теорию "автоматов с абстрактными состояниями" - модель вычислений, которая наиболее плодотворна из всех ныне существующих. Основные достоинства этой модели - это её протяжённость по уровню абстракции, от аналога UML-диаграмм с одного конца до аналога машин Тьюринга с другого; моделирование параллельных и распределённых вычислений; строгая математическая формализация и логичное обобщение классической модели вычислений - машин Тьюринга.
Основной тезис его лекции - что машины Тьюринга, представляющие любую программу как функцию над строками, безнадёжно устарели. Например, какую функцию вычисляет операционная система? С точки зрения Тьюринга, это очень странная программа - мало того, что она работает месяцами и чаще всего принудительно останавливается прежде, чем успеет вычислить результат; на самом деле, "результат" операционной системы как функции - это то, что она выдаёт, когда перестаёт работать; это синий экран. Таким образом, у нас есть "функция", и нам надо, чтобы она "вычислялась" подольше
Другой недостаток машин Тьюринга - что многие объекты, типичные для практических вычислений, - графы, множества, вещественные числа и т.п. - невозможно эффективно представить в виде строк. Т.е. если мы хотим математически описать эффективную программу, то мы обязаны выйти за рамки строк и одномерной ленты машины Тьюринга.
Конечная цель его работы - научиться определять для двух записей программ в разных формах (например, на разных языках), одна и та же это программа или разные. В рамках модели Тьюринга неосуществимо не только это, но даже решение более простого вопроса: определить по программе, что она делает. Однако это ключевой момент тестирования, имеющий огромную практическую значимость.
Что самое важное: это не обычный профессор, сочиняющий непонятно что от скуки, а сотрудник Microsoft, создающий реально полезные продукты. Понятно, что система формального описания программ необходима и на этапе постановки задачи ("что должно получиться"), и на этапе тестирования ("то ли получилось, что надо"). Созданная его группой система постепенно внедряется во все отделы Microsoft; в частности, он хвалится, что отдел Windows уже использует эту систему.
gaidar, я тебя переубедил?