Qual seria a melhor linguagem de programação para agentes de IA?

Caí num artigo do Fabio Akita que fazia uma pergunta incômoda: e se a linguagem de programação "ideal" não fosse otimizada para humanos lerem, e sim para LLMs editarem? Ele parte da ideia de que esses dois objetivos brigam entre si o tempo todo, e na maior parte do tempo a gente otimiza só para o lado humano.

A provocação é boa. Mas a conclusão dele me deixou pensando, e eu discordo do tom. Vou explicar por quê, e no fim mostro a linguagem hipotética que eu apostaria que vai existir.

O conflito de verdade

Linguagens convencionais como Python e Ruby priorizam clareza para humanos. Sintaxe enxuta, pouco cerimonial, muita liberdade. Isso é ótimo quando uma pessoa escreve e outra lê.

O problema aparece quando quem escreve é um agente. Liberdade vira ambiguidade. Dez jeitos de fazer a mesma coisa viram dez chances do modelo escolher o caminho que compila mas está errado. O que ajuda o humano (concisão, implícito, "magia") atrapalha a máquina.

O que as linguagens formais acertam

Akita observa um padrão desconfortável: as linguagens teoricamente melhores para LLM são as de verificação formal e tipos sofisticados. Lean 4, F*, Idris 2 no topo. Rust, Haskell e Dafny acertam em parte. Python e Ruby ficam de fora.

Faz sentido. Tipo explícito reduz o espaço de busca do modelo. Verificação em tempo de compilação pega o erro antes de rodar. Modularidade clara deixa o agente carregar só o pedaço relevante no contexto.

O problema é o preço. Essas são justamente as linguagens com a curva de aprendizado mais brutal para humanos. Escrever prova formal o tempo todo é caro e ninguém quer. É aí que a conclusão do Akita fica cética: a linguagem ideal seria IA-first à custa do humano, e por isso ela ainda não existe.

Onde eu discordo: o destravamento é gradiente, não técnico

Eu não acho que o obstáculo seja técnico. Acho que é de dosagem.

Ninguém aceita escrever prova formal em todo lugar. Mas e se a verificação fosse opcional por gradiente? Você paga o custo da prova só onde o risco justifica. Código de UI fica leve. Código de pagamento ganha contrato. E o trabalho pesado de gerar a prova fica com a IA, não com você.

O humano lê o contrato para confiar. O agente escreve a implementação dentro de uma cerca que ele mesmo não pode furar. Os dois públicos ganham sem que um pague pelo outro.

Como seria essa linguagem

Minha aposta não é uma linguagem exótica do zero. É algo perto de Rust + Lean com cara de TypeScript. Os pilares:

1. Tipos explícitos na assinatura, inferência local no corpo. O contrato fica visível, o ruído some.
2. Efeitos colaterais no tipo. Saber que uma função toca rede, banco ou estado só de ler a assinatura. Ouro para o agente planejar e para o humano confiar.
3. Contratos de primeira classe, opcionais. requires e ensures no estilo Dafny, adotados só onde dói.
4. Imutável por padrão. Reduz o espaço de raciocínio do modelo e os bugs sutis que escapam no review.
5. Uma sintaxe canônica, sem dialetos. Um formatador único e obrigatório, no espírito do gofmt.
6. Erros de compilação feitos para o agente. O compilador devolve a correção em formato aplicável, não um texto para humano interpretar.

Vou chamar essa linguagem hipotética de Duet: dois leitores, o humano e o agente. O exemplo é o caso clássico onde o contrato vale a pena, uma transferência de dinheiro entre contas.

module banking/transfer
  exposes { transfer }
  depends { banking/account.{Account, AccountId} }
 
# Invariante embutido no tipo: o contrato vive no tipo, não num comentário.
type Money = Int satisfies { value >= 0 }   # centavos, nunca negativo
 
# A assinatura é o contrato. Efeitos aparecem no tipo: !{db, log}.
# requires/ensures são opcionais; aqui pagamos o custo porque é dinheiro.
fn transfer(from: AccountId, to: AccountId, amount: Money) -> Result<Receipt, TransferError> !{db, log}
  requires from != to
  ensures  ok(r)  => r.debited == amount and r.credited == amount
  ensures  err(_) => no_change(from) and no_change(to)   # falhou: nada mudou
{
  let src = account.load(from)?          # `?` propaga TransferError
  let dst = account.load(to)?
 
  # `check` é uma guarda verificada: se cair, o ensures err(_) acima
  # é satisfeito automaticamente (rollback atômico).
  check src.balance >= amount else InsufficientFunds
 
  let src' = src with { balance: src.balance - amount }   # cria novo, não muta
  let dst' = dst with { balance: dst.balance + amount }
 
  account.commit([src', dst'])?          # transação atômica; efeito {db}
  log.info("transfer ok", { from, to, amount })           # efeito {log}
 
  ok(Receipt { debited: amount, credited: amount, at: now() })
}

Repare no que cada parte diz para os dois leitores. O type Money garante para o humano que não existe dinheiro negativo, e tira do agente a chance de gerar amount = -1. O !{db, log} mostra de relance que a função toca banco e log. O ensures deixa o humano confiar lendo só o contrato, enquanto o compilador prova que a implementação cumpre. O with cria valores novos em vez de mutar, então nada muda nas costas de ninguém.

A parte que não existe em linguagem nenhuma hoje

Se o agente esquecer de cobrir o saldo insuficiente, o compilador da Duet não cospe um texto. Ele devolve algo aplicável direto:

{
  "error": "contract_unsatisfied",
  "where": "transfer:ensures[1]",
  "message": "ensures err(_) => no_change(from) não é garantido: o branch que retorna InsufficientFunds ocorre APÓS account.commit",
  "suggested_fix": {
    "op": "move_before",
    "node": "check src.balance >= amount",
    "anchor": "account.commit"
  },
  "confidence": 0.91
}

O agente lê suggested_fix, reordena, recompila. O loop de correção é parte da linguagem, não um plugin colado por cima.

O gradiente em ação

A mesma transferência, na versão rápida e sem contrato, também é Duet válida:

fn transfer(from: AccountId, to: AccountId, amount: Money) -> Result<Receipt, TransferError> !{db, log} {
  let src = account.load(from)?
  let dst = account.load(to)?
  check src.balance >= amount else InsufficientFunds
  account.commit([
    src with { balance: src.balance - amount },
    dst with { balance: dst.balance + amount },
  ])?
  ok(Receipt { debited: amount, credited: amount, at: now() })
}

Mesma linguagem, mesma sintaxe. Você só paga o custo da prova onde o risco justifica. É o gradiente: a IA escreve as duas, o humano lê o contrato quando ele existe, e ninguém é obrigado a escrever prova formal o tempo todo como o Lean exige.

Por que isso nasce como extensão, não do zero

Tem um detalhe que decide tudo: o ecossistema vence a linguagem. Uma "linguagem ideal para agentes" sem o equivalente a npm ou cargo, e sem milhões de exemplos no treino dos modelos, nasce morta. O agente é bom em TypeScript e Python porque viu bilhões de linhas delas.

Por isso minha aposta real de curto prazo não é uma linguagem nova. É TypeScript ou Rust ganhando uma camada de contratos verificáveis e efeitos no tipo, porque já têm massa crítica de treino e tooling. O Akita descreveu o destino. O caminho passa por estender o que a IA já sabe escrever bem, não por inventar um idioma que ninguém fala.

A linguagem ideal para agentes e humanos provavelmente já está entre a gente. Só falta a camada de contrato gradual por cima.