Comment by penteract

> dependent types and total functions do not scale.

I'm not convinced that this is much more true than the claim "correct code doesn't scale". If you add to your code in a way depends on a new property for correctness, and the code was not previously written with awareness that the new property was necessary, then you need to check through the rest of your code and make sure that the property is maintained. Formally verifying things is painful because it actually makes you check this.

Instead, we live in a world where we use software that is not completely correct. Browsers have remote code execution vulnerabilities because people who make browsers decided it's more important that javascript can run quickly, and that new standards get implemented, than that we avoid such vulnerabilities at all costs.