Bend2

O que é o Bend2

Bend2 (ou Bend 2) é uma linguagem de programação criada pelo desenvolvedor brasileiro Victor Taelin e lançada em 17 de setembro de 2026. A proposta central é combinar velocidade próxima à da linguagem C, execução paralela em GPU e um sistema de provas matemáticas capaz de barrar, em tempo de compilação, código incorreto — inclusive o código escrito por modelos de inteligência artificial. O lema oficial do projeto resume a combinação: "uma linguagem rápida que bloqueia erros de IA via prova — velocidade de C, paralelismo de CUDA, provas de Lean, sintaxe de Python".

A linguagem é distribuída como software livre sob licença Apache 2.0, com código no repositório bendlang/bend no GitHub e documentação em bend-lang.com. O desenvolvimento é conduzido pela Higher Order Company (HOC), empresa fundada por Taelin.

O público-alvo declarado são projetos escritos majoritariamente por agentes de IA. O argumento do autor é que, quando humanos deixam de ler e revisar o código linha a linha, a revisão precisa migrar para o sistema de tipos: em vez de confiar na saída do modelo, o programador escreve a especificação do que o programa deve cumprir, e o compilador rejeita qualquer implementação que não prove esse cumprimento.

Quem é Victor Taelin

Victor Taelin é pesquisador e desenvolvedor brasileiro, fundador da Higher Order Company. Em publicação própria às vésperas do lançamento do Bend2, ele resumiu a trajetória: começou a programar aos 11 anos mantendo um servidor de Open Tibia em C++ e Lua, ingressou em Engenharia da Computação sem concluir o curso, trabalhou no ecossistema Ethereum e passou a última década estudando teoria de linguagens de programação.

Antes do Bend2, assinou três projetos encadeados: o Kind, uma linguagem mínima de provas; o HVM (Higher-order Virtual Machine), uma máquina virtual paralela; e o Bend1, descrito por ele como um protótipo inicial do Bend2. A linha de pesquisa que sustenta esses trabalhos é a redução ótima do cálculo lambda e as redes de interação formuladas por Yves Lafont.

Como funciona: provas no lugar da revisão humana

O verificador de tipos do Bend2 funciona também como verificador de provas, na mesma linhagem de assistentes como Lean e Rocq. A linguagem tem suporte nativo a tipos dependentes, o que permite expressar no próprio tipo de uma função a propriedade que ela precisa satisfazer.

O fluxo de trabalho proposto separa a intenção humana da implementação gerada por máquina em dois arquivos:

• LAWS.bend, escrito por pessoas, declara as invariantes e regras que o programa não pode violar;
• PROOF.bend, produzido pela IA, contém as provas de que a implementação respeita essas leis.

A sintaxe é próxima da de Python, com tipagem inspirada em linguagens funcionais. O gerenciamento de memória usa um sistema de tipos afim, que dispensa coletor de lixo: não há pausas de garbage collection em tempo de execução. A linguagem não tem comando if — o desvio condicional é feito por match sobre os construtores True e False — e o disparo de trabalho para a GPU é marcado por um operador dedicado.

Desempenho e execução em GPU

O Bend2 compila para um único arquivo em C, que é então compilado por clang para a CPU e por Metal ou CUDA para a GPU. Segundo os números publicados pelo próprio projeto, uma implementação do Jogo da Vida roda em 7,8 segundos em um único núcleo de um Apple M4 Max, contra 6,78 segundos da versão equivalente em C, e cai para 0,06 segundo quando executada na GPU. Ainda conforme benchmarks do projeto, a verificação de 3.200 instanciações genéricas leva 0,38 segundo no Bend2, contra 19,2 segundos no Lean e 6,04 segundos no Rocq.

Em 10 de setembro de 2026, antes do lançamento público, Taelin apresentou a Astra, uma engine gráfica escrita inteiramente em Bend2. A demonstração processava 1 milhão de objetos por quadro em resolução 1024x1024 e atingia 80 quadros por segundo em ray tracing na GPU de um Apple M4, sem usar shaders nem buffers de OpenGL.

Do Bend 1 ao Bend 2

O Bend original foi lançado em maio de 2024 e rodava sobre o HVM2, um runtime baseado em redes de interação que distribuía o trabalho automaticamente entre milhares de threads. O anúncio de "rodar uma linguagem de alto nível em GPU" teve grande repercussão na comunidade de programação.

O Bend2 rompe com essa arquitetura. Taelin explicou que abandonou as redes de interação porque não conseguiu torná-las tão rápidas quanto variantes de ordem inferior no hardware comum, e que a nova versão foi desenhada para ser prática, não idealista: "está mais perto de C do que de Haskell". Programas escritos em Bend1 não são compatíveis com o Bend2.

As diferenças práticas incluem a ampliação do limite de memória de 2 GB para 8 TB e a mudança nos tipos numéricos, que passaram a incluir Nat, U32 e F32. Os tipos de 64 bits ficaram de fora desta versão — o autor citou, entre os motivos, o fato de o Metal não oferecer suporte a f64.

