I understood the other poster correctly. This view of mathematics is as limiting and ignorant as the other poster’s.
The entire field of theoretical computer science, to which functional programming and type theory is closely tied, is a branch of mathematics. The Church-Turing thesis which gives both to our field equates the two at a very fundamental level. Questions about type theory, programming language design, and programmer ergonomics are fundamentally about math and applied math.
Maybe you and the other poster have in mind specific fields of math, but then you need to make claims for why those fields are sufficiently different as to be exempt from applicability of any of the advances in notation observed in other fields.
Your implicit assumption that you can divide computer science into a different bucket from “real math” is incorrect, and gatekeeping.
As I said though, I don’t think this is a profitable debate to have here on HN.
The entire field of theoretical computer science, to which functional programming and type theory is closely tied, is a branch of mathematics. The Church-Turing thesis which gives both to our field equates the two at a very fundamental level. Questions about type theory, programming language design, and programmer ergonomics are fundamentally about math and applied math.
Maybe you and the other poster have in mind specific fields of math, but then you need to make claims for why those fields are sufficiently different as to be exempt from applicability of any of the advances in notation observed in other fields.
Your implicit assumption that you can divide computer science into a different bucket from “real math” is incorrect, and gatekeeping.
As I said though, I don’t think this is a profitable debate to have here on HN.