4 ms·

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