What do you mean? It's a nice and simple language. Way easier to get started than OCaml or Haskell for example. And LLMs write programs in Lean4 with ease as well. Only issue is that there are not as many libraries (for software, for math proofs there is plenty).
But for example I worked with Claude Code and implemented a shell + most of unix coreutils in like a couple of hours. Claude did some simple proofs as well, but that part is obvs harder. But when the program is already in Lean4, you can start moving up the verification ladder up piece by piece.
Well, if you do not need to care about performance everything can be extremely simple indeed. Let me show you some data structure in coq/rocq while switching off notations and diplaying low level content.
In Lean, strings are packed arrays of bytes, encoded as UTF-8. Lean is very careful about performance; after all, a self-hosted system that can't generate fast code would not scale.
You know you could just define the verified specs in lean and if performance is a problem, use the lean spec to extract an interface and tests for a more performant language like rust. You could at least in theory use Lean as an orchestrator of verified interfaces.
You could have a multi agent harness that constraints each agent role with only the needed capabilities. If the agent reads untrusted input, it can only run read only tools and communicate to to use. Or maybe have all the code running goin on a sandbox, and then if needed, user can make the important decision of effecting the real world.
A system that tracks the integrity of each agent and knows as soon as it is tainted seems the right approach.
With forking of LLM state you can maintain multiple states with different levels of trust and you can choose which leg gets removed depending on what task needs to be accomplished. I see it like a tree - always maintaining an untainted "trunk" that shoots of branches to do operations. Tainted branches are constrained to strict schemas for outputs, focused actions and limited tool sets.
reply