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