3 ms·

Type systems aren't magic. They do stop all incorrect programs from running, but also the majority of correct programs too.

• anon291 9mo ago
  Luckily most everyday programs are typeable.
  • noosphr 9mo ago
    And you don't need cut in logic either: https://philpapers.org/rec/BOODEC https://philpapers.org/rec/BOODEC It's just that your typeable program might take more data to store than there are bits in the universe. I'm not saying that types are bad. They aren't. I'm saying they aren't magic and they come with a trade off.
    • lmm 9mo ago
      Types are the closest thing to a free lunch that exists in this fallen world. Yes they're not perfect because nothing is, but their cost/benefit is astonishingly good.
      • noosphr 9mo ago
        A shoe five sizes too small is very comfortable for someone who cut off his toes.
        • lmm 9mo ago
          It would be a mistake to conclude that this means shoes are pointless or there's no such thing as a shoe that fits well.
          • noosphr 9mo ago
            Indeed, there are other invariants to type systems that are much better than cutting off your toes.
      • antonvs 9mo ago
        > Types are the closest thing to a free lunch that exists in this fallen world. Chef's kiss
• rerdavies 9mo ago
  ... for some spectactularly inconsistent and arbitrary definition of "correct program".
  • noosphr 9mo ago
    Yes, like giving the correct result for every possible input.
    • rerdavies 9mo ago
      Not really sure that a type system is going to guarantee that your program generates the correct result for every possible input.