The closest I've seen is Idris, which lets you pass around data along with proofs about that data. The proofs can be generated at either runtime or compile time

The closest I've seen is Idris, which lets you pass around data along with proofs about that data. The proofs can be generated at either runtime or compile time (the usual distinction between the kinds of things you can do at runtime vs compile time is blurred in all sorts of delightful ways in Idris). The Idris Book (https://www.manning.com/books/type-driven-development-with-idris https://www.manning.com/books/type-driven-development-with-i...) is structured in a very practical, "learn some then build some" format that I found to be a joy to read.