Quando a parte difícil deixa de ser difícil
Um experimento com provas formais
Um trabalho coassinado por Ilya Sergey, aceito para a OOPSLA’26, apresenta um novo sistema de tipos para Move, linguagem de contratos inteligentes inspirada em Rust. A ideia técnica central é usar expressões regulares para representar a alcançabilidade no heap. O ponto principal, porém, é como o trabalho foi produzido: a parte que normalmente consome entre 80% e 90% do esforço de um artigo de projeto de linguagens de programação - a mecanização da metateoria e as provas formais de solidez - foi realizada por uma única pessoa em Lean, com auxílio de um LLM de fronteira, em cerca de quatro semanas e em escala comparável à de um compilador de produção, não de um cálculo de brinquedo.
O autor afirma que já havia apresentado esse experimento em palestras e discutido seus resultados com integrantes proeminentes da comunidade de pesquisa em linguagens de programação. As reações variaram de curiosidade e entusiasmo a ceticismo, com alguns interlocutores sugerindo que a formalização não poderia ter sido tão difícil, e rejeição à ideia de que esse fosse um modo apropriado de fazer teoria de linguagens. Para ele, essas respostas revelam uma cultura de publicação que tende a associar credibilidade à quantidade visível de esforço humano, dificuldade ou sofrimento envolvido.
A mudança na escala de produção
Segundo essa visão, ideias elegantes costumam ser aceitas quando acompanhadas por oito a dez pessoas-mês de trabalho, como uma implementação grande, avaliações extensas ou provas verificadas por máquina conduzidas manualmente. Ferramentas atuais podem remover esse “invólucro” de trabalho: um pesquisador experiente com uma boa ideia talvez consiga transformá-la em uma publicação competente em aproximadamente um mês. O autor compara essa situação à área de inteligência artificial e aprendizado de máquina, na qual, segundo relatos que ouviu, seria rotineiro passar de uma ideia a uma submissão sólida ao NeurIPS em um sprint mensal.
Ele afirma que os primeiros efeitos já apareceram. O número de submissões ao POPL teria quase dobrado em 2026, de cerca de 350 para 600. A surpresa, segundo o texto, é que a proporção de material totalmente gerado por IA seria relativamente pequena: a maioria consistiria em pesquisas competentes produzidas em ritmo até dez vezes maior que o habitual, com provas, implementações e avaliações trabalhosas amplamente automatizadas. Se antes ter mais de dois artigos em um grande evento de linguagens indicava uma visão forte, um grupo prolífico e uma ampla rede de colaboradores, o mesmo volume agora poderia ser produzido por um único doutorando com boas ideias. O autor considera possível que três ou quatro artigos de autoria individual em um evento de ponta se tornem algo comum em um ou dois anos.
Um novo patamar para a pesquisa
A previsão é que a comunidade eleve os critérios quando perceber que artigos antigos, baseados em pequenos cálculos e resultados limitados, não representam um bom uso das ferramentas modernas. Se pesquisadores puderem construir do zero sistemas da escala de CompCert ou do microkernel seL4 em assistentes de prova, a área terá de assumir problemas mais ambiciosos, inclusive desafios que pareciam inimagináveis poucos anos atrás. A conclusão não é que a pesquisa ficou simples em todos os sentidos, mas que a automação pode deslocar a dificuldade: produzir e verificar artefatos técnicos deixa de ser o principal gargalo, enquanto a escolha de problemas mais relevantes e ousados ganha importância.