I think somewhat of the opposite will actually occur. LLMs won’t formally verify LLM generated imperative style code. We (including agentic development) will move on from imperative languages, skipping functional and move to deterministic declarative languages.

Likely, a proliferation of experimental languages all somewhat akin to Typescript for SQL with significantly more nuanced operators to tersely capture the same outcomes as imperative languages.

They’ll compile down to be able to run performantly for game development or even for the Linux kernel (as if Linus would ever agree lol) but also they’ll be able to run on distributed execution engines with effectively a shared memory space, etc.

Allows for significantly more terse artifacts. Lower chance of hallucination, fewer output tokens, fewer thinking loop iterations and concise enough for humans to review (for domains that need it).

On top of that, additional theorem like syntax to drastically limit the ability of functions, etc. likely some sort of higher level effect system for verification. Used for many things like “constant time compilation for crypto functions”, and also “ensure acid compliance” for writes and reads in a local context, and things like “ensure only once delivery” for functions on a distributed execution engine.

At which point every program will be formally verified by default. You could think of it as AdaErlangSQL+++

What you're describing is a language that can effectively take a high-level design doc (limited to a formal language representing a pseudo-English-subset) and compile to almost arbitrarily complex, formally verifiable systems. I say systems because you're also implying these could essentially orchestrate distributed systems.

Which, if that were really possible, would be pretty good evidence of AGI. Or, at least, the end of 6-7 figure software engineer salaries. Conversely, I think it's a pipe dream. Writing a compiler that actually works well across such a broad range of hugely complex behaviors would itself be absurdly complex.

Depends really. I tried some experiments towards a pretty uniform relational language for expressing ordinary logic, temporal logic, requirements etc. It does work, but there's some unexpected obstacles.

You'd think performance would be easy to achieve because you'd just write clear, high-level declarative facts and LLM + good optimiser + proof certification system will get you there in terms of performance. But you'll be surprised that relational/declarative specification gives you so much behaviour 'for free' that choosing what to actually compute from those relations is a very deliberate choice. It starts to look like finding an imperative-like path of demand through the relations. It seems that you get exactly the same problems but one level up.

I think it won't happen because people just care to much for performance. You already see this now. You see a ton of rewrites moving to rust even from higher level languages.

So Inform7 like languages generating Rust code and then binary code and linked against the OS.

[dead]

> They’ll compile down to be able to run performantly for game development or even for the Linux kernel (as if Linus would ever agree lol) but also they’ll be able to run on distributed execution engines with effectively a shared memory space, etc.

Linus doesn't have to care, MirageOS already exists for OCaml, and I'm pretty sure there's something like MirageOS for Rust...