But what you can prove at compile time is rarely useful. You can use phantom types, smart constructors, and the like, but after a while you need a runtime to do

But what you can prove at compile time is rarely useful. You can use phantom types, smart constructors, and the like, but after a while you need a runtime to do anything interesting. An example: this function is only valid on positive, odd integers in the range 3-91. With any static type system, this has to be a runtime check anyway. I’m not an expert on dependent types, but that sounds like what those try and solve. But at that point, you just want compile time to be a full program, which has all of the same pitfalls as the runtime of a program.