Métodos formais e o futuro da programação

• Métodos formais são ferramentas para provar que o software satisfaz as propriedades pretendidas, e a disseminação da programação com agentes está mudando a avaliação de custo-benefício
• A Jane Street antes via os métodos formais como algo de baixo valor em relação ao custo, exceto em alguns casos especiais, mas agora está criando uma equipe dedicada
• O seL4 consumiu 25 anos-pessoa para verificar 8.700 linhas de código C, e foram necessárias cerca de 23 linhas de prova e meio dia-pessoa de verificação por linha de código
• O código gerado por agentes ainda difere da qualidade pronta para lançamento, e os métodos formais estão se tornando importantes como forma de reduzir o gargalo de verificação e dar feedback forte aos agentes
• A Jane Street acredita que, por poder controlar profundamente sua linguagem e contar com uma comunidade de programadores preparada, há espaço para desenvolver OxCaml junto com técnicas orientadas a provas

---

Métodos formais e o futuro da programação

• Ao longo dos últimos 25 anos, a Jane Street vinha dizendo que, no nível organizacional, não tinha interesse em métodos formais, mas agora não mantém mais essa posição
• Há muito tempo a empresa valoriza o poder de ferramentas para escrever código melhor e mais confiável, e os sistemas de tipos são vistos como métodos formais leves que trouxeram grandes ganhos
• Fora de casos especiais, especialmente a síntese de hardware, a avaliação era de que os métodos formais custavam caro demais para se adequar à maior parte do software
• seL4 é um microkernel formalmente verificado e uma conquista importante, mas a verificação de 8.700 linhas de código C consumiu 25 anos-pessoa
  • Foram necessárias cerca de 23 linhas de prova por linha de código, e aproximadamente meio dia-pessoa para verificar cada linha
• Em casos de alto risco e com especificações relativamente claras, como microkernels críticos para segurança, essa abordagem pode valer a pena
• Ela não parecia adequada para a maior parte do software, nem para o software mais importante da Jane Street
• O surgimento da programação com agentes mudou essa avaliação, e o ceticismo sobre o potencial dos métodos formais se transformou em expectativa
• A Jane Street está montando uma equipe de métodos formais e espera transformá-los em uma ferramenta de construção de software tão amplamente útil quanto sistemas de tipos sofisticados

Por que mudaram de ideia

• A programação com agentes mexe, de várias maneiras, com a antiga relação de custo-benefício dos métodos formais
• Isso não significa que agentes consigam, sozinhos, construir provas arbitrariamente difíceis, mas os modelos ajudam muito e permitem que mais pessoas usem essas ferramentas de forma produtiva
• Como usar métodos formais ficou mais fácil do que antes, passou a valer a pena reavaliar o cálculo de custo versus efeito feito no passado

• O gargalo de verificação ficou mais importante

  • Os modelos estão cada vez melhores em escrever código útil, mas ainda existe uma grande diferença entre o código gerado pelo modelo e o código que realmente pode ser lançado
  • Os modelos são surpreendentemente bons em atingir o objetivo dado, mas ainda não são fortes o suficiente para manter ou melhorar a qualidade da base de código durante o processo
  • O código produzido por agentes está melhorando, mas tende a ser excessivamente complexo, cheio de bugs estranhos e casos de borda, além de frequentemente não respeitar os invariantes centrais da base de código
  • Pessoas ainda precisam gastar muito tempo verificando se o código produzido por agentes tem qualidade suficiente
  • Os métodos formais podem reduzir essa carga de verificação e tornar o processo de revisão mais eficiente

