Ask HN: Which languages have the most compile-time checks?

You should check ML programming languages family, like Ocaml.

Agda. It halts.

Ada would probably be put in a similar box with those.

For some more possibilities, see:

https://en.wikipedia.org/wiki/Category:Statically_typed_prog...

Right, but I'm curious to know among statically typed languages, which ones have more checks than others.

Still probably Ada. Compared to other statically typed languages, Ada is a "big" language. Things like Modula-2 or ML simply have far fewer things to check.