Sistemas de tipos funcionam como oráculos de busca para LLMs

Aditya Kumar observa um aparente paradoxo: o Rust e o Lean gerados por modelos de linguagem funcionam melhor na prática do que o C++ gerado, embora os benchmarks públicos digam o oposto - Rust é considerado uma linguagem de poucos recursos nos dados de pré-treinamento, com pontuação abaixo de Python em benchmarks multilíngues como o MultiPL-E, e Lean mal aparece. As duas observações são corretas, e reconciliá-las muda a compreensão do propósito de um sistema de tipos.

O que a acurácia de uma passada não captura

O autor argumenta que pass@1 mede apenas se a primeira minuta está certa, mas ninguém publica a primeira minuta. A métrica relevante é quantos programas que chegam à produção estão errados, e quanto trabalho isso custou. O experimento mais limpo que ele encontrou usou Idris: Li e Krishnamachari deram ao GPT-5 cinquenta e seis problemas do Exercism em Idris, medidos zero-shot contra outras linguagens. Zero-shot, o resultado segue o previsto pelos benchmarks - Idris resolve 39% (22 de 56) contra 90% de Python (45 de 50). Mas quando os erros do compilador são realimentados ao modelo, Idris salta para 54 de 56 (96%), acima do ponto de partida de Python. A ablação é reveladora: alimentar documentação ou guias de classificação de erros funcionou pior do que devolver os erros locais de compilação, gerados do próprio código quebrado do modelo. O mecanismo proposto: os dados de treinamento determinam onde a primeira minuta cai; o sistema de tipos determina se o laço seguinte converge para algo correto ou apenas para algo que roda.

O mesmo padrão em escala corporativa

Como corroboração, Kumar cita David Tolnay, que publicou dados de oito anos de adoção de linguagens na Meta, derivados das tabelas de controle de versão que alimentam os painéis internos. A métrica é uma razão ano a ano, dentro de janelas de noventa dias. Cinco linguagens inflectem juntas por volta de fevereiro e março de 2026, e Tolnay atribui o fato sem rodeios à adoção de codificação agêntica pelos engenheiros da Meta no primeiro trimestre de 2026: TypeScript, Rust, Swift, JavaScript e Go - descontando o JavaScript, atribuído a arquivos de configuração dentro de projetos TypeScript, restam quatro linguagens, todas estaticamente tipadas.

O autor levanta duas ressalvas para evitar leituras apressadas. Primeiro, C++ e Python estarem planos não prova que os modelos os escrevem mal: a razão de crescimento divide pela base, e um movimento de 1% em C++ pode superar em termos absolutos a duplicação de Rust. Segundo, a unidade é o desenvolvedor, não a linha de código - Tolnay explica o crescimento de TypeScript por painéis e widgets pessoais que engenheiros e gestores nunca teriam feito sem IA. O que sobrevive às ressalvas é um número que não é razão: engenheiros da Meta escreveram o dobro de Rust de primeira parte neste ano do que nos nove anos anteriores somados. Geração barata aplicada de forma ampla teria erguido o gráfico inteiro; o crescimento se concentrou em linguagens cujo compilador rejeita um programa errado antes de executá-lo.

C++ como grupo de controle e Lean como caso-limite

Se a tese fosse "tipagem estática ajuda", C++ estaria bem - é estaticamente tipado, com um sistema de tipos Turing-completo em tempo de compilação. A distinção, argumenta o autor, não é estático contra dinâmico, mas o quanto uma compilação bem-sucedida promete. Em Rust, compilar garante propriedades específicas: sem use-after-free, sem data races, matches exaustivos, todos os caminhos de erro tratados; contornar isso exige unsafe, lexicalmente visível. Em C++, compilar verifica apenas resolução de nomes e sobrecargas - não verifica use-after-free, invalidação de iterador, data races, acesso fora dos limites nem overflow de inteiros com sinal, e o comportamento indefinido não oferece diagnóstico. Um verificador que pode ser contornado silenciosamente tem uma aprovação que vale menos.

Lean é o caso em que o argumento vira algoritmo. Uma prova em Lean é verificada por um kernel: a resposta é uma decisão, não uma opinião, o que torna a geração pesquisável por busca. Amostrar trinta e duas provas candidatas e manter a que verifica é um procedimento correto. O Delta Prover atinge 95,9% no miniF2F assim, com um modelo de propósito geral sem fine-tuning, dirigindo o Lean 4 por decomposição e reparo iterativo. O mesmo em Python produz trinta e dois programas que concordam com a suíte de testes - uma afirmação muito mais fraca, com um oráculo parcial e uma busca não-correta.

Limites e o que muda na prática

Rust que compila ainda pode estar errado: tipos restringem a forma de uma computação, não sua intenção. A literatura de autorreparo mostra que erros sintáticos e de tipo são muito mais reparáveis a partir de feedback do que erros lógicos ou algorítmicos - e o autor lê isso como o próprio mecanismo: um sistema de tipos mais forte move erros da categoria cara para a barata, tornando um índice com off-by-one um erro de compilação, por exemplo.

O argumento pesa mais para código gerado do que para código humano: um revisor humano consegue perguntar ao autor o que ele pensava, mas código gerado chega como texto localmente plausível sem modelo mental por trás - e plausível-porém-errado é a falha que revisão humana pior captura. O próprio autor reconhece as limitações da evidência: um experimento controlado em linguagem ninguém implanta, resultados de theorem-proving que dependem de um oráculo total que programação comum não tem, uma curva de adoção que registra o que engenheiros buscaram e sua experiência não controlada. O que ele gostaria de ver é o número que ninguém publica: defeitos por mil linhas de código gerado em produção, por linguagem. Mesmo assim, ele conclui que o mecanismo é claro o suficiente para agir: escolher a linguagem de um código que será substancialmente escrito por máquinas é, em parte, decidir quanta especificação se quer que o compilador sustente.