The problem you're running into is that people who have some "mathematical maturity" don't get bogged down in notation, so it's difficult for them to see the distinction you're trying to draw between e.g. `{ x∈S | x.id = 1}` and `select x from S where x.id = 1`[0]. You say "a SQL query is a SQL query" and they just think "yes, which is also obviously a mathematical expression".

Computer programs are proofs[1]. This is intuitively and also formally true. You would agree writing proofs is doing math, yeah? Then obviously writing a computer program is also doing math.

Like I have a degree in math and have been a software engineer for over a decade. I do not know what distinction people are trying to get at. It's like trying to argue about the distinction between U(1), the complex numbers with magnitude 1, and the unit circle, and getting upset when the mathematicians say "those are 3 names for the same thing". Or saying that writing C is programming but writing in a functional language like Scala or Haskell (or Lean) is not.

[0] Modulo details like NULLs and multi-set semantics, but surely that's not the distinction?

[1] Up to isomorphism

A better analogy is if someone got upset that someone else said "the set of natural numbers is the set of real numbers." One is a subset of course, and when that is highlighted, the response is "yeah, by 'is', I actually mean subset", therefore indeed: the set of natural numbers is the set of real numbers.

This is an interesting example: "Or saying that writing C is programming but writing in a functional language like Scala or Haskell (or Lean) is not."

The first part is everything we need to look at. Are we saying that writing C is equivalent and equal to the entirety of all programming? That if you're programming then you are writing C code. No, there is an implied "is a form of" in there. Given the other clarifications and that so many people are claiming to be mathematicians, I would have expected the precision to say exactly "C is a form of programming" rather than "C is programming."

Turns out, the analogy of saying "the set of reals is the set of naturals" is more fitting compared to sets that are actually equal.

Code is logical in nature and is defined by mathematics.

I'd agree code is usually governed by mathematics, not defined by it though.

Goes back to this ridiculous proposition:

- Cashier: You mean, I used math to give you change?

- Customer: No, giving change doesn't use math, it IS math!!!!" [2]

The proposition is that "code IS math", not defined by, not uses, not inspired by, not relies on, not modeled after, but IS.