• Agentes ficam mais fortes com feedback

  • Agentes se beneficiam de feedback tanto quando são treinados com aprendizado por reforço quanto quando são usados para programar
  • Métodos formais podem se tornar uma forma poderosa de feedback capaz de aumentar a habilidade dos agentes em resolver problemas difíceis
  • Testes também têm muito valor, e podem ficar ainda melhores com testes baseados em propriedades e fuzzing
  • Só testes não bastam, e há limites inerentes para cobrir, apenas com eles, o espaço de estados que um programa pode explorar
  • Na experiência de programação com OxCaml, agentes se beneficiam bastante das garantias universais oferecidas pelo sistema de tipos
  • Se o sistema de tipos consegue impedir condições de corrida de dados, então ele pode eliminar condições de corrida de dados
  • Se os tipos forem estruturados de forma a tornar impossíveis vulnerabilidades de cross-site scripting, então é possível eliminar essas falhas de um jeito que testes simples dificilmente conseguem
  • Tipos ajudam a aliviar o gargalo de verificação e a fornecer feedback melhor ao programar com agentes
  • O uso de técnicas de prova mais poderosas pode abrir espaço para melhorias adicionais

Por que fazer isso aqui

• O mundo todo está pensando no que os agentes significam para o futuro da programação, e há muitas startups tentando combinar métodos formais e agentes
• A Jane Street consegue controlar profundamente a linguagem que usa, o que permite ajustá-la para ficar mais adequada a técnicas orientadas a provas
• Há várias direções possíveis
  • É possível integrar especificações modulares de propriedades ao sistema de tipos
  • É possível adicionar restrições em nível de tipo para elementos como propriedade e mutabilidade, facilitando certas provas
  • É possível incorporar técnicas de prova diretamente na linguagem

• Uma comunidade de programadores preparada

  • Na Jane Street, existe uma comunidade de programadores pronta para adotar esse tipo de técnica
  • Para quem trabalha com linguagens de programação, é mais difícil fazer com que boas ideias de programação sejam usadas no trabalho real do que criar essas ideias
  • Na Jane Street, é comum que usuários reclamem porque novos recursos prometidos e incomuns do sistema de tipos não chegam rápido o bastante
  • Há muitas pessoas com a base necessária para usar essas técnicas, e o interesse em produzir resultados corretos e software de alta qualidade já está estabelecido
  • Uma base de usuários ativa e com altas expectativas dá liberdade para tentar melhorias de curto prazo e visões de longo prazo ao mesmo tempo
  • Melhorias de curto prazo podem ter impacto relativamente rápido
  • A visão de longo prazo pode se tornar uma meta mais ambiciosa, alcançável ao longo de vários anos
  • É possível aprender com as tentativas de curto prazo enquanto se constrói em direção aos objetivos de longo prazo

• Relação com ferramentas externas

  • O trabalho do mundo externo não é ignorado, e há expectativa e inspiração no que está sendo feito em várias comunidades de linguagens de programação
  • Entre as ferramentas relacionadas estão Lean, Dafny, Rocq, Agda, Iris
  • A empresa está buscando formas de integrar o OxCaml com algumas dessas ferramentas para aproveitar a excelente infraestrutura que já existe
  • Também vê vantagens únicas que só podem ser realizadas ao lidar simultaneamente com a linguagem e com as técnicas de prova

Como se juntar

• A Jane Street está procurando pessoas para trabalhar com métodos formais em Londres e Nova York
• As entrevistas e a formação da equipe para essas vagas ainda estão em estágio inicial
• Há uma enorme quantidade de trabalho pela frente, e a empresa está buscando pessoas para se juntar ao time

Complemento

• Modelos ainda precisam de ajuda e orientação humanas ao lidar com provas complexas
• Programadores humanos podem ter ideias sobre por que um sistema funciona e sobre como demonstrá-lo em alto nível
• A maioria dos programadores não sabe como codificar ideias de prova de uma forma que satisfaça um sistema de prova específico
• Modelos podem automatizar grande parte do trabalho repetitivo e fornecer especialização nos detalhes técnicos da escrita de provas
• Escapes como Obj.magic podem permitir contornar restrições no nível de tipos
• Se essas exceções forem rastreadas e proibidas na maior parte do código, é possível chegar muito perto de garantias universais
• Métodos formais podem tornar explícito por que o uso desses escapes é de fato seguro

[GN⁺]

Comentários do Hacker News

