alt Hacker NewsModern programming already is very, very far from strict obedience and formal symbolism. Most programmers these days (myself included!) are using libraries, frameworks, and other features that mean what they are doing in practice is wielding sky-high abstractions, gluing things together they do not (and can not) fully understand the inner workings of.
If I create a website with Node.js, I’m not manually managing memory, parsing HTTP requests byte-by-byte, or even attempting to fully grasp the event loop’s nuances. I’m orchestrating layers of code written by others, trusting that these black boxes will behave as advertised according to my best, but deeply incomplete, understanding of them.
I'm not sure what this means for LLMs programming, but I already feel separated from the case Dijkstra lays out.
> 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?