I still think it is (in the source-code generating mode) a compiler, just like LiquidHaskell is. (I haven't used LH but it essentially can automatically supply functions based on the type conditions you specify.)

In my view, reasoning LLMs have learned a large number of close to true sentences of "logic" in natural language. These rules are not consistent (unlike typing rules of LH that allow creation of provably correct programs), but they work in practice better than LH. Essentially, they represent an unsound formal specification of natural language, together with many useful (almost)tautologies that helps solving constraint problems (just like LH does, but again unlike LLM, provably correctly).

LLMs proved that human language can be formalized reasonably close to soundness. I believe we can have a sound formalization of human language, and that kind of formal language will be once superior to LLMs.

It will also not be as complicated as LLMs and require only fraction of compute to use.