• Trabalhei com provas de correção décadas atrás, e na época o sistema tinha mais automação de provas do que muitos sistemas posteriores.
  A parte fácil era resolvida pelo simplificador Oppen-Nelson, o primeiro solver SAT, e a parte difícil ficava com o provador Boyer-Moore, que usava heurísticas e lemas anteriores. O trabalho difícil para humanos era sugerir lemas que o provador pudesse tentar e depois reutilizar em provas futuras.
  Os sistemas posteriores parecem ter reduzido a automação, e acho que os métodos formais saíram do rumo porque se apegaram demais ao formalismo em vez da prática. Do ponto de vista de quem queria código sem bugs em projetos comerciais, parecia que os projetos acadêmicos tinham caído num viés de matemático, preferindo notações concisas para artigos e análise de poucos casos.
  Na prática, é preciso muito trabalho automatizado pesado e pouca necessidade de insight. Pessoas inteligentes continuaram criando novas lógicas, como lógica modal e lógica temporal, para evitar a verbosidade de provas com papel e lápis, mas isso não ajudou muito. A verdade básica desta área é que a maioria dos teoremas é bastante comum.
  Como o pessoal da Jane Street diz, o fato de poder controlar a linguagem é uma grande vantagem. As afirmações de verificação deveriam estar integradas à linguagem de programação; se ficam enfiadas em comentários, em outra sintaxe ou em arquivos separados, só aumentam trabalho desnecessário. Parece bom que a Jane Street esteja empurrando nessa direção.
  Fiz esse trabalho cedo demais, há mais de 40 anos, e naquela época levar cerca de 45 minutos de tempo de computação para construir teoria dos números do zero com o provador Boyer-Moore era normal, mas agora leva menos de 1 segundo.
  https://archive.org/details/manualzilla-id-5928072/page/n3/m...

  • Como alguém que trabalha com métodos formais há muito tempo, acho um pouco difícil concordar com a ideia de que novas lógicas não ajudam. As lógicas industriais são práticas e permitem escrever de forma muito concisa propriedades sofisticadas que os sistemas precisam satisfazer.
    A lógica ocupa, em ciência da computação e engenharia de software, um papel parecido com o do cálculo em física, engenharia mecânica e engenharia civil. Coisas como LTL e a mais recente lógica de separação foram avanços enormes.
    A popularidade razoável de TLA+ é prova disso, e model checking é muito prático. O ponto interessante agora é que métodos formais mais pesados, especialmente prova de teoremas, podem ficar baratos o bastante para uso até em software de sistemas geral.
    Escrever uma especificação formal para uma função, sintetizá-la com um híbrido de SAT/SMT, provador de teoremas e LLM, e receber uma prova de correção pode virar padrão em breve.
    On the Unusual Effectiveness of Logic in Computer Science: https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf
    From Philosophical to Industrial Logics: https://www.cs.rice.edu/~vardi/papers/icla09.pdf
  • Em especificação formal, o fato de pessoas conseguirem interpretar e escrever isso vai se tornar realmente importante.
    O que preocupa é o surgimento de matemática difícil de decifrar, guardada por um pequeno grupo de fiéis. Diferentes notações obscuras não seriam compatíveis entre si, e entender uma talvez ajudasse pouco a entender outra. A maioria acabaria escrevendo apenas frases em inglês que não podem ser verificadas de fato.
    Pior ainda: pode-se deixar a máquina formalizar suas próprias frases e, sem entender esse formalismo nem a prova, participar de um teatro de verificação e depois fingir surpresa quando tudo explodir.
  • Fico curioso se você já olhou Ada/SPARK. Se sim, também queria saber se isso bate com sua intuição sobre como esse trabalho deveria ser feito.
    Eles estão lentamente tentando integrar esse tipo de capacidade nas partes que o sistema de tipos não consegue tratar rapidamente, então me interessa a visão de quem já percorreu esse caminho antes.

