Введение

Евклид — это императивный язык программирования для написания верифицируемых программ. Он был разработан в середине 1970-х годов Батлером Лэмпсоном и Джеймсом Г. Митчеллом в лаборатории Xerox PARC в сотрудничестве с Джимом Хорнингом из Университета Торонто, Ральфом Л. Лондоном из USC ISI и Джеральдом Дж. Попеком из UCLA. Реализацией руководил Рик Холт из Университета Торонто, а Джеймс Корди был главным программистом первой реализации компилятора. Изначально он был разработан для микропроцессора Motorola 6809. Он считался инновационным для своего времени; команда разработчиков компилятора имела бюджет в 2 миллиона долларов на 2 года и была профинансирована Агентством передовых исследовательских проектов Министерства обороны США и Канадским департаментом национальной обороны. В течение нескольких лет он использовался в I. P. Sharp Associates, MITRE Corporation, SRI International и различных других международных институтах для исследований в области системного программирования и безопасных программных систем. Евклид произошел от Pascal, Mesa, Alphard, CLU, Gypsy, BCPL, Modula, LIS и SUE. Функции в Евклиде имеют закрытую область видимости, не могут иметь побочных эффектов и должны явно объявлять импорты. Евклид также запрещает использование операторов goto, чисел с плавающей точкой, глобальных присваиваний, вложенных функций и псевдонимов, а ни один из фактических параметров функции не может ссылаться на одну и ту же ячейку памяти (которую Евклид называет «переменной»). Евклид реализует модули как типы. К потомкам Евклида относятся язык программирования Concurrent Euclid и язык программирования Turing.