Strongly typed
Research language
Originally developed for theorem proving systems
Solves the type problems of C and Pascal