• Muito bom. Nos últimos meses, em Scala 3, venho usando tipos expressivos para fazer os tipos carregarem cada vez mais provas em tempo de compilação. Não uso macros, mas algumas parecem úteis.
  Isso não só ajuda a reduzir o problema da proliferação de testes agentivos, como também parece evitar que o agente caia em formas de trabalho de baixa qualidade. Em especial, impede o acúmulo de substantivos, em que o agente tenta criar um novo tipo nominal para tudo, mesmo quando deveria generalizar de forma razoável.
  Acho que o lado que acelera código de agentes com boa qualidade é o das ferramentas parecidas com métodos formais, inclusive linguagens com sistemas de tipos fortes.
  Aqui, por tipos expressivos, quero dizer técnicas que eu não gostaria de colocar numa base de código comum se a equipe já não estivesse habituada a programação em nível de tipos. Ou seja, precisa ser uma equipe para a qual tipos de ordem superior e funções de tipo não sejam esquisitices, mas blocos básicos.
  Em termos de conhecimento, os agentes costumam ser melhores em “matemática” do que a maioria dos desenvolvedores, e muitas vezes melhores até do que desenvolvedores obcecados por teoria das categorias. Além disso, se considerar que têm paciência “infinita” para conversa, também ensinam muito bem.
  Pessoalmente, pedi ao Codex para converter algumas provas de hobby para algo no estilo Lean, e foi muito fácil. Não estou dizendo que esteja 100% “correto”; para verificar mais a fundo eu precisaria aprender mais Lean 4, mas basicamente ele parece checar até armadilhas clássicas de prova. Estou muito animado com o futuro dos métodos formais.

• Parece ser uma proposta de deslocar o valor humano para o lado da verificação, já que a Gen AI produz muito código. Às vezes penso no que programação realmente é
  Para quem não tem o inglês como língua nativa, aprender programação em si já é um grande desafio. Para entender documentação em inglês que não foi traduzida, é preciso depender de tradução automática, e os materiais no meu idioma estão atrasados uns 5 ou 6 anos
  Agora que ficou impossível revisar manualmente dezenas de milhares de linhas de código geradas por IA, parece haver uma discussão sobre estabelecer regras absolutas, como provas matemáticas. Ao ler este texto, pensei no borrow checker do Rust. Na prática, depois de usar Rust algumas vezes, as pessoas acabam desenvolvendo o mau hábito de recorrer a gambiarras para fugir do borrow checker
  Quando o rigor matemático é excessivo, as pessoas acabam procurando desvios. Programadores com pouca formação, como eu, tendem especialmente a fazer isso
  Acho que esse tipo de tentativa vai acabar resultando em código escrito apenas para respostas formalizadas específicas. Se isso se padronizar assim, não tenho certeza de que conseguirá responder às demandas humanas
  Essas tentativas de programação defensiva são aceitáveis, mas, usando uma expressão minha, eu quero fazer programação agressiva. É um modo de trabalhar em que se aceita o risco, mas se corrige e implanta rápido, acreditando que, com o tempo, ficará bom o suficiente
  Claro, em indústrias já estabelecidas como a Jane Street, onde a precisão é importante e o escopo do trabalho é bem definido, a abordagem deste texto faz sentido. Isso porque há dados suficientes para modelar adequadamente as exigências do mercado
  Mas, para um fracassado social como eu, que vive se movendo em busca de uma mina de ouro para ganhar dinheiro, essa metodologia parece um luxo. Sei que negócios já existentes, com modelagem madura, exigem otimização contínua por profissionais especializados e muito bem formados, e na prática não dá para acompanhar essa demanda. Por isso procuro lugares onde a modelagem não está estruturada, mas nem aí sei se essa abordagem serviria

  • É preciso ver isso do ponto de vista da Jane Street. Eles são uma empresa de trading de alta frequência e negociam ações e instrumentos financeiros na casa dos milhões, talvez até das dezenas de milhões
    Lá não existe isso de “depois a gente corrige”. Quando você entender o que deu errado, talvez já tenha perdido bilhões
    Por isso, a abordagem agressiva pode funcionar em áreas não centrais
    Aliás, a abordagem defensiva já é usada em vários lugares. Python, Java etc. têm garbage collector, e isso de certa forma verifica que o código executa como pretendido
    Eu me perguntava quando a verificação formal começaria a aparecer, mas é natural sair da fase de se preocupar com detalhes de implementação para a fase de descrever o problema de forma científica e matemática
  • Gostei da expressão “programação agressiva”. Só que esse paradigma já é o estado padrão da indústria
    Por causa da Gen AI, o custo da programação defensiva caiu muito, e o custo da verificação humana subiu bastante. Já as técnicas formais tornam a verificação barata, mas trazem um grande overhead de implementação, como escrever especificações, tipos e provas, além de entortar a implementação para encaixá-la em um molde rígido
    Só que a Gen AI pode automatizar esse trabalho pesado. As duas foram feitas uma para a outra
  • Se você depende de tradução automática para ler documentação em inglês não traduzida, fugindo um pouco do assunto, eu recomendo fortemente aprender inglês
    Exige um pouco de esforço, mas eliminar esse overhead constante de tradução deve ajudar enormemente
  • Concordo que essa metodologia é um luxo. O texto também reconhece isso, e a Jane Street é uma organização especialmente preparada para se beneficiar dessa abordagem
  • É natural que a Jane Street publique um texto assim porque isso é relevante para ela, e também é natural que isso não se aplique de forma geral a toda programação
    Só não entendo bem como se autodenominar “fracassado social” ou dizer que não segue esse tipo de prática na carreira se relaciona com esse ponto

