Beyond Code, toward proof first
I like to say "coding is dead". We are now in the era where agentic workflows matter far more than code. So in this post I'll discuss what it means to think "beyond code", and address the topic of agentic workflows.
The basic workflow that most people use when using AI, is to go to ChatGPT, prompt the chatbot, and perhaps learn prompt engineering skills. This is not generally a form of "agentic coding", this is essentially vibe coding. The novice tells the Chatbot "build cool app" and in one shot, the Chatbot builds an app. This typically results in AI slop, the code quality is usually low because the prompt simply was "build cool app" or some variation of that. Why is this a problem? From a cybersecurity perspective, the app is most likely to have bugs, from a UX perspective, the app may look like it works, but then under the hood the app has placeholder code, TODO, no error handling, etc. Unfortunately, vibe coding has caught on, and the easy way has become the standard way.
I'm not here to discuss the standard way of doing things. The agentic workflows I'm introducing are not vibe coding. In fact, this workflow will require thinking about software in an entirely different way than even most software developers with decades of experience think about software. The word to start with, is abstraction, and the phrase is "abstraction as a super power". The difference between vibe coder and agentic engineer, are that the vibe coder is a prompt engineer, they know how to prompt, but they don't understand the deep concepts behind software. For example, when you think about what the LLM actually does, it's an abstraction layer, it's not AGI, it's predicting the next token, it's primary abilities are pattern matching, search, translation, and with this tool you can go to a very high level of abstraction above the code level.
From abstraction, to loop engineering
You can think about software as state machines for example. When you do this, you abstract away the unnecessary parts and keep the vital parts. This allows you to map out the software and every behavior. You can think use the LLM to search for disaster states, states which you want to be unreachable. How do you do this? You have to go beyond prompt engineering, and begin loop engineering, and the loop that enables this is the neuro symbolic loop. You connect the LLM to a formal checker, a proof assistant, and you treat the LLM as a proposer. The loop is propose, check, refine.
This is basically abstracting the LLM itself into a component in the toolchain of your loop. By doing this, the code isn't the problem anymore. The programs become math formulas, proofs, state machines, and you can very exactly talk about the behavior of these programs in this form. You can't talk about software in code in this way because code is too ambiguous, too many lines, at too low level of abstraction. You can however speak in math, those formulas are not ambiguous, high level of abstraction, and the best part of all, you can prove the behavior of the math without having to know anything about the code. That's where things are today with software, and in the ideal world we would have a lot more high assurance software because of AI. In the actual world, we have a lot more software, but it also means more bug surface.
In future posts, I will go into some of the techniques, and the tools like Lean, Z3, Aristotle, etc.