If by "correctness" you mean what I call "small-c correctness" ("this reference won't be null", "this function call doesn't write to the database") then Haskell

If by "correctness" you mean what I call "small-c correctness" ("this reference won't be null", "this function call doesn't write to the database") then Haskell is currently best-in-class. If by correctness you mean what I call "big-V Verification" then the sibling answer[1] is better for you. [1] https://news.ycombinator.com/item?id=22464576 https://news.ycombinator.com/item?id=22464576