> But it is misleading, if not just a bit malicious, to claim I "vibe-coded" a language without knowing about a field I've spent a decade researching about.

Sorry. See the edit at the top if you haven't already. I didn't realise how much it came off as a critique of you rather than a particular approach to software engineering.

It's easy to write something and have a model of what you're writing in your head that is massively different from how someone else will read it without realising, not that that excuses it.

---

I disagree with LLMs manually writing proofs without other tools doing all the work they possibly can ever being a good solution for a couple of reasons:

1. Tokens are really expensive when we have a LLM spending hours hacking aware at a proof, not to mention generating those tokens is slow.

2. The context window becomes flooded with proof work rather than work on the original problem, which will lead to a worse solution. LLMs are demonstrably worse at writing code when you continue a session on a new task instead of starting a new one.

> It is my vision that a good proof language should be fully explicit, because this reduces proof-checking time significantly.

We can cache the results and help the checker along with assertions rather than throwing out all the smart parts of the checker.

I would encourage you to think more deeply about the assertions you're making here.

I've done a fair amount of work in this space as well, specifically my main toolbox of formal verification tools in the past have been Rocq, Idris, Dafny, and TLA+, and I can say that I've come away with roughly the same set of tradeoffs as what LightMachine describes in his comment.

Current formal verification tools are often very slow precisely because they try to reduce the number of lines of code that are required to write a proof. By making proofs more verbose and more explicit, proofchecking is sped up immensely (my own experiments check out with what LightMachine is saying here; indeed I've seen even greater speedups in the range of 100-1000x).

It makes far more sense to pay a series of one-time costs in LLM tokens that reduces your compilation time from 1 hour to 1 second than to pay the 1 hour compilation cost again and again (these are not exaggerated numbers for larger projects). This is especially true because with modern LLMs, it's usually just fire and forget and let it churn in the background than anything else.

Caching and incremental compilation has a lot of limitations, e.g. for CI. This is the promise that languages like GHC Haskell have promised for a while that always gets blown away by the other side like OCaml where global compilation is just so fast that you don't have to deal with those limitations.

1. LLM inference is cheap compared to the cost of a bug, and you can use tools to automate the proof-work, as you said so yourself.

2. Why would it? The AI shouldn't load already completed proofs, only their type signatures (which are one liners). Sounds like you're projecting bad context management?

Caching only works until you change a deeply nested constant. Then you must wait 2 hours as Lean re-checks every transitive dependency of a massive simp-ridden codebase. Also, first time check time IS relevant to UI. Nobody wants to wait 2h to start using a library after they first download it. Perhaps you don't mind that but I do; that's the kind of bad UX that made me go for that design choice on Bend. Which again, may be wrong or may be right. But it was intentional.

Having a checker that is just fast by construction, regardless of caching, was a top design priority, and I weighted it over verbosity in a layer I believe nobody will be reading anyway.

> 1. Tokens are really expensive

Just don't use frontier models by American labs. Chinese models are much cheaper and competent enough for most stuff

> 2. The context window becomes flooded with proof work rather than work on the original problem,

This can be solved by doing proofs in subagents. You can even have a tree of agents, for demanding proofs. They can share a database or otherwise have communication channels if some of them stumble upon something relevant for another agent

> Tokens are really expensive when we have a LLM

Expensive compared to what? Vs. human writing proofs they're definitely not.

> The context window becomes flooded with proof work

Context management is more art than science, but proofs are unusually good at compactation. Once proved, you can just keep the lemmas, you know,like humans do.

Moving the goalposts a bit here, aren’t you?

Clearly the author knows what he is doing, even if you think it isn’t a sensible approach.

It might still be true that LLMs make it too easy to create a broken design and don’t warn you if you ask for something already exists.

The thing is, the example you decided to pick on does not work.

You accused the author of having fallen into the ‘vibe-coding trap’. He clearly did not.

>Sorry. See the edit at the top if you haven't already.

Sorry about what? Getting caught? You entire post is based on a nasty lie about Victor and his work.