The Lean Language #
A functional language and theorem prover that is used in the Mechanics of Proof course.
It has been suggested that formal proofs or specifications are going to be more important if we want to take advantage of AI generated code.