If you pair LLMs/AIs like Claude with a formal verification framework you essentially have a new sort of compiler.

That’s technically correct, but it still means that someone has to write the formal specs that Claude’s output is verified against, and someone has to design the formal languages the specs are written in. And once you have formal specs that truly covers all aspects that you ever will care about, it’s unclear if you couldn’t instead build a non-LLM mechanism that efficiently and deterministically spits out an implementation of such a spec.

▲

kettlecorn 4 hours ago | parent [-]

I expect in the future it will become hybrid. Formal specs provide guardrails for LLMs / AI but within those guards LLMs will author traditional compiler programs and at times drop-down to manually compile / prove certain snippets.

Could we describe the first humans manually writing Assembly and their own higher level abstractions as "compilers"? Loosely I think we could, and LLMs fit the same mold.

	▲	layer8 4 hours ago \| parent [-]
		I disagree in the sense that source code (compiler input) leaves little space as to the behavior of the resulting program. With LLMs, either there is much more implied leeway, in which case I’d argue that it’s different in nature. Or the specs will restrict the LLM output to a similar extent as a conventional programming language restricts a compiler’s freedoms, in which case it’s not clear that LLMs are the most expedient technology for generating that output. Levels of abstraction actually matter with regard to how much observable behavior they leave unspecified, and with regard to how much control is needed over each respective behavioral aspect.