"Lean" sounds awesome.
You can only write programs that will halt in it.
This is a common property for proof-oriented languages. Coq shares this property for instance, and you can write an optimizing C compiler in Coq: https://github.com/AbsInt/CompCert .