Bend: Uma Linguagem com Verificação de Provas que Bloqueia Erros de IA em CPU e GPU

Bend é uma linguagem compilada e paralela voltada para código gerado por IA. Sua proposta central: em vez de confiar em uma saída que você nunca leu, você declara leis em um arquivo LAWS.bend e exige que o agente as prove antes do merge.

A promessa soa como a de qualquer outra ferramenta de codificação com IA, mas a mecânica é diferente. O verificador de tipos do Bend é um verificador de provas, a mesma ideia do Lean ou do Rocq. A diferença que ele destaca é a velocidade: esses verificadores podem levar minutos em bases de código de porte médio, enquanto o Bend afirma levar no máximo um segundo, para que um agente possa rodar verificações após cada alteração.

De onde vem a velocidade

• Compila para código nativo. Quase na velocidade de C em um único núcleo.
• O mesmo binário escala para dezesseis núcleos ou para a GPU. A documentação afirma ser até 100x mais rápido que um único núcleo.
• O paralelismo é automático. Você divide o trabalho em dois; o Bend distribui as chamadas entre núcleos da CPU ou da GPU e depois as junta. Sem threads, sem locks, sem código de kernel.

O site mostra um exemplo pow2.bend rodando em 4.096 núcleos de GPU.

As leis e o modelo de prova

Você escreve uma lei em LAWS.bend:

# LAW: no move sequence leads to victory.
law you_cant_win : for moves: List<Move>
    board = replay(start(), moves)
    is_won(board) == False

O agente então escreve a prova correspondente em PROOF.bend:

# PROOF: you_cant_win holds.
def Laws.you_cant_win (moves):
    # ... written by the AI

Depois que uma lei é declarada, o site argumenta que o agente não consegue fazer merge de uma linha que a viole. A demonstração usa um jogo: peça ao Claude para fazer o tabuleiro dar a volta. Sem o LAWS.bend, o bug é mesclado e entra em produção. Com ele, o agente precisa tentar de novo até construir uma prova. A formulação na fonte: mesclar um bug se torna "matematicamente impossível".

Configuração

Instalação:

curl -fsSL https://bend-lang.com/install.sh | sh

Depois adicione este bloco ao seu AGENTS.md para que os agentes saibam o que fazer:

When using Bend:
- run `bend guide` to learn it
- use `LAWS.bend` to keep important rules
- run `bend PROOF.bend` before committing
- parallelize the code whenever possible

O Bend essencialmente trata o LAWS.bend como um AGENTS.md respaldado por provas. "Não cometa erros" passa a ser verificado por tipos.

Ressalvas da fonte

A documentação é sincera: o Bend é jovem, espere bugs e os reporte. Ele funciona melhor no back-end e tem como alvo Linux e macOS. O núcleo é respaldado por dois artigos — BendTT (teoria de tipos dependentes afins) e BendRT (runtime paralelo de CPU/GPU).

Para quem é

Equipes que deixam agentes enviarem código que não leem, especialmente serviços de back-end em que uma regra como "saldos nunca ficam negativos" precisa de imposição em vez de revisão de código.