Lançamento e repercussão

O lançamento ocorreu em 17 de setembro de 2026 e foi precedido por sucessivos adiamentos. Em 4 de setembro, Taelin anunciou que a versão inicial sairia com escopo reduzido, sem gráficos em janela, compilação para HTML5, síntese de programas via SupGen e arrays atômicos compartilhados. Em 9 de setembro, informou que o código estava pronto, mas que o lançamento seguia travado por incertezas regulatórias em torno do sistema de cobrança nos Estados Unidos.

Depois da publicação, o ritmo foi de correção contínua: foram nove releases nas dez primeiras horas. Em 20 de setembro, o autor reconheceu publicamente ter esquecido de integrar o suporte a arrays atômicos antes do lançamento, o que impedia algoritmos GPGPU que dependem de leitura e escrita em buffers compartilhados, e prometeu a correção no mesmo dia.

Em 21 de setembro, Taelin anunciou a suspensão de novas funcionalidades. A justificativa foi o tamanho do código, que já passava de 100 mil tokens: o objetivo declarado é manter o kernel e o compilador dentro de um limite que caiba no contexto de um modelo de IA, permitindo auditoria e refatoração automatizadas. A partir daí, passou a aceitar preferencialmente contribuições que reduzam o número de linhas.

No mesmo dia 21, o repositório do Bend foi retirado do ar pelo GitHub, sem explicação pública sobre o motivo. Taelin abriu um chamado de suporte, e o repositório voltou a ficar acessível horas depois.

Limitações e críticas

O próprio projeto mantém uma seção extensa de limitações conhecidas. O compilador, ao contrário do kernel de verificação, foi escrito em grande parte por IA e não passou por auditoria humana equivalente — Taelin avisou desde o anúncio que bugs eram esperados. A biblioteca padrão é enxuta: recursos básicos como HTTP, TLS, JSON, fuso horário e entrada e saída de terminal dependem de efeitos externos escritos à mão. Não há estabilidade de ABI, as provas não se estendem além da fronteira com o código em C, e o sistema de provas não tem táticas nem inferência, o que torna as demonstrações verbosas e anotadas manualmente. Falta também uma biblioteca de lemas de aritmética sobre Nat, lacuna que o autor reconhece.

Em 19 de setembro, Taelin ofereceu uma recompensa de 10 mil dólares a quem escrevesse um arquivo que provasse uma falsidade lógica — o tipo Empty — sem recorrer a unsafe ou a buracos (holes). Ele admitiu que a implementação atual divergiu da formalização e que exploits nos primeiros dias não são impossíveis; a premiação só valeria depois de a implementação ser sincronizada com a formalização. Outra limitação reconhecida no mesmo período é que a linguagem não permite, por design, reutilizar hipóteses em provas matemáticas.

Do lado externo, as críticas se concentraram nas comparações de desempenho e no vocabulário. O desenvolvedor Nezk apontou que os números de velocidade do verificador são enganosos porque o Bend pula etapas de elaboração, unificação e argumentos implícitos que Lean e Rocq executam. Liam Powell observou a ausência do termo "verificação formal" na comunicação do projeto e relatou ter provado propriedades equivalentes em SPARK/Ada de forma automática, com 442 linhas a menos.

Higher Order Company, Bender e o modelo de negócio

A Higher Order Company levantou uma rodada seed de 4 milhões de dólares em 2023, o que permitiu montar uma equipe de cerca de dez engenheiros com aproximadamente três anos de caixa. No lançamento do Bend2, Taelin declarou que a empresa "entrega sem um produto": tudo o que havia sido considerado como fonte de receita esbarrava em restrições legais ou no fato de o mercado não pagar por compiladores. A equipe atual, segundo ele, é de quatro humanos e 25 "não humanos" — agentes de IA.

O produto pago é o Bender, um agente de provas que se apoia em modelos de Anthropic e OpenAI e deve ser integrado ao SupGen, com a meta de provar teoremas em Bend2 mais rápido do que LLMs de propósito geral. Em 20 de setembro, Taelin informou que o Bender havia faturado 2 mil dólares desde o lançamento, em tom irônico sobre a escala do número.

No mesmo dia, anunciou que a HOC procura um cofundador para assumir a gestão da comunidade e liderar a captação, e que viajaria aos Estados Unidos para buscar capital de risco. Ele também afirmou que a qualidade média do código gerado por IA no repositório está abaixo do padrão que produz manualmente.

Como instalar e onde está o código

A instalação recomendada pelo site oficial é um script único:

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

O código-fonte fica em github.com/bendlang/bend, sob licença Apache 2.0. Em 21 de setembro de 2026 o repositório somava cerca de 22,3 mil estrelas, número em boa parte herdado do repositório do Bend1, que foi renomeado. O projeto mantém ainda documentação e um hub de pacotes em subdomínios de bend-lang.com, além de comunidade no Discord.