• Tenho brincado com ideias parecidas recentemente, e o que me surpreendeu foi o quanto os modelos de ponta, especialmente o ChatGPT-5.5, conseguem completar bem certas provas manuais em Roqc, o antigo assistente de provas Coq
  As provas nem sempre ficam bonitas, mas o ChatGPT frequentemente consegue, em poucos minutos e dentro de 10 a 100 iterações, demonstrar algo que levaria bem mais tempo para mim, mesmo eu tendo experiência limitada, mas não nula, com assistentes de prova e uma experiência de domínio relativamente grande na área dos lemas que estão sendo provados
  O que torna isso interessante no contexto deste pequeno texto é que isso abala uma premissa básica de funcionamento de certas ferramentas de métodos formais. Frama-C, Ada/SPARK etc. focam em gerar obrigações de prova que ferramentas como CVC5 e Z3 consigam resolver automaticamente e, quando isso falha, passam para a alternativa bem dolorosa de fazer a prova manualmente em Roqc
  O fluxo comum é descobrir que alguma obrigação é “difícil”, ou seja, não é resolvida automaticamente, e então reestruturar o conjunto de lemas auxiliares e assertivas visíveis no ponto do código que gera a obrigação para torná-la “fácil”, ou até mudar o próprio código
  Isso faz sentido num mundo em que provas em Roqc custam o dobro. Elas são difíceis para humanos escreverem e ainda sofrem muita variação de manutenção quando o código e as provas ao redor mudam
  Mas, se a prova em Roqc virar “resolução automática com IA no loop”, essa diferença de custo desaparece. Aí seria possível escrever provas como se escreve código, priorizando em primeiro lugar a clareza legível por humanos, e deixando a otimização para compiladores ou provadores para bem depois. Ainda não processei totalmente as implicações disso, mas acho bastante interessante

  • Quando os requisitos mudarem e você ficar numa situação em que não dá mais para provar, qual é a chance de a IA simplesmente mudar o código e os requisitos para facilitar a prova
    Nunca lidei com provas, mas às vezes já vi a IA, quando se diz “depois da mudança este teste falhou”, alterar o próprio teste em vez de corrigir o código para que ele passe tanto no teste antigo, que era a minha intenção, quanto no novo teste
  • Minha experiência é parecida, mas eu escolhi Lean. Tinha mais relação com as funcionalidades que eu queria criar
    Estou animado com o futuro
  • Quando você diz que o ChatGPT consegue fazer uma prova em Roqc em poucos minutos e dentro de 10 a 100 iterações, fico curioso sobre como você sabe se a prova em si está correta

