A Euclid a helyesség-bizonyítható programok nyelve. A Toronto Egyetemen fejlesztették Ric Holt és tsai. Eredetileg a Motorola 6809 processzorra tervezték. A compiler első implementációját James Cordy vezette a Toronto Egyetemen. A maga idejében innovatívnak számított; a fordítót fejlesztő csapat 2 év alatt összesen 2.000.000$ költségvetéssel dolgozott, a Defense Advanced Research Projects Agency of the US DoD, és a Canadian Department of National Defence megbízásából. Pár évig használta is a I.P. Sharp Associates, Mitre Corporation, SRI International, és más, rendszerprogramozás és biztonságos szoftver-rendszerek témákkal foglalkozó nemzetközi kutató intézetek.
James R. (Jim) Cordy Számítástechnika-tudós és oktató Kanadából, érdemei között szerepel az első Euclid fordító, a TXL programozási nyelv, a Turing-nyelvcsalád, az SP/k, Concurrent Euclid és S/SL nyelvek fejlesztése.
Az Euclid nyelvet azért hozták létre, hogy ezzel megkönnyítsék a bizonyítható rendszerprogramok készítését. Az Euclid nem általános célú programozási nyelv, csupán kis programok számára tervezték. A bizonyíthatóság érdekében a felhasználónak fel kell adnia valamennyit a hatékonyságból, illetve el kell viselnie némi kényelmetlenséget a program írása alatt.
Az Euclid azt a fejlesztési elvet képviseli, melyben a helyes program létrehozásával és bizonyításával kapcsolatos legtöbb munka a programozó helyett a nyelvre, illetve a fordítóra hárul.
Az Euclid sokat felhasznál a Pascal nyelv jellemzőiből. A főbb különbségek a két nyelv között a következők:
- Láthatóság: az Euclid expliciten kezelhetővé teszi az azonósítók láthatóságát azáltal, hogy a programban minden rutin, vagy modul előtt megköveteli az importált vagy exportált azonosítók felsorolását.
- Változók: a nyelv biztosítja, hogy két azonosító ugyanabban a láthatósági körben nem hivatkozhat ugyanarra a változóra. Ha egy rutin hivatkozik egy változóra, vagy megváltoztatja azt, akkor annak elérhetőnek kell lenni minden olyan láthatósági körben, ahol a rutint meghívják.
- Mutatók: a dinamikus változók csoportosíthatók, és a nyelv biztosítja, hogy két különböző csoportbeli mutató nem hivatkozhat ugyanarra a változóra.
- Tárfoglalás: a program expliciten tudja kezelni a dinamikus változók tárfoglalását, olyan módon, hogy leszűkíti a tipushibák lehetőségét, sőt lehetővé teszi az olyan deklarációkat is, ahol a nyelv nyilvántartja a változóra való hivatkozások számát, és ha ez nulla, akkor felszabadítja a változót.
- Típusok: a típusok tartalmazhatnak formális paramétereket, így a tömböknek például olyan határaik is lehetnek, melyek csak a létrehozáskor konkretizálódnak, és a variáns rekordot típusbiztos módon lehet kezelni. A rekordok konstans komponenseket is tartalmazhatnak.
- Modulok: a modul egy újfajta rekord, amely tartalmazhat rutin, vagy típus komponenseket is, segítve ezzel a modularizációt. A modul tartalmazhat inicializáló és befejező utasításokat, amik minden alkalommal végrahajtódnak, amikor létrehozunk, illetve megszüntetünk egy modul változót.
- Konstansok: az Euclid úgy defíniál egy konstanst, mint egy literált, vagy mint egy olyan azonosítót, melynek értéke a deklaráció láthatósági körében konstans.
- FOR utasítás: generátort, mint modultípust lehet hozzá deklarálni, és a FOR utasításban az értékek felsorolására használni.
- "Kibúvók": lehetőség van arra, hogy az adott számítógép lehetőségeit kihasználjuk, illetve a típusellenőrzést kikerüljük ellenőrzött módon. Az explicit kibúvók kivételével az Euclid típusbiztos.
- Kijelentések, állítások: a szintaxis megengedi, hogy a program megfelelő pontjain állításokat helyezzünk el.
- Elhagyások: a Pascal több jellemzőjét elhagyták az Euclidból; például az input-output-ot, a valósokat, a többdimenziós tömböket, a címkéket, a goto-kat, és a függvények, eljárások paraméterként való átadását.
Sok egyéb szempont befolyásolta az Euclid tervezését: nem volt fő szempont a hordozhatóság, de a fordító azért több gépre képes kódot generálni. Ha elég hatékony a tárgykód, nincs szükség a fordító optimalizálására, ahhoz hogy hatékony kódot kapjunk. Kis programokra tervezték az Euclidot, ezért az egy részben való fordítás ajánlott.