Лингвист Ноам Хомский, создатель иерархии грамматик, носящей его имя.
Меньший успех имела формальная спецификация семантики языков программирования, то есть описание их поведения. Было разработано несколько спецификаций, но ни одна из них не пользуется такой популярностью, как формальные средства описания синтаксиса.
Первой из предложенных была VDL (Vienna Definition Language), созданная в венской лаборатории IBM для формального определения языка PL/I. Она состоит из двух частей: транслятора, выстраивающего абстрактное синтаксическое дерево для программы на языке PL/I, и интерпретатора, который указывает, как следует исполнять или интерпретировать программу, соответствующую этому дереву. Эта семантика называется операционной семантикой и является крайне подробной. Так как язык PL/I очень объемен, беспорядочен и изобилует частными случаями, его формальная спецификация также очень объемна и сложна для понимания. За свои размеры она получила шутливое название VTD — Vienna Telephone Directory («Венский телефонный справочник»). Тем не менее создание этой спецификации стало важным достижением в данной области.
Работы в венской лаборатории были продолжены, и появилась вторая, улучшенная версия спецификации — VDM (англ. Vienna Development Method — венский метод разработки), содержащая несколько особых свойств для создания спецификаций императивных языков. Эта спецификация была создана в 1982 году как объединение точек зрения Динеса Бьёрнера и Клиффа Джонса, которые легли в основу двух школ программирования — датской и английской соответственно. VDM использовался для созданий спецификаций языков Pascal и Алгол-60, а также для подмножества языка Ада’79.
С другой стороны, выдающийся американский ученый Роберт Флойд в 1967 году показал, как можно оценить корректность программы с помощью утверждений (assertions), помещенных в определенные участки программы. Каждое утверждение — это логическая формула, устанавливающая некое отношение между переменными программы. Утверждение остается истинным по завершении программы и устанавливает связь между ее входными и выходными значениями. Метод Флойда улучшил и дополнил британский логик Чарльз Хоар, изложив его в виде набора аксиом и правил вывода, связанных с построением языков программирования, и дав определение аксиоматической семантике. В 1973 году Хоар и Вирт опубликовали аксиоматическую спецификацию подмножества языка Pascal. Во время работы над ней они обнаружили некоторые недостатки в языке и исправили их, создав новую, улучшенную версию Pascal. В следующем году Хоар и Лоуэр изучили возможность одновременного использования аксиоматической и операционной семантики. Эдсгер Дейкстра представил понятие слабейшего предусловия в 1973 году.
Дональд Кнут (слева) и Гэрман Цапф обсуждают свойства новой компьютерной типографики. Стэнфордский университет, Калифорния, 1980 год.
Существуют и другие способы описания семантики языка. В 1968 году силами Дональда Кнута, одного из самых уважаемых специалистов в области вычислительных систем, известного своим чувством юмора, была создана атрибутивная грамматика.
Эта грамматика подробным образом изучается применительно к методам компиляции. Существует и четвертый тип семантики — денотационная, которая была разработана в Оксфордском университете американцами Даной Скоттом и британцем Кристофером Стрэчи в начале 1970-х. В денотационной семантике каждой программе присваивается значение, называемое денотацией (denotation), выраженное в терминах математических объектов. Денотация, как правило, является функцией, сопоставляющей входные и выходные значения программы. Проводились исследования систем для генерации компиляторов на основе денотационной семантики языка, однако на данный момент подобные системы являются крайне неэффективными.
Теория вычислительных систем далека от того момента, когда найдут применение все ранее полученные результаты и будут объединены ранее созданные теории. Напротив, эволюция вычислительных систем продолжается, и она как никогда связана с развитием технологий, дающих нам возможности, о которых раньше нельзя было и мечтать. Языки программирования управляют не только нашими компьютерами, но и телевизорами, мобильными телефонами и даже простейшей бытовой техникой. Мы вновь совершаем первые шаги в новый мир. Как вы увидели, современный облик нашего мира сформировался не случайно, а в результате упорного труда человека. Тем не менее настоящее — лишь эпизод по дороге к непредсказуемому, но, вне всяких сомнений, удивительному будущему.