• Sempre que leio sobre especificações formais, parece “escrever os mesmos testes de outro jeito” e, pior ainda, “escrever a mesma implementação de outro jeito”
  Escrever duas vezes pode até ajudar a encontrar erros, mas, se a especificação formal também pode ter exatamente os mesmos bugs que os testes ou a implementação, não entendo muito bem o que ela tem de especial
  O problema fundamental é que, para provar formalmente que um programa faz alguma coisa, é preciso definir essa “alguma coisa” de forma muito específica. Aí, na prática, isso acaba parecendo reescrever os testes ou a implementação
  Tenho acompanhado esse tema de forma intermitente há alguns anos, e continuo com a sensação de que estou deixando passar alguma coisa, mas não sei o quê. Alguém poderia explicar?

  • Como na famosa frase de Dijkstra, “testes de programas podem mostrar a presença de bugs, mas nunca a sua ausência”
    A limitação dos testes é que você só consegue testar comportamentos que imaginou que poderiam ser um problema. Para corrigir preventivamente até comportamentos que você nem sabia que poderiam dar errado, é preciso recorrer a ferramentas mais incomuns. Fuzz testing é um começo nessa direção, e a verificação formal é outro
    Claro, a qualidade dessas ferramentas depende de quão bem você consegue escrever um modelo formal abrangente, que permita os comportamentos desejados e proíba os indesejados, e em muitas áreas ainda estamos surpreendentemente longe disso
  • A grande diferença é que métodos formais permitem usar o quantificador universal de para tudo
    Por exemplo, em um teste unitário você pode escrever “foo('abc') retorna uma string sem espaços em branco no final”
    Mas, com métodos formais, você pode provar “para qualquer entrada x, foo(x) retorna uma string sem espaços em branco no final”
    É um exemplo trivial, mas dá para imaginar algo mais complexo, como “para qualquer programa P, compile(P) se comporta da mesma forma que P”
    Claro, é preciso definir o que significa “se comporta da mesma forma”
  • Não uso isso em software, mas em projetos de ASIC e FPGA as especificações de métodos formais permitem que ferramentas como SAT solvers determinem se o projeto em questão satisfaz a especificação
    Você define propriedades do projeto, e a ferramenta testa o projeto de várias maneiras para verificar se alguma delas pode violar essas propriedades
    Por exemplo, em um sistema que controla semáforos, você pode especificar a propriedade de que faixas que se cruzam não podem ficar verdes ao mesmo tempo, nem ambas dentro de um certo intervalo de tempo
    A ferramenta verifica isso por busca exaustiva e pode mostrar o rastreamento de código que viola a regra
  • É mais do que simplesmente “escrever os mesmos testes de outro jeito”. Cada teste tende a ser em grande parte independente ou crescer até ficar impossível de administrar, e a completude do conjunto de testes acaba sendo avaliada por formas relativamente grosseiras de sobreposição, como cobertura de branches
    Um sistema de tipos comprovado estaticamente faz com que cada componente seja previamente verificado em encaixe com todos os demais. Não é só “este teste passa”, mas sim a garantia de que, quando combinados, “todos esses testes formam um todo razoável e coerente”, impedindo que um modelo inconsistente seja implementado no código
    É parecido com pegar a exigência de o match do Rust cobrir completamente todos os branches possíveis e ampliá-la para a escala de toda a base de código
    É verdade que isso não impede erros fundamentais de lógica ou de teoria. Mas você pode se surpreender com o quanto isso é mais robusto, por exemplo, do que combinar sistema de tipos de Haskell, testes funcionais ad hoc e testes baseados em propriedades. Tudo isso já forma um conjunto forte, mas criptografia formalmente provada opera em um padrão muito mais alto
  • A diferença poderosa está entre um teste específico e uma prova exaustiva. Se você não pensar em um teste de condição de contorno, ele simplesmente passa despercebido. Com um bom modelo, dá para saber que ele existe e corrigi-lo antes do deploy
    Isso é especialmente valioso em cenários de concorrência, distribuição e multithreading. Race conditions e deadlocks são extremamente difíceis de testar e de raciocinar, e problemas como “A, B, C podem acontecer na ordem A, C, B?” entram aí
    Acho que a maturidade dessa área deve evoluir mais ou menos assim. Primeiro, LLMs vão acelerar muito o aprendizado e o uso de métodos formais, mesmo que no início fiquem só em uma verificação posterior no estilo “segunda tentativa”
    Segundo, vamos caminhar para automações em que a LLM verifica “o código de implementação mudou; parece que isso quebrou o modelo?”. Ainda não será algo determinístico, mas provavelmente já será muito melhor do que depender de revisão humana para algo que muda só de vez em quando
    Terceiro, o verdadeiro salto estará em levar para o próximo nível as ferramentas de “escreva apenas a especificação formal e gere a implementação”. Já existem vários projetos de geração de código assim, mas a maioria ainda não amadureceu totalmente até o nível que as empresas querem. E se ferramentas com LLM pudessem acelerar aqueles 1 ou 2 anos de trabalho manual necessários para adaptar uma delas às suas necessidades?

