4 ms·
“Want B” is not the same as “B”. “Should do A” is not the same as “A”. The reverse of “types prevent certain kinds of bugs” would be that “all code which does
by riwsky 4y ago
“Want B” is not the same as “B”.
“Should do A” is not the same as “A”.
The reverse of “types prevent certain kinds of bugs” would be that “all code which doesn’t suffer from those kinds of bugs is typed”, not “if you don’t want those bugs, use types”. The parent does not assume B->A; your actual disagreement with them is over whether A -> B implies A -is-the-most-effective-way-to—> B.
I share your understanding of the evidence base around types, and I agree with your conclusions; my beef here is just with divorcing the language of formal logic from its substance.
- jolux 4y agoYeah, though I do actually think “all code which doesn’t suffer from those kinds of bugs is typed” is true to a first approximation, for what it's worth. That's a big part of the reason I prefer static types. Under a few thousand lines it's less true. It's really at scale that these things become a problem, and even so they're still manageable most of the time, they're just kind of a pain.
- pron 4y agoFormalising natural language is tricky, but I believe "every PL that leads to more correct programs is typed" is either equivalent or stronger than "if you want a PL that leads to more correct programs it should be typed." It could be stronger if the latter phrasing takes measure into account (so a bit of fuzzy logic), meaning the possibility that other approaches also lead to more correct programs but not as well. Still, I contend that my formalisation is correct enough to demonstrate the logical error that even if types imply correctness (not substantiated by evidence), it does not follow that correctness implies types (even less supported by evidence).