bilíngue · en / pt
o manifesto do bend2
Linguagens e compiladores#Bend#provasBend2 shipped this week (two days ago, as I write this), and I want to defend the idea behind it before the discussion turns into a benchmark fight.
Scope warning: I have not run Bend2. I have not installed it, have not written a line of it, and have no opinion on its ergonomics. What I have is an opinion on the bet, and I think the bet is right.
what broke
Over the last two years the amount of code I read grew past the amount of code I write. That is not a complaint, it is just what the job looks like now.
And that is where a problem nobody has solved shows up: human review measures whether code looks right. That is literally the job. Read, understand the intent, look for the case the author forgot, and approve when nothing turns up.
Except "looking right" is exactly what a model trained on human code does better than anyone. It produces the most plausible code it can. Plausible is the metric it optimizes for, and plausible is the metric my review applies. Both point at the same target, and the bug lives in the blind spot they share.
I have already written here about four things I broke in production. None of them failed on bad math. They failed on seams: a constant that never reached the function, one scope keyword, a check run in the wrong order. All of them passed review. All of them looked right.
Tests do not fix this either, for a harder reason: a test shows a bug exists, never that it does not. You sample the space of inputs and hope you sampled the case that matters.
Scaling AI with a sampling guarantee is a bet that does not add up.
the inversion
What Bend2 proposes is to stop trying to fix review and change the artifact the human maintains instead.
Instead of you writing the code with the machine helping, you write the law, and the machine writes the code and the proof that the code obeys the law. The law lives in the repository, in a file called LAWS.bend, and it is the thing you read, version, and argue about in a pull request.
law you_cant_win:
for moves: List<Game.Move>
board = Game.replay(Game.start(), moves)
{Game.is_won(board) == False{} : Bool}
That reads as: for any sequence of moves, replaying them from the starting state never results in a won board. It is not a test case. It is a claim about every possible sequence, including the ones you never thought of.
The implementation becomes output. The proof becomes output. What you keep is the claim.
The project's slogan is that merging a bug becomes mathematically impossible, because it has become a theorem. That is strong, and it is literal, with an asterisk I think deserves to be in bold: within the scope of the law you declared. Nothing there protects you from declaring the wrong law. The responsibility did not disappear, it moved, and it moved somewhere much smaller and much more legible.
Trading ten thousand lines of implementation for twenty lines of law is the best deal this profession has seen in a while.
why proof and not more tests
The difference between the two is the difference between sampling and quantifying.
A test says: for these thirty inputs, it worked. A proof says: for every possible input, it works, and here is the argument you can check line by line.
This is not a new idea. Coq, Agda, Lean and Idris have done this for decades, and the reason it never caught on is well known: writing a proof is expensive, tedious, and demands training most programmers neither have nor want. The cost of the proof was always higher than the cost of the bug.
What changed is that there is now a machine willing to do the tedious part. The proof was the bottleneck because it was human labor. It no longer is.
That is why I think this is the first time formal verification has a real shot outside academia and safety-critical systems. Not because the math got better, but because its price fell through the floor.
the objection I take seriously
There is one, and it sits right in the project's own README, stated with an honesty I respect a lot: the Bend2 compiler is 99% AI-written and has not been fully audited yet.
Read that again and feel the size of the irony. The tool that exists to stop AI mistakes was itself written by AI and left unchecked.
That seems to sink the whole thesis. I don't think it does, and the reason is the most important thing in this post.
In a proof system, generating and checking are completely different jobs. Generating a proof is brutally hard and creative, and can be done by anything: you, an AI, a monkey with infinite luck. Checking a proof is mechanical, decidable, and the program that does it is small. It does not matter where the proof came from, because it arrives with the full argument attached, and the checker walks that argument step by step.
So the question is not "is the compiler trustworthy?". It is "is the checker trustworthy?". And the checker is the small part, the part that fits inside a real audit, done by people, once, valid forever.
This is old. A serious proof assistant has always been built this way, with a minimal core that everything else has to convince. That the generator around it is huge, opaque and suspect is the expected shape. It is the design, not the flaw.
I still want to see that checker audited. I want to see people outside the project trying to break it. But the structure of the argument is right, and it is the opposite of "trust the AI": it is "trust no one, demand the argument".
what still doesn't work
Being excited about the idea is not the same as pretending the release is ready, and it isn't.
No type classes, no traits, no macros beyond templates. No LSP, no debugger, no tactics. Type annotation is mandatory everywhere. The numbers are Nat, U32 and F32, and that's it. Strings are linked lists of characters, which means exactly what anyone who has written Haskell knows it means in practice. No TLS, HTTP, JSON or regex. No native Windows, only through WSL. One GPU per program.
This is a 2.0.5 release of a project that just shipped, and the list above is long enough that nobody should be putting this in production this week.
I am not saying use it. I am saying pay attention.
what I now expect
What I wrote about cryptography yesterday applies here, in reverse.
There, the argument was that cryptography treats a new algorithm with organized distrust: an open competition, years of people trying to break it, and only then does it become a standard. And that AI does the opposite, publishing the paper in two weeks and shipping to production in the third.
Bend2 is the first thing I have seen trying to bring that rigor inside the pipeline of machine-generated code. Not asking for trust: asking for proof, and offering a cheap way to produce the proof.
Bend2 might not make it. Most languages don't, and this one carries a list of limitations the length of an arm. But the question it asks does not go away, and it is the right question: if the machine writes the code, what exactly does the human remain responsible for?
Its answer is "for saying what counts as correct". I can't think of a better one.
O Bend2 saiu essa semana (dois dias atrás, no momento em que escrevo isso), e eu quero defender a ideia dele antes que a discussão vire briga de benchmark.
Aviso de escopo: eu não rodei o Bend2. Não instalei, não escrevi uma linha, não tenho opinião sobre a ergonomia dele. O que eu tenho é opinião sobre a aposta, e a aposta eu acho certa.
o que quebrou
Nos últimos dois anos a quantidade de código que eu leio ficou maior que a quantidade de código que eu escrevo. Isso não é reclamação, é só a descrição do trabalho agora.
E aí aparece o problema que ninguém resolveu ainda: revisão humana mede se o código parece certo. É literalmente isso que a gente faz. Lê, entende a intenção, procura o caso que o autor esqueceu, e aprova quando não acha nada.
Só que "parecer certo" é exatamente o que uma máquina treinada em código humano faz melhor do que qualquer um. Ela produz o código mais plausível possível. Plausível é a métrica que ela otimiza, e plausível é a métrica que a minha revisão aplica. As duas apontam pro mesmo lugar, e o bug mora no ponto cego comum.
Eu já escrevi aqui sobre quatro coisas que eu quebrei em produção. Nenhuma delas falhou por matemática errada. Falharam por costura: uma constante que não chegava na função, uma palavra de escopo, uma ordem de checagem. Todas passaram por revisão. Todas pareciam certas.
Teste também não resolve, e por um motivo mais duro: teste mostra que o bug existe, nunca que ele não existe. Você amostra o espaço de entradas e torce pra ter amostrado o caso que importa.
Escala de IA com garantia de amostragem é uma conta que não fecha.
a inversão
O que o Bend2 propõe é parar de tentar consertar a revisão e mudar o artefato que o humano mantém.
Em vez de você escrever o código e a máquina te ajudar, você escreve a lei, e a máquina escreve o código e a prova de que o código obedece a lei. A lei fica no repositório, num arquivo chamado LAWS.bend, e ela é a coisa que você lê, versiona e discute em pull request.
law you_cant_win:
for moves: List<Game.Move>
board = Game.replay(Game.start(), moves)
{Game.is_won(board) == False{} : Bool}
Isso lê como: para qualquer sequência de jogadas, replicar essas jogadas a partir do estado inicial nunca resulta num tabuleiro vencido. Não é um caso de teste. É uma afirmação sobre todas as sequências possíveis, incluindo as que você nunca imaginou.
A implementação vira saída. A prova vira saída. O que você mantém é a afirmação.
O slogan do projeto é que integrar um bug passa a ser matematicamente impossível, porque virou teorema. É forte e é literal, com um asterisco que eu acho que precisa estar em negrito: dentro do escopo da lei que você declarou. Nada ali te protege de declarar a lei errada. A responsabilidade não sumiu, ela mudou de lugar, e mudou pra um lugar muito menor e muito mais legível.
Trocar dez mil linhas de implementação por vinte linhas de lei é o melhor negócio que essa profissão viu em bastante tempo.
por que prova e não mais teste
A diferença entre as duas coisas é a diferença entre amostrar e quantificar.
Um teste diz: para essas trinta entradas, deu certo. Uma prova diz: para toda entrada possível, dá certo, e aqui está o argumento que você pode conferir linha por linha.
Isso não é ideia nova. Coq, Agda, Lean e Idris fazem isso há décadas, e a razão de não ter pegado é bem conhecida: escrever prova é caro, chato e exige treinamento que a maioria dos programadores não tem nem quer ter. O custo da prova sempre foi maior que o custo do bug.
O que mudou é que agora tem uma máquina disposta a fazer a parte chata. A prova era o gargalo porque era trabalho humano. Deixou de ser.
É por isso que eu acho que essa é a primeira vez que verificação formal tem chance fora da academia e de sistema crítico. Não porque a matemática ficou melhor, e sim porque o preço dela caiu pro chão.
a objeção que eu levo a sério
Tem uma, e ela está no próprio README do projeto, escrita com uma honestidade que eu respeito muito: o compilador do Bend2 é 99% escrito por IA e ainda não foi auditado por completo.
Leia isso de novo e sinta o tamanho da ironia. A ferramenta que existe pra impedir erro de IA foi, ela mesma, escrita por IA e não conferida.
Isso parece derrubar a tese inteira. Eu acho que não derruba, e o motivo é a coisa mais importante desse post.
Num sistema de prova, gerar e conferir são trabalhos completamente diferentes. Gerar a prova é dificílimo, criativo, e pode ser feito por qualquer coisa: você, uma IA, um macaco com sorte infinita. Conferir a prova é mecânico, decidível, e o programa que faz isso é pequeno. Não importa de onde veio a prova, porque ela chega acompanhada do argumento completo, e o checador percorre esse argumento passo a passo.
Então a pergunta não é "o compilador é confiável?". É "o checador é confiável?". E o checador é a parte pequena, que cabe numa auditoria de verdade, feita por gente, uma vez, valendo pra sempre.
Isso é velho. Assistente de prova sério sempre foi construído assim, com um núcleo mínimo que todo o resto precisa convencer. Que o gerador ao redor seja gigante, opaco e suspeito é o esperado. É o desenho, não a falha.
Eu ainda quero ver esse checador auditado. Quero ver gente de fora do projeto tentando quebrar. Mas a estrutura do argumento está certa, e ela é o oposto de "confia na IA": ela é "não confia em ninguém, exige o argumento".
o que ainda não dá
Entusiasmo com a ideia não é fingir que o release está pronto, e ele não está.
Não tem type class, não tem trait, não tem macro além de template. Não tem LSP, não tem debugger, não tem tactic. Anotação de tipo é obrigatória em tudo. Os números são Nat, U32 e F32, e só. String é lista ligada de caractere, o que qualquer um que já escreveu Haskell sabe o que significa na prática. Não tem TLS, HTTP, JSON nem regex. Não roda em Windows nativo, só via WSL. Uma GPU por programa.
Isso é uma versão 2.0.5 de um projeto que acabou de sair, e a lista acima é longa o bastante pra que ninguém deveria estar colocando isso em produção essa semana.
Eu não estou dizendo pra usar. Estou dizendo pra prestar atenção.
o que eu passo a cobrar
Aquilo que eu escrevi sobre criptografia ontem vale aqui, do avesso.
Lá o argumento era que a criptografia trata algoritmo novo com desconfiança organizada: concurso público, anos de gente tentando quebrar, e só então virar padrão. E que a IA faz o contrário, publica o artigo em duas semanas e sobe em produção na terceira.
O Bend2 é a primeira coisa que eu vejo tentando trazer esse rigor pra dentro do fluxo de código gerado por máquina. Não pedindo confiança: pedindo prova, e oferecendo um jeito barato de produzir a prova.
Pode ser que o Bend2 não vingue. A maioria das linguagens não vinga, e essa carrega uma lista de limitações do tamanho de um braço. Mas a pergunta que ele faz não vai embora, e ela é a pergunta certa: se a máquina escreve o código, o que exatamente o humano continua sendo responsável por?
A resposta dele é "por dizer o que conta como estar certo". Eu não consigo pensar numa melhor.
acompanhe os próximos textos
Adicione este feed RSS ao seu aplicativo leitor de feeds para acompanhar novos textos. Sem cadastro ou e-mail.