If you've internalized many of the interesting ideas of Haskell, check out Idris: https://www.idris-lang.org/ https://www.idris-lang.org/ It builds on the idea

If you've internalized many of the interesting ideas of Haskell, check out Idris: https://www.idris-lang.org/ https://www.idris-lang.org/ It builds on the ideas in Haskell (and similar languages) and adds proofs and first class types to the language. With it you can use the type checker to prove almost any invariant about your code that you care about. So the obvious stuff is there, prove that I never access an array out of bounds, sure. But also: prove that this code obeys this network protocol (e.g. never sends header before a successful handshake, never sends body before header has completed, etc). Ordinarily the best that you can do is expose an API that enforces these constraints, but nothing is checking that the internals of the implementation of that API uphold the constraints. With Idris you can move that into the type system, so that changes that would introduce a protocol violation fail at compile time. It's wild! And that's really only scratching the surface. It's still firmly in academia land, but the ideas present are fascinating and definitely worth puzzling through. The book is super good. It's well written, and introduces the ideas gradually but in a satisfying way: https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...