18 de setembro de 2026 Bend serve como um exemplo útil do meu ponto geral sobre vibe-coding, pois é recente, de alto perfil e possui aspectos que o tornam fácil de usar como exemplo. Não sei nada sobre o histórico do autor no design de linguagens ou se ele realmente considerou os trade-offs abaixo e fez o que eu acredito ser uma escolha ruim. Sinta-se à vontade para substituir “o autor” abaixo por “um autor hipotético que poderia ter criado a mesma coisa”.

Obviamente não gosto das decisões de design tomadas em Bend e eu queria apresentá-las, porém isso foi excessivamente confundido com o ponto principal que estou tentando fazer abaixo. Não quero editar isso agora e fazer parecer que quaisquer comentários existentes estão sendo excessivamente duros, então sinto que a melhor solução é explicar qual era meu modelo mental do artigo enquanto eu o escrevia. Aqui está um comentário do autor de Bend.

Bend 2 está sendo promovido como uma linguagem para a era da codificação com IA: humanos escrevem “leis”, a IA escreve implementações e provas, e o compilador verifica se as provas são sólidas. Tudo isso soa bastante impressionante e eu consigo ver por que alguém quereria uma linguagem que faça isso. Na verdade, existem alguns problemas maiores com essa ideia; no entanto, isso não é o que este artigo trata.

Em vez disso, quero falar sobre como o Bend em si parece ter caído em uma armadilha comum com vibe-coding que eu não vejo mencionada muito. Vamos começar com uma linha de base do que o Bend exige que o desenvolvedor escreva para sua demonstração na página inicial:https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/LAWS.bend Não vou reproduzi-lo aqui porque o código não é muito importante. O que é importante para este artigo é que ele contém bastante código.

São 58 linhas de código apenas para afirmar que o jogador nunca pode tocar a bandeira ou vencer o jogo. Também há outros problemas no fato de que o LLM pode redefinir os subprogramas de Game para fazer qualquer coisa; porém, isso novamente não é o ponto do artigo. Em seguida, vamos ver o que o LLM que está escrevendo o código para este programa precisa escrever para provar as “leis”:https://github.com/bendlang/bend/blob/main/demos/app_win_is_bug_2d/PROOF.bend Isso é muito.

São 442 linhas de código para provar essas propriedades simples. Então, qual é o meu problema com isso? Por que eu o chamo de armadilha do vibe-coding? O problema é que o vibe-coding torna possível construir uma solução substancial antes de aprender o suficiente sobre o problema para reconhecer que existe uma solução muito melhor. Um desenvolvedor pode produzir uma linguagem e um compilador inteiros enquanto deixa passar uma abordagem que uma pesquisa introdutória no campo teria colocado diretamente na frente deles.

O campo em questão é a verificação formal. É digno de nota que essas duas palavras não aparecem em nenhum lugar na página da web do Bend ou em sua base de código. O desenvolvedor construiu uma linguagem inteira em torno de um campo aparentemente sem perceber que esse campo existe. Para demonstrar claramente por que isso é um problema, vamos recriar o mesmo programa que o Bend usa como demonstração no SPARK, uma linguagem e compilador de código aberto para verificação formal.

Para ser justo com o Bend, eu mesmo fiz vibe-coding nesse caso, eu simplesmente disse a um LLM para recriar a demonstração no SPARK sem mais orientações:package Game with SPARK_Mode issubtype Column is Integer range 0 .. 11;subtype Row is Integer range 0 .. 7;type State is record X : Column; Y : Row; Won : Boolean;end record; Start : constant State := (8, 5, False);function Wall (X : Column; Y : Row) return Boolean is(((X = 3 or X = 11) and Y <= 3)or ((Y = 3 or Y = 7) and X <= 3));function Cell (X : Column; Y : Row) return Character is(if Wall (X, Y) then '#' elsif X = 1 and Y = 1 then 'F' else '.');-- Inductive invariant: outside the sealed room, off walls, not won.function Safe (G : State) return Boolean is((G. X > 2 or G. Y > 2) and not Wall (G.

X, G. Y) and not G. Won)with Ghost;procedure Step (G : in out State; Key : Character)with Post => (if Safe (G'Old) then Safe (G));-- Both Bend laws, including the actual cell drawn by the terminal.function Replay (Keys : St...