• barsoap
    link
    fedilink
    arrow-up
    1
    ·
    1 year ago

    because all of those results are trivially translatable between them.

    Then go ahead, reformulate everything in CoC or HoTT or similar. I’m waiting. Prove it trivial, prove that what you did is actually consistent.

    • Kogasa@programming.dev
      link
      fedilink
      arrow-up
      1
      ·
      1 year ago

      Hence why what you’re saying is stupid. You might as well say “all computer science should be done in binary.” What you’re saying is completely unreasonable and has no bearing on actual mathematics.

      • barsoap
        link
        fedilink
        arrow-up
        1
        ·
        1 year ago

        Are you saying that the proofs of the four colour theorem aren’t proofs, aren’t mathematics, or something to that effect?

        And no, working in Coq (as Gonthier did) is quite different from punching holes into cardstock. CS loves abstraction, all those Type Theory based systems basically look like functional programming languages and are just as ergonomic. Because they are functional programming languages (with fancy-pants type systems).

        And by denying those systems you then are also denying the value of category theory because there’s some rather strong isomorphisms between those systems. Are you sure you want to throw all that maths out of the window just to be salty on the internet?

        • Kogasa@programming.dev
          link
          fedilink
          arrow-up
          1
          ·
          1 year ago

          Are you saying that the proofs of the four colour theorem aren’t proofs, aren’t mathematics, or something to that effect?

          No, and I can’t see how a reasonable person would think I’m saying anything like that.

          And no, working in Coq (as Gonthier did) is quite different from punching holes into cardstock.

          I didn’t say anything to that effect whatsoever.

          CS loves abstraction, all those Type Theory based systems basically look like functional programming languages and are just as ergonomic. Because they are functional programming languages (with fancy-pants type systems). And by denying those systems you then are also denying the value of category theory because there’s some rather strong isomorphisms between those systems. Are you sure you want to throw all that maths out of the window just to be salty on the internet?

          Who are you talking to? What is this fucking insanity?

          • barsoap
            link
            fedilink
            arrow-up
            1
            ·
            edit-2
            1 year ago

            No, and I can’t see how a reasonable person would think I’m saying anything like that.

            So now you do consider working in CoC to be a reasonable way to do maths. Thus, we have a contradiction. Thus, you make no sense. QED.

            I didn’t say anything to that effect whatsoever.

            You said “in binary”. Peolpe haven’t done that since the days of hand-punching things into cardstock. Which is, precisely, working in binary. Don’t ask me whether a hole is a 0 or 1 I’m not from that era.

            • Kogasa@programming.dev
              link
              fedilink
              arrow-up
              1
              ·
              1 year ago

              So now you do consider working in CoC to be a reasonable way to do maths. Thus, we have a contradiction. Thus, you make no sense. QED.

              I never said otherwise you literal lunatic. I said it would be completely unreasonable to “just rewrite the whole thing in rust CoC.” The vast majority of all math has literally nothing to do with nitpicky foundations issues.

              You said “in binary”. Peolpe haven’t done that since the days of hand-punching things into cardstock. Which is, precisely, working in binary. Don’t ask me whether a hole is a 0 or 1 I’m not from that era.

              I can’t have this conversation with someone who can’t read.

              • barsoap
                link
                fedilink
                arrow-up
                1
                ·
                1 year ago

                The vast majority of all math has literally nothing to do with nitpicky foundations issues.

                The whole of maths is built on it. The validity of everything hinges on the foundations. I’d even say that the beauty of everything depends on it but formalists are so caught up in their world that they don’t even bother to look at constructive maths. The vast majority of maths already has been rewritten in constructive terms. It enabled proofs that were previously impossible.

                Now your area of maths might be so arcane and special and everything that nothing whatsoever from the constructive side could ever amount anything but, frankly speaking, I fucking doubt it because you seem to be largely ignorant about the whole topic. For one, doing constructive maths doesn’t mean a pre-occupation with “nitpicky foundation issues”. Those foundations have been laid ages ago, it’s been high-falutin from then on.

                Have you watched that video I linked?