Decades of research in machine learning have recently produced a very interesting, non-deterministic product: LLMs.
Their ability to interact with text-based environments has turned out to be the latest universal tool available to vast amounts of people.
Interestingly enough one of our most prominent layers in society can also be controlled via text - computers!
The last decades have produced a variety of approachable, text-based interfaces for instructing "the computer" - programming languages!
At the intersection of programming languages and the computer hardware sits the component performing the translation of programs specified in a programming language to the binary code that can be executed from the computer.
This component became the central component for verification in a new wave of software: Software that was generated by LLMs.
As it turns out compilers are not able to perform validation for us, meaning they can't determine if the seemingly correct program actually solves the problem that it was intended to solve.
Let's have a look at where LLM's sit in the Software Development Life-cycle and what we can infer from that with regards to tasks that Software Engineers have more time for now (aka. what the daily tasks will evolve into).

Verification vs Validation

Let's quickly clarify the difference between the two terms:

• verification: does the program do what it's supposed to do?
  Does the program adhere to the provided specification?
• validation: is that the program we need in the first place?
  Does it solve the problem of the users?

The biggest importance for the further reading is: Verification can performed by checking a program against a specification, meaning it can be performed by a machine. Validation can't. It's not encodable.

The LLM-infused Software Development Life-cycle

LLM's are used to produce code.
The current type of toolchains around them allow for the creation of automated flows where generated code is validated by trying to compile it.
So we can place LLM's at the 'Build' step in the SDL:

Zooming into the build step, we can find that LLM's actually perform a whole SDL inside it!
So called harnesses like Pi allow LLM's to:

• create a plan (to solve a given "task" via a prompt by the user)
• break it down into sub-tasks with validation criteria
• execute on the tasks (build)
• and perform a test/validation (to a certain extend) after completing all tasks

So - why is there even a human still in the loop?
Why not allow everyone to "one-shot" every software "thing" they can think of and just use that? Because it (sadly) doesn't work.
I for sure hope we get there.
I wouldn't love anything more than a software generator that produces perfect software.
But in reality LLM's work only within a certain scope and the final product still needs to convince us (the users/humans) that it's doing the right thing...reliably.

From coding to modeling

Previously writing code by hand gave you a degree of confidence about it's correctness.
Or at least you were aware if you even wrote it with the goal of making it correct/robust or just "work for a specific scenario".
This approach/practice is generally not applicable to generated code.
You only know about your generated code what you defined in tests, while trying to archive a 100% test coverage.
The fastest way to archive great tests is not writing them by hand, but derive them based on a logical representation of your system.
May I introduce the Quint Language!
With Quint you can model our system/program and test that model for correctness (trademark):

1. Modeling your software:
   In Quint you specify your system using types (data) and actions (data changes). The behavior of the system is then specified in a protocol which consists basically of a initializing the data and defining chains of actions that model what happens in the system.
2. Model testing:
   Now specify invariants, meaning assumptions that should hold true in every system state.
   Additionally you can also write tests that simulate specific scenarios.
3. Generate tests for the implementation:
   After verifying that your model is correct, you can generate tests for your actual code based on your model. This is one of the core features of Quint.
4. With the generated tests we can be stellar devs and follow TDD, but the lazy/modern version: have an LLM generate code that passes all the tests.
5. Done!

I am definitely a fan of Quint, but it's not the only tool that can be used to archive this model -> verify -> gen. tests -> gen. code workflow. But I deem it to be the most approachable one currently.

And there you have it. A program written by LLMs that you don't have to inspect but still can trust.

That's not the whole truth

Not all software engineering can be done that way. At least that's my guess for now. And that's fine.
I hope that we can all run fully owned models with the capabilities of the currently best "online-only" ones on our phones, which would maybe change that assumption again.
But LLMs definitely have their use, and it's worth trying to maximize the benefit's we can have from them. For now, let's all not try to put ourselves into boxes like "pro-AI" or "Human-only code". It's a tool. Know it, use it if you like, or don't. But knowing how to work with it is valuable.

Title: A smiling nod towards a slogan on the Quint homepage

Title picture: "The Red Horseman" by Roy Lichtenstein (1976)