bend

Bend 2 é uma nova linguagem de programação projetada para a era pós-AGI, onde humanos comunicam intenções a sistemas de IA por meio de uma linguagem sem ambiguidade. Sua inovação central é LAWS.bend — um mecanismo onde desenvolvedores declaram invariantes (leis) que a IA deve provar matematicamente para qualquer mudança de código, tornando matematicamente impossível mesclar bugs que violem essas regras. Capacidades principais evidenciadas no README: **Desempenho**: Visa velocidade de nível C em CPU e nível CUDA em GPU. Benchmarks mostram desempenho competitivo de núcleo único e escalabilidade paralela massiva em milhares de núcleos. O compilador explora tipos fortes, pureza e linearidade para otimização. **Verificação de provas**: Alega verificação ordens de magnitude mais rápida que Isabelle, Agda, Lean ou Coq, verificando provas complexas em menos de um segundo. **Paralelismo implícito**: Sem threads, locks ou kernels para escrever. Funções de dividir e conquistar se distribuem automaticamente por todos os núcleos de CPU/GPU disponíveis. O exemplo mostra pow2(20) distribuído em 4.096 núcleos de GPU. **Fluxo de trabalho colaborativo com IA**: Projetado para desenvolvimento assistido por IA. Desenvolvedores escrevem leis em LAWS.bend (ex.: "soma dos saldos deve ser zero", "jogadores não podem atravessar paredes"), então exigem que a IA execute `bend PROOF.bend` antes de commitar. O compilador aplica provas mecanicamente. **Recursos da linguagem**: Sintaxe semelhante a Python com tipos dependentes. Sistema de tipos afim/linear (valores não podem ser compartilhados). Recursão terminante exigida (com escape @unsafe). Alvos: C, Metal, CUDA, JavaScript. Biblioteca base é mínima; efeitos incluem I/O, canais, TCP/UDP, acesso a arquivos. **Limitações atuais (listadas explicitamente)**: Anotações verbosas, sem classes de tipos/traits/macros, sem táticas ou busca de provas, tipos numéricos limitados (apenas Nat, U32, F32), strings lentas (listas ligadas), sem HTTP/JSON/TLS/regex, uma GPU por programa, sem compilação incremental, compilação nativa lenta, ferramentas mínimas (sem LSP, debugger, formatador, REPL), compilador amplamente escrito por IA e não auditado. O projeto inclui formalização em Lean (bend.lean), artigos acadêmicos (teoria de tipos BendTT, runtime BendRT) e uma coleção crescente de demos. Canais da comunidade: Discord, Reddit, X/Twitter. Licença não especificada no material fornecido.