[jnash]

Have you tried Idris? It is a "practical" programming language that also gives you the full power of Dependent Types to prove your code correct. There is a great book "Type-Driven Development with Idris" that really helped me open my mind to the power of Dependent Types.

[schoen]

Yes, I'm borrowing that specific book from a friend who is really into functional programming, but I haven't read it.

It does look like Idris helps make it especially straightforward to write correct code and know when you've done so.