Bend – uma linguagem que bloqueia erros de IA via provas e roda em GPUs
Uma nova linguagem de programação chamada Bend pretende permitir que desenvolvedores especifiquem “leis” formais que o código gerado por IA deve satisfazer, usando um sistema de tipos dependente afim e um runtime acelerado por GPU para checar provas rapidamente. Os comentaristas se mostram intrigados com a ideia de restringir LLMs com invariantes verificadas por máquina, mas levantam preocupações práticas: escrever leis completas e corretas pode ser tão difícil quanto escrever o programa, leis mal especificadas podem ser burladas, e o ecossistema atual (stdlib, ergonomia, ferramentas) ainda é imaturo. Também surgem questões de confiança em torno do uso intenso de IA no próprio código e documentação do projeto, da remoção anterior do histórico do git e das afirmações ousadas de desempenho e correção em comparação com assistentes de prova maduros como Lean ou Agda.
Objetivos do projeto e posicionamento
- Bend é apresentada como uma linguagem com uma teoria de tipos dependente afim, voltada a provar “leis” sobre programas e compilar para código eficiente em CPU/GPU.
- Ideia central: humanos/agentes escrevem uma pequena especificação LAWS.bend; a IA (ou humanos) escreve o restante; o compilador verifica que todo o código satisfaz as leis.
- Comercializada explicitamente para o mundo “pós-AGI” e para agentes de codificação baseados em LLM.
Histórico do repositório, confiança e código gerado por IA
- Grande preocupação com o repositório do GitHub ter sido reduzido a um único commit, apagando histórico, forks e reprodutibilidade; visto como um problema de confiança, especialmente diante de grandes promessas.
- O histórico foi posteriormente restaurado após اعتراض; alguns argumentam que isso foi exagerado, outros veem como crucial para auditabilidade e benchmarks.
- Partes significativas do compilador/documentação foram geradas ou ajudadas por LLMs; alguns veem isso como normal, outros como “AI slop” e um sinal de alerta quando combinado com afirmações grandiosas.
Sistema de tipos, provas e “leis”
- Bend usa tipos lineares/afins e universos indexados por quantidade, proibindo clonagem de closures em tempo de execução para garantir terminação e bom comportamento em GPU.
- As leis são essencialmente invariantes/provas verificadas em tempo de compilação; testes são explicitamente contrastados por não oferecerem as mesmas garantias.
- Vários comentaristas observam o problema clássico: especificar leis corretas e não vacuosas para sistemas grandes é pelo menos tão difícil quanto escrever o código.
- Risco de “programação do espaço negativo”: a IA satisfaz as leis mudando o problema (por exemplo, regras de movimento do jogo, tamanho do mundo) em vez de refletir a intenção do usuário.
Desempenho, história da GPU e comparações
- Alegações de checagem de provas uma ordem de grandeza mais rápida que Lean/Agda/Isabelle são recebidas com ceticismo:
- Bend evita unificação, táticas e inferência, então comparações com elaboradores completos são vistas como enganosas.
- O uso de GPU é atualmente para paralelismo em tempo de execução; checagem de provas em GPU no compilador ainda é “não por enquanto”.
- Alguns se interessam pela linhagem de interaction-net/HVM; outros observam que Bend 2 é arquiteturalmente diferente do trabalho anterior.
Design da linguagem, ergonomia e documentação
- A documentação (GUIDE) é elogiada pela ambição, mas criticada por ser confusa:
- Dúvidas sobre argumentos apagados, parâmetros Kind, sintaxe de arrays e tipos surpreendentes como
Array<T> & U32. - Arrays/linearidade levam a APIs pouco intuitivas (leituras retornando
(array, value)), o que é reconhecido como algo que provavelmente precisa de redesenho.
- Dúvidas sobre argumentos apagados, parâmetros Kind, sintaxe de arrays e tipos surpreendentes como
- A ausência de táticas e inferência torna as provas verbosas; a posição do autor é que a verbosidade é aceitável se a IA escrever as provas.
Adoção, ecossistema e alternativas
- Preocupações com:
- stdlib pequena, falta de bibliotecas matemáticas e dificuldade de portar grandes provas existentes de sistemas como Cubical Agda.
- Ferramentas ausentes ou nascentes (changelogs, releases, integração com linguagens existentes).
- Alguns estão entusiasmados e experimentando (por exemplo, portar pequenos apps, agendas de reunião); outros preferem ferramentas já existentes como Lean, Coq, Dafny, Verus, ou contratos semelhantes a provas em linguagens mainstream.
- Vários observam que isto é uma pesquisa/engenharia promissora em estágio inicial, mas o marketing atual exagera a maturidade e o escopo.