o manifesto do bend2

O Bend2 saiu hoje, 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 de um dia atrás, 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.