3 ms·
You're making a very strong statement, so we might as well look at extreme cases, namely the formally verified middle-end of CompCert: https://users.cs.utah.edu
by miloignis 3y ago
You're making a very strong statement, so we might as well look at extreme cases, namely the formally verified middle-end of CompCert: https://users.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf https://users.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf
I believe this would count as empirical evidence of very strong static typing reducing bugs.
I think this points to what many other comments have been getting at, which is that typing is not a binary yes/no question, but a large, multi-axis (static/dynamic, strong/weak) spectrum with lots difference between type systems, as well as big differences in how people apply those type systems to their problem. You could still work in a static, strongly typed language and represent everything as strings, converting back and forth as necessary, but that's essentially working in a dynamically typed language. You could also take advantage of the tools the type system gives you in order to reap the benefits, creating classes representing the legal values and asserting important invariants.