Can lisps place arbitrary code in types and formally verify complex properties of stateful systems--all in the same language? Doubt it. Lisp isn't the epitome of power.
Lisp is usually an academic language, which means research into type systems and type safety frequently takes place in it.
ACL2 is a theorum prover written in Common Lisp [0]. And not just a random project either, but something AMD, ARM, IBM, etc. have used.
> Lisp isn't the epitome of power.
Lisp is the epitome of simplicity. If the foundations based on simplicity you can do very powerful things.
And of course, Lisps that include meta-object protocols (Flavours, Common Lisp again, &c.) deliver power, very elegantly, but for people unfamiliar with them, there is a learning curve to climb.
That is exactly the reason why Scheme was chosen for SICP.
“Lisp dialects strive for elegance.”
Elegance is not always synonymous with simplicity. For example, Smalltalk’s use of Class and Metaclass is very elegant, but most programmers encountering this for the first time would not call it “simple.”
After they got over the hump and grok how the two things work together to serve as the foundation for Smalltalk’s OOP and allow programmers to alter Smalltalk’s OOP... Then the elegance emerges.
I think elegance is a measure of the simplicity of a tool relative to the complexity of the problem domain, whereas simplicity feels like a more absolute measure.
This is the Lisp I manual:
http://bitsavers.org/pdf/mit/rle_lisp/LISP_I_Programmers_Man...