Comment by tired-turtle

> Modern programming already is very, very far from strict obedience and formal symbolism

Difficult to sort this out with what follows.

Consider group theory. A group G is a set S with an operator * that supports an identity, closure, and an inverse. With that abstraction comes a hefty amount of power. In some sense, a group is akin to a trait on some type, much like how a class in Java can implement or extend Collection. (Consider how a ring ‘extends’ a group.)

I’d posit frameworks and libraries are no different in terms of formal symbolism from the math structure laid out above. Maybe the interfaces are fuzzy and the documentation is shoddy, but there’s still a contract we use to reason about the tool at hand.

> I’m not manually managing memory, parsing HTTP requests byte-by-byte

If I don’t reprove Peano’s work, then I’m not really doing math?