• Vale a pena ver também o post anterior de Kleppmann https://martin.kleppmann.com/2025/12/08/ai-formal-verificati..., e naturalmente faz sentido avaliar se algo pode ser colocado no sistema de tipos ou no linter
  Espero que surjam formas mais fáceis de usar isso. Entre as ferramentas mencionadas no texto, parece que Dafny e Iris são as mais próximas do uso industrial. Também sei que o Amazon S3 tem histórico de uso interno de TLA
  Mas ainda não vi surgir o equivalente ao TypeScript nessa área: algo que se encaixe naturalmente nas ferramentas existentes, funcione como uma abstração sem custo e que as pessoas realmente prefiram ao modo antigo de trabalhar
  Até usar linters customizados ainda é bem ruim. O golangci-lint é uma base de código dolorosa, e nunca usei semgrep, mas o mecanismo de regras dele sempre pareceu intimidador. Também ainda não usei nenhuma API de AST de que eu realmente gostasse

• Esse tipo de elogio ao raciocínio dedutivo, ou seja, às “técnicas formais”, sempre deixa de fora sua limitação fundamental: o quanto axiomas e definições se encaixam bem no domínio-alvo
  É como dizer: “em teoria, não há diferença entre teoria e prática. Na prática...”. Imagino que a Jane Street manterá uma grande base de código com mapeamento 1:1 porque o propósito do código é implementar algoritmos determinísticos. Muitos desenvolvedores trabalham em áreas assim, mas milhões não. A maior parte das UIs, a maior parte do trabalho exploratório etc. não é assim
  Em paralelo às técnicas formais, também existe uma corrente que tenta definir critérios de aceitação em alta resolução, embora não por meios lógicos ou matemáticos. Essa corrente pelo menos encara o problema do mapeamento, mas não o resolve na maioria dos lugares em que o mapa não é o território
  A página de resultados de busca do Google tem um framework interno de otimização extremamente evoluído, mas será que realmente chegou ao ponto ótimo? Será que um protótipo improvisado para capturar uma ideia vaga poderia ter mostrado melhor? Perguntas assim são melhor respondidas olhando para fora do sistema que ele serve, e não para dentro dele

  • Técnicas formais são exatamente para domínios com semântica bem definida
    Circuitos lógicos, componentes de CPU com muita verificação formal, kernels, protocolos, parsers, compiladores, criptografia, frameworks de segurança, primitivas de concorrência etc. se beneficiam muito de verificação
  • Na prática, a maior parte das UIs acaba se reduzindo a máquinas de estados, e isso combina muito bem com verificação formal
    Para aprender mais, o texto do Hillel Wayne é um bom ponto de partida: https://www.hillelwayne.com/formally-specifying-uis/
  • A página de resultados do Google em si não é bem definida, mas provavelmente mais de 90% do código por baixo dela é
    E em alguns casos dá para aprender mesmo quando o resultado não é bem definido, então não é apenas uma questão de sentar e pensar no que faria sentido

