• ultimate_worrier@lemmy.dbzer0.com
    link
    fedilink
    arrow-up
    154
    ·
    1 day ago

    I don’t make the rules…. but I have observed far too often for it to be coincidence that the more brilliant a type theorist is, the more likely it will be that they identify as 🏳️‍⚧️ or 🏳️‍🌈.

    • drolex@sopuli.xyz
      link
      fedilink
      arrow-up
      126
      ·
      1 day ago

      Counterpoint: I used to be a computer scientist in obscure languages, I’m as cis as they come, and I’ve always been absolutely average. Wait that’s not a counterpoint at all

      • degen@midwest.social
        link
        fedilink
        English
        arrow-up
        48
        ·
        1 day ago

        It’s kinda like set or category theory. The kind of math that hardly resembles anything at all yet somehow applies everywhere, to infinity and beyond

        • YTG123@sopuli.xyz
          link
          fedilink
          arrow-up
          2
          ·
          edit-2
          6 hours ago

          Indeed. [And caveat this whole comment with “as far as I understand” because this is maths and you can’t be too careful…] The difference being that set theory is way more fundamental and abstract than most mathematicians ever need, so on the one hand it can be completely stated with only 8 or 9 axioms (and a system of first-order logic) but on the other hand it can take some ingenuity to encode a mathematical object as a set in a way that makes it easy to do stuff correctly and hard to mess up.

          Most type theories take a more intuitive approach, so they do resemble something, namely, functional programming. Just a very rigorous approach to it. If you manage to construct a term of the correct type, you can be sure that it’s what you think it is, whereas with set theory you have to constantly check yourself (if you require the rigor). The trade-off being that type theory requires you to work with complete rigor and reasoning at a low level can be more difficult than set-theoretic reasoning at a low level.

          The TL;DR is that in type theory your constructions often look like what you actually want to do (and as a consequence you sometimes have to work directly with the underlying system, like a programming language), but in set theory there’s a disconnect between the conceptual level and the underlying nitty-gritty logic.

      • Jankatarch@lemmy.world
        link
        fedilink
        arrow-up
        17
        ·
        edit-2
        24 hours ago

        People who use templates and types to achieve absurd outcomes that just work, maybe?

        I have seen a few haskell magic.

    • bobo@lemmy.ml
      link
      fedilink
      arrow-up
      2
      ·
      21 hours ago

      What about Gödel, Frege, Cantor, and the other great philosophers-mathematicians of the 20th century?