4 ms·
> so loses the "if it compiles there's a good chance it's correct" property that people want from statically typed languages. If that's what people actually wa
by 9rx 2y ago
> so loses the "if it compiles there's a good chance it's correct" property that people want from statically typed languages.
If that's what people actually wanted, Coq and friends would be household names, not the obscure oddities that they are. All the languages that people actually use on any kind of regular basis require you to write tests in order to gain that sense of correctness, which also ends up validating type-correctness as a natural byproduct.
"A machine can help me refactor my code" is the property that most attracts people to the statically typed languages that are normally used. With "I can write posts about it on the internet" being the secondary property of interest.
- gwd 2y agoIt's a spectrum, with costs and benefits at each level. I lock my front door even though I don't have bars on my windows; I prefer Golang, where doing a basic compile will catch a fair number of errors and testing will catch the rest, to Python or Perl where testing is the only way to catch errors.
- 9rx 2y ago> where doing a basic compile will catch a fair number of errors In the case of refactoring this is incredibly useful. It doesn't say much about the correctness of your program, though.