• Do ponto de vista de alguém com algum interesse em design e implementação de linguagens de programação, esta frase foi realmente interessante: “para a maioria das pessoas que trabalham com linguagens de programação, a parte fácil é ter ideias novas e melhores para tornar a programação melhor. A parte difícil é convencer alguém a usar essa ideia em trabalho real”
  Concordo totalmente. Há um limite para a quantidade de estranheza que se pode colocar em uma nova linguagem, mesmo que haja benefícios
  Mas agentes de IA provavelmente não terão grande resistência a ideias radicalmente novas no design de linguagens de programação. Tenho pensado há algum tempo em como o design de linguagens pode evoluir depois da IA agêntica
  Será muito interessante ver que novas ideias podem ser criadas para melhorar linguagens de programação quando houver muito menos preocupação com adoção
  https://steveklabnik.com/writing/the-language-strangeness-bu...

• Estou trabalhando para aplicar técnicas formais em testes de segurança de aplicações, e acho que a mesma abordagem pode ser aplicada à verificação de lógica de negócio
  Para isso, estamos usando taint analysis. É uma abordagem de técnicas formais bem estabelecida, mas ainda não foi amplamente aplicada em campo por causa da complexidade do fluxo de dados em bases de código reais
  Expandir técnicas formais para além de correspondência de padrões em AST e checagem simples de tipos é um trabalho realmente difícil. Foram necessários anos de P&D para chegar ao nível de rastrear, com taint analysis, o fluxo de dados interprocedural em bases de código reais em poucos minutos e encontrar vulnerabilidades profundamente escondidas
  Se tiver interesse, você pode ver o projeto: https://github.com/seqra/opentaint

• Há cerca de 18 meses fiquei obcecado em usar tipos com LLMs, e comecei a levar lean4 a sério há uns 6–8 meses. Agora eu nem considero usar assistência de IA em trabalho de software sem uma base de prova CIC com FFI prático para C/C++, e portanto conectável a praticamente tudo
  Banimos tudo, de JSON a Python, e até reescrevemos nix para que tivesse um compilador. Quase tudo que usamos não só passa por testes de propriedades e vários testes de fuzz levados ao limite, como também tem pelo menos provas em lean4 que acionam testes de propriedades via ligação .olean. Quando sobra tempo, chegamos a provar completude do domínio inteiro e também testamos essas propriedades
  As partes rápidas são todas geradas em lean4, então pulamos a discussão C++/Rust. Há vantagens quando um bug em C++ na verdade é um bug no código lean4, mas pode ir para qualquer lado
  É uma mudança grande, e não culpo quem fique cético com “banir JSON e Python?”. Mas já verificamos milhões de linhas dessa forma, e IA + sistema formal é um salto muito maior do que sair de sem IA para IA com Python. Este último, pela nossa experiência, não progride de forma monotônica, mas o primeiro quase sempre progride monotonicamente
  Dá para fazer coisas bem ousadas. Isto é uma prova formal de computação tensorial politópica multifacetada, do tipo modelado por coisas como ISL e CuTe, e com isso dá para fazer swizzling e tiling em dispositivo com mdspan do C++23 e ainda provar que está correto. Este exemplo, porém, não mostra muito bem um argumento “à la L'Hôpital” sobre cobertura: https://github.com/b7r6/mdspan-cute
  O resultado é realmente rápido, e rápido já na primeira tentativa
  https://straylight.software/assets/lambda-hierarchy.svg

  • Colocar Agda e Idris 2 abaixo de CIC torna o diagrama da hierarquia lambda enganoso, mesmo na melhor interpretação
  • Então fico curioso sobre que tipo de software foi feito e por que ele é útil