A big differentiator is whether one imagines an LLM in-band with most/all future software. If there is, and we’re deferring until very late parts of a program that world have been load bearing, and we’re able to programmatically ands reliably squint and say “eh i know what you meant” … then yeah formalizations seem superfluous-to-counterproductive.

OTOH if LLMs are to write, but not supplant, much of software, then boundaries, delegation to deterministic layers, good compilers to bonk miscreant models on the head with error message seem essential.

At one point it would have been shocking to assert that the compiler would live in-band with the program too. and yet JS eats the world. It seems shocking today that we could have a universal prior over the world operating in the ms/us nJ/pJ range required. And yet … ?