The goal is to produce a program with as few serious bugs as possible, as cheaply as possible. It is never a goal to use a programming language with certain properties; that could just be a means to that end.
> The more bugs I can statically guarantee are absent the better!
Only provided that those guarantees don't come at a cost that could make finding the bugs you don't statically eliminate harder. How could it make it harder? By making the language overall harder to understand -- both by informal and formal analysis -- making safe evolution more tricky, and by slowing down compilation, which slows down the testing cycle and reducing the number of tests you write.
Correctness is a very complex subject, and that "the more sound guarantees the better" is not a consensus opinion on how to get there. For example, even in formal verification circles, a lot of current research focuses on reducing soundness (e.g. concolic testing vs. model-checking/deductive proofs). It's like the question of how to catch more fish: is a smaller net with small holes that guarantees no fish can get through it better, or is it better to cast a wider net with larger holes, that might let some fish slip through but covers a wider area?
Perhaps in the case of the net and the fish an answer could be given ahead of time if you know everything there is to know about the distribution of the fish size and their dispersion, but that's not the case with software bugs. We simply don't know enough, and the only way to answer the question is through empirical observation, over a wide range of applications and over a long time. It's also possible that both approaches are equally good at achieving correctness, and then it's just a matter of personal preference based on other aspects of the language.
The goal is to produce a program with as few serious bugs as possible, as cheaply as possible. It is never a goal to use a programming language with certain properties; that could just be a means to that end.
> The more bugs I can statically guarantee are absent the better!
Only provided that those guarantees don't come at a cost that could make finding the bugs you don't statically eliminate harder. How could it make it harder? By making the language overall harder to understand -- both by informal and formal analysis -- making safe evolution more tricky, and by slowing down compilation, which slows down the testing cycle and reducing the number of tests you write.
Correctness is a very complex subject, and that "the more sound guarantees the better" is not a consensus opinion on how to get there. For example, even in formal verification circles, a lot of current research focuses on reducing soundness (e.g. concolic testing vs. model-checking/deductive proofs). It's like the question of how to catch more fish: is a smaller net with small holes that guarantees no fish can get through it better, or is it better to cast a wider net with larger holes, that might let some fish slip through but covers a wider area?
Perhaps in the case of the net and the fish an answer could be given ahead of time if you know everything there is to know about the distribution of the fish size and their dispersion, but that's not the case with software bugs. We simply don't know enough, and the only way to answer the question is through empirical observation, over a wide range of applications and over a long time. It's also possible that both approaches are equally good at achieving correctness, and then it's just a matter of personal preference based on other aspects of the language.