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+++
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 this is indeed the direction, but am wondering is anyone actually trying it right now? Love to explore it.
I think for now the answer to adaerlangsql+++ is just Rust - but its semantics have always been about human usability.
Humans have this thing where we can only keep 7 things at once and have to juggle our context, but recall seems much more broad than model contexts.
If we were to start designing a language and toolkit based around LLM context sizes, limitations and quirks - how would that look?
Also terseness and operators are one thing, but what if it’s the other way around - English words etc - can have a much bigger vocabulary of things that can be done but can easily be generated on the fly.
For a new LLM language realistically you would need to probably either write or convert a shit ton of software to it first if you are to train an adequate model on top of it …
And also what about “IDEs” for agents? So far they are clumsily using human tools - just looking Claude string along bash loops and greps to try to eek out meaning form code _it itself had written a week ago_ is frankly frustrating.
There must be a better way and some rich agent specific tooling for code exploration and verification.
Anthropic stance has always been “yeah we tested them all, grep is better” but I still am not convinced - just by the fact that it constantly fails one or two attempts before “figuring it out” yeah it’s fast anyway but it could be _faster_ and could allow the agent to “think” in code space more and not have to validate itself at every minute step …
I needed a chuckle and this delivered - “Typescript for SQL” gives me a mental image of a plane crashing into a train wreck.
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.
I’m generally cautious/sceptical about the current LLM hype, but if that did ever happen and it worked to a useful degree, it might truly be a significant advance. I’m not saying that just because of the LLMs themselves, though.
To reach that point, we would first need to overcome the classic problems in this area:
1. How can you specify the required behaviour for a system in precise detail without ending up with a specification language that is essentially another programming language with similar complexity to the ones we use today?
2. How do you solve the sufficiently smart compiler problem so that producing reasonably efficient and reliable implementations of those declarative specifications is not only viable but expected?
And then, if you still need someone (let’s call them a “developer”) to carefully specify the required behaviour of the system in detail, and you also know how to reliably generate a good implementation of a specification, how much value is left for LLMs to add in this picture?
Maybe LLMs really could be trained to reliably produce good implementations in that scenario? Never say never, but it seems more likely to me that we would develop deterministic algorithms for doing so. That’s already a very hard problem that a lot of smart people have explored, but if a solution could be found, most likely it would be strictly better than relying on LLMs in this part of the process.
Maybe there would still be a role for LLMs to convert natural language problem statements into specifications? Maybe for systems that don’t really matter, that would be enough and a big time saver. However, I’m sceptical about how much time it would be likely to save for systems that did need to work, where you would still need careful design and review of all the detailed specifications by developers anyway.
Maybe LLMs would end up in a similar role to the scaffolding tools that are popular in some ecosystems today, where you feed in some basic choices and the tool then produces a first pass at the files and code you might need, which you take as a starting point for the real work but without wasting so much time on boilerplate? That seems realistic and useful, but it’s a relatively small part of what would then be the overall development process.
In short, I would love for the existence of LLMs/agents to push us towards those better programming languages and tool chains, but if that did ever happen, I wonder how much benefit LLMs/agents could still offer once developers had the more powerful languages and tools available and could work at a “higher level of abstraction” themselves.
i dont even think that it would be possible to build a declarative language that is flexible enough to do what an imperative language is capable of without being an imperative language itself
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...
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.