[lifthrasiir]

> Strong type systems can give provably correct code.

"Sound" [1] type systems only guarantee the absence of some class of bugs as well. There are a lot of bug classes that remain exploitable. Memory safety happens to be a low-hanging fruit because many existing softwares are not even written in such languages.

[1] "Strong" type systems generally refer to the intolerance towards implicit type conversions or memory unsafety, and that alone doesn't make type systems provably safe in some sense.

[anyfoo]

I did not claim that everything about the code was proven correct, but a subset of properties expressable by the type system.

I agree that using the word “strong” was wrong. I basically meant it in the sense of “good”/“elaborate”, mistakenly ignoring that “strong” already has a very specific meaning in type systems. Thanks for correcting.

[robertlagrant]

> Strong type systems can give provably correct code

^ I think this is where you seemed to claim that everything about the code was proven correct.