Comment by dmitriid

I sometimes phrase it as “yeah, your program is correct because it’s type-checked, but who has checked that your types are correct”?

With dependent types some of the logic will be coded in types, and we would need to check those.