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.
AGI will accelerate it, but way before agentic development I learned this was the future when I worked at Amazon. I no longer have access to the internal talks about it (amazing to watch) but here is a public link worth reading:
https://aws.amazon.com/blogs/storage/how-automated-reasoning...
You don't really need compilers anymore. LLM's can write programs over any AST and provide an equivalence proof provided you have good semantics for the source and target.
What semantics do you mean here? What are bad semantics in an interpretation/compilation context?
Semantics of a language describe the behaviour of a sentence in that language when executed. When you have semantics in a theorem prover you can construct equivalence proofs between programs expressed in different languages (or proofs that a compiler from one language to another is semantics preserving).
I was mostly referring to accuracy when I said "good" above, in the sense that they should reflect the actual behaviour of the language they describe.
Then we don't really need software anymore, LLMs can just receive every user input and perform the action required.
/s
Also you would probably want to cache the compiler's output in git because running that compiler would take a long time, and you probably want the compiler's output to still be inspectable to human inspection. In the end that compiled artifact would look a lot like source code.
I think Rust's success in the AI space shows how useful formal proofs are, as Rust provides something very similar to that. Both because it helps with the understanding of LLMs, as well as with trusting the LLMs are not violating any basic properties (like please no nasal demons if the user sends a buffer larger than the allowed amount).
> formal proofs are, as Rust provides something very similar to that
Since when? Rust just has an ML-like type system, and seemingly many have met that for the first time with Rust, even though it has decadeS of history, and multiple production languages running it just fine (ocaml, scala, etc).
Formal proofs are way way above an ML type system. Like how do you encode mathematical statements in Rust's type system? What about statements about program semantics, like program A is equivalent to program B <- in formal verification THAt is the type of an expression, and the implementation of it is the proof.
``` SELECT A, B, Sum(C) FROM Somewhere GROUP BY ALL ```
Very few developers look at the underlying “source code” that this SQL compiles into. Very few people even read the “source code” that tsc outputs.
The reality is the lowest level checkpoint worth looking at and understanding is the highest possible abstraction layer which preserves 100% of the needed precision and flexibility that the product being built requires.
Also, you’d just use something like sscache or just .o files to speed up compilation. It’d be unusual to store compiler MIR/LIR in git.
I think the important part will be figuring out what we need from the higher level language that achieves 100% of the precision and flexibility of Rust for the product being built.
We've got inform7 with an English like language generating complex inform6 OOP optimized code since a few decades and the i7 compiler might even run under a Pentium II with 128MB of RAM under NetBSD. I6, under 32 and a Pentium. And maybe even less. ZMachine games themselves (the biggest v8 ones) under the Frotz interpreter, under a 486 and 8MB (with FreeDOS and Frotz). Or maybe an Amiga or a m68k Mac with the same amount of RAM.
Now imagine what AMD64 machine can do with 2GB of RAM (minimum baseline for legacy, maybe some C2D computer) today.
inform7 is closer to a dsl than a general purpose language. We might be looking at something closer to spark/ada.
Check Inform7 for text adevntures. No AGI nor AI needed. On Inform6, it's a dumb simple OOP language where the structure it's almost self-evident. Classes, in-game objects with real-life attributes (enterable, a container for other objects, non-movable/pickable scenery and so on).
PD: inform7 can run on an RaspPi B+ or 25 year old PC's like nothing, and i6 down to 30 year old ones. The ZMachine adventures themselves, from any 16 bit computer and up.
[dead]
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've enjoyed embedding declarative syntax inside imperative languages, like LINQ and prolog as a dsl. The imperative code can express temporality much easier, and the declarative code allows you to throw that away when you don't want it.
Coming at it from another angle, we have historically made distributed systems manageable / 'verifiable' with RTOSs which give deterministic scheduling and locking primitives. We know that a task's max duration is its uninterrupted duration + max duration of all higher priority tasks which could pre-empt it, and so on. Deterministic pre-emptive scheduling and locking alone could be enough to prove a lot of invariants without full temporal logic, and writing code in 'RTOS logic' might be more natural for humans/LLMs than the more expressive and powerful alternatives.
I needed a chuckle and this delivered - “Typescript for SQL” gives me a mental image of a plane crashing into a train wreck.
Yes, that was the vision of 4 GLs and Japan's Fifth Generation Computer project.
However just like the uptake in SaaS, iPaaS, serverless, managed cloud environments, this means way smaller teams will be needed, and everyone that doesn't get to press buttons at the software factory, will need to find another occupation.
> I think somewhat of the opposite will actually occur. LLMs won’t formally verify LLM generated imperative style code.
This result is exactly the opposite. They're verifying at the machine code level, which is totally imperative.
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 …
Yes, plenty of people are.
That is what low code/no code enterprise tools have pivoted to.
Check Boomi, Workato, Optimizely Opal, Sitecore AI, PowerPlatform.
This is why you see my comments regarding the way AI based coding is going to, I have already tasted the future in such tools, and even if they have issues today, they will eventually be ironed out.
Rust is great! No two ways about it.
What I want tho would be Rust+Akka for example. There has to be a distributed execution mechanism that is as seamless as Java’s GC. Then the distributed execution mechanism needs to evolve to also be as light weight and “zero cost” while being seamless like Rust’s compile time memory management.
Where's the stance that "we tested them all", any links?
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.
These are the good good questions. I wish I was smart enough to answer them.
I think the best bet is to let a hundred developers play at it for a bit. There will be a lot of bespoke domain specific declarative languages. They will over time learn from each other to be better and better.
Experiments like GoogleSql’s pipe syntax https://docs.cloud.google.com/bigtable/docs/reference/sql/pi... getting pushed even further and further. That’s where I’d put my money. Cloudflare might be another candidate for building such a programming language for the distributed compute and memory “machine”.
(Also once we are there) I think there will be even better questions: What does programming CRDTs like a blockchain that reconcile across Mars and Earth look like? and in that way, LLMs will constantly be useful helpers to explore the state/latent space.
See tools like https://boomi.com/platform/agentstudio
Granted this isn't usable for all kinds of problems, however plenty of enterprise CRUD software can be easily tackled with such agentic runtimes.
Buzzword salad, yummy
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.
They will skip the generating Rust code part, from my point of view.
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
We don’t need “a declarative language flexible enough to do what an imperative language is capable of”
We need “a declarative language flexible enough to do what the product requires”
[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...