Gabriela Moreira, CEO da Quint na Informal Systems – Série de Entrevistas

Gabriela Moreira, CEO da Quint na Informal Systems, é uma engenheira de pesquisa especializada em linguagens de programação e métodos formais, com um foco forte em construir ferramentas que tornem a verificação de sistemas complexos mais acessível aos engenheiros. Ela lidera o desenvolvimento da Quint, uma linguagem de especificação executável moderna baseada em TLA+, onde ela continua a manter e evoluir a linguagem e sua ferramenta. Seu trabalho abrange verificação formal, análise estática e ferramentas de desenvolvedor, e ela também contribuiu para a academia ensinando métodos formais, refletindo uma combinação de engenharia prática e profundidade teórica.

Quint, desenvolvida e mantida na Informal Systems, é uma linguagem de especificação moderna projetada para modelar, testar e verificar sistemas complexos, como redes distribuídas, blockchains e bancos de dados. Construída sobre as fundações da Lógica Temporal de Ações (TLA), a Quint introduz uma sintaxe mais amigável para desenvolvedores, juntamente com ferramentas avançadas como verificação de tipos, simulação e verificação de modelos, permitindo que os engenheiros detectem falhas de sistema antes do deploy. A plataforma enfatiza especificações executáveis, permitindo que os desenvolvedores não apenas descrevam o comportamento do sistema, mas também o testem e explorem ativamente, fechando a lacuna entre a correção teórica e a implementação do mundo real.

Voltando ao início, o que primeiro despertou seu interesse em programação, e como você eventualmente encontrou seu caminho para métodos formais e sistemas distribuídos?

Eu era uma jogadora ávida com um computador ruim, e percebi que gostava de consertar os problemas e fazê-lo funcionar. Eu me inscrevi em ciência da computação e fui atraída pela teoria e compiladores. 

Em 2015, fui apresentada a concursos de programação. Neles, você geralmente recebe alguns exemplos de entrada e saída esperada, e você escreve o código que resolve o problema e funciona para esses exemplos. No entanto, após você submeter para avaliação, o código é na verdade testado com muitos mais exemplos além dos que eles mostram. Essa realização de que o código pode funcionar para os cenários que eu vejo ou penso, mas ainda falhar em casos que eu não considerei, tornou a programação em um tipo de desafio que eu me apaixonei.

Trabalhando na indústria, fui rapidamente atraída por sistemas distribuídos, onde tínhamos que considerar diferentes ordens em que as mensagens poderiam chegar, diferentes modos de falha e um mundo de comportamentos ocultos. Em 2018, um colega me apresentou a uma linguagem de especificação formal chamada TLA+. Eu fiquei viciada. Eu imediatamente comecei a construir ferramentas em torno do TLA+ e tenho trabalhado nesse espaço desde então.

Você construiu sua carreira em torno de métodos formais e linguagens de programação, desde seu trabalho inicial em ferramentas baseadas em TLA+ até liderar o desenvolvimento da Quint na Informal Systems. O que motivou você a se concentrar em tornar a verificação formal mais acessível, e como essa visão moldou o design da Quint?

TLA+ é muito bom para não ser usado extensivamente na indústria. Eu ainda era bastante júnior quando aprendi sobre ele, e eu me juntava a essas chamadas com meus colegas de trabalho para tentar encontrar soluções juntos, e eu estava constantemente encontrando cenários em que nossas soluções falhariam. No entanto, eu era sempre a última linha de defesa contra esses cenários na maioria dos casos. Eu imaginei que havia uma maneira melhor, menos custosa e mais valiosa de resolver esses cenários. Assim, a ideia de usar métodos formais para criar especificações antes de implementar o código foi criada. Então, eu comecei minha jornada acadêmica em direção a isso, o que me levou à Informal Systems e à Quint.

Quint não foi originalmente concebida como um produto. Nós a construímos por necessidade na Informal Systems. Nós estávamos escrevendo especificações TLA+ para sistemas que precisávamos confiar mais do que fazíamos, mas que não se expandiam além de um pequeno grupo de pessoas, pois a sintaxe era muito assustadora com muitos símbolos matemáticos, e a ferramenta não atendia às expectativas básicas das pessoas. Nós mostrávamos colegas e colaboradores externos: “olhe para essa coisa incrível que eu fiz”, mas eles não podiam lê-la e não tinham tempo para aprender uma nova ferramenta.

As escolhas de design na Quint seguem diretamente dessa experiência. A linguagem é fácil de ler e lembrar. A primeira coisa que construímos foi uma extensão do VSCode que destaca erros à medida que você digita. Ela tem tipos e modos distintos para separar camadas explicitamente. Ela tem um REPL para que você possa explorar interativamente e um simulador para que você possa obter feedback rápido e iterar. Ela exporta traços para um formato JSON padrão que é fácil para máquinas analisarem. Essas foram coisas que os programadores já esperavam de suas ferramentas e que nós mesmos precisávamos. A verificação por baixo é a mesma lógica do TLA+.

Eu estou obcecada em tornar os métodos formais mais acessíveis, e enviar ferramentas é emocionante, mas o impacto real só é sentido se as equipes de engenharia realmente usá-las. Há ainda uma diferença entre o que as ferramentas podem fazer e como úteis elas parecem para os desenvolvedores, e estou trabalhando para fechar essa lacuna.

Para os leitores que não estão familiarizados com isso, como você explicaria o que é a Quint e por que uma nova linguagem de especificação foi necessária ao lado de ferramentas existentes como o TLA+?

A maioria das especificações é documentação. Você escreve o que o sistema deve fazer e verifica isso lendo-o. O problema é que a documentação está errada de maneiras que não podem ser detectadas mecanicamente: nomes não definidos, comportamento ambíguo, suposições implícitas. Você geralmente descobre durante a implementação ou em produção.

Uma especificação da Quint é algo que você executa. Você modela o sistema como uma máquina de estado, define as propriedades que ele deve satisfazer e executa ou verifica o modelo. Se houver uma violação, você obtém um contraexemplo mostrando exatamente a sequência de passos que dispara isso. Isso muda quando e como barato você pega um erro de design.

TLA+ sempre pôde fazer isso. A Quint torna isso prático para engenheiros que não são especialistas em lógica temporal.

A Quint é projetada para fechar a lacuna entre métodos formais e engenharia de software do dia a dia. Quais foram as principais barreiras de usabilidade que você visou eliminar em comparação com as abordagens tradicionais?

Honestamente, a maior barreira de usabilidade era a sintaxe. É por isso que começamos com a sintaxe. Depois de abordar isso, pudemos nos concentrar mais em outros fatores. O sistema de tipos e efeitos da Quint veio para sinalizar tantos erros quanto possível antes de começar o processo de verificação regular, e as pessoas valorizaram isso muito. Isso nos levou a escrever especificações de alta qualidade que até mais pessoas pudessem ler. Nós as integramos em editores e oferecemos a funcionalidade básica que todos os desenvolvedores têm o direito de esperar.

O maior impacto após isso foi nosso simulador. Ele começou como apenas uma maneira de oferecer às pessoas o primeiro feedback sobre o comportamento do sistema, como um desenvolvedor quer ser capaz de, de alguma forma, executar o código após escrevê-lo. Então, ele se tornou extremamente valioso como uma maneira de obter confiança em especificações que são grandes demais para a verificação lidar, desde que a expertise de adaptar uma especificação para torná-la viável para verificação não deve ser levada como certa. Nosso simulador tornou a confiança mais acessível e temos usado extensivamente em muitos projetos.

Meu maior ponto de dor com a sintaxe do TLA+ foi como frequentemente eu misturava minhas barras e barras regulares, e você precisa digitar essas coisas muito. Eu gosto mais da sintaxe da Quint, mas o que realmente a torna impossível de voltar para mim é toda a ferramenta.

Uma das principais forças da Quint é sua capacidade de modelar e testar sistemas distribuídos antes do deploy. Como isso muda a forma como os engenheiros devem pensar sobre a construção de sistemas como blockchains ou infraestrutura em tempo real?

A maior mudança é mover a validação mais cedo. Leslie Lamport, criador do TLA+, compara escrever especificações antes do código a desenhar plantas antes do trabalho de construção. Mesmo se você já construiu algo sem uma planta, ainda é uma boa ideia escrevê-la agora e usá-la para informar suas mudanças posteriores.

Na indústria de software, usamos arquivos markdown e quadros brancos. Talvez você possa comparar isso a tentar descrever um prédio textualmente. Isso funciona, mas você saberia se o tamanho das paredes soma? A Quint oferece uma maneira de descrever sistemas onde você pode ser tão de alto nível quanto desejar e obter insights sobre seu comportamento e correção.

A Quint se baseia nas fundações do TLA+, que é amplamente usado para descrever sistemas distribuídos. Como você equilibrou manter esse rigor teórico enquanto tornava a linguagem mais amigável para desenvolvedores?

A chave foi restringir a Quint a um fragmento do TLA (a lógica por trás do TLA+) em vez de expor tudo o que a lógica permite. O TLA é muito expressivo, e parte dessa expressividade inclui operadores que não são suportados por nenhuma ferramenta e permite combinações que as pessoas entendem e usam de forma errada, tornando as coisas muito difíceis de depurar. Nós fizemos uma escolha deliberada: ficar com o que as especificações realistas realmente precisam e evitar o que tem potencial para confusão.

O sistema de tipos e efeitos adiciona restrições, mas restrições que são úteis. Eles impedem uma classe inteira de erros de especificação que não são divertidos quando encontrados após a verificação já estar em andamento. Os tipos são quase inteiramente inferidos e os efeitos são ocultados dos usuários, então isso adiciona valor com nenhum atrito.

Antes de eu aprender sobre a existência do TLA+, eu estava fazendo trabalho de pesquisa em sistemas de tipos, o que significa que o verificador de tipos da Quint foi provavelmente meu componente favorito para escrever. Eu me lembro de beber um café sabor paçoca em meus primeiros meses na Informal enquanto revisava algum artigo de sistema de tipos e pensava “minha vida é incrível”. 

Tornar a linguagem boa para usar enquanto ainda mantém a correspondência com o TLA+ (pois as especificações da Quint podem ser transcompiladas para TLA+) foi um exercício de linguagem de programação, e as discussões com a equipe foram o recurso mais útil, seguido de feedback de usuários iniciais. Há melhorias que ainda queremos fazer, e pode ser minha parte favorita do trabalho.

Você também trabalhou em análise estática e sistemas de tipos. Como essas experiências influenciaram a verificação de tipos da Quint, a ferramenta e a experiência geral do desenvolvedor?

A maior lição que eu aprendi nesse mundo é que nem todas as linguagens são iguais. Você ouvirá pessoas dizendo que é apenas uma questão de aprender uma nova sintaxe, todos os conceitos ainda se aplicam, então todas as linguagens são iguais e é apenas uma questão de gosto. Isso não é verdade. O campo de linguagens de programação tem grandes pesquisadores que fazem um trabalho incrível para avançar nesse campo, e isso não é apenas para fazer uma linguagem parecer mais bonita ou mais do seu agrado.

A programação funcional foi introduzida a mim muito cedo, eu aprendi Haskell ao mesmo tempo que aprendi C (minha primeira linguagem de programação), e sou muito grata por isso. Isso é a base que me ajuda a ver que isolar mutações de estado e não determinismo em uma camada fina na Quint, e ter toda a complexidade em funções puras, objetivamente ajuda em muitos fatores, e não é apenas uma questão de gosto. Eu não acho que construir a Quint teria sido produtivo se questões de gosto estivessem sujeitas a discussão com frequência.

Ensinar métodos formais como um professor lhe dá uma perspectiva única. Quais são os conceitos errados mais comuns que os engenheiros têm sobre verificação formal hoje?

Bem, eu estava ensinando estudantes de graduação que estavam apenas começando na indústria. A grande maioria deles nunca ouviu falar de métodos formais ou verificação formal antes, então não havia conceitos errados! O currículo foi feito de tal forma que a maioria deles também não aprendeu sobre sistemas distribuídos, e cerca de metade deles aprenderia sobre threads no mesmo semestre. Eu costumava dizer a eles que me sentia como se estivesse ensinando a eles o que um guarda-chuva é bom antes que eles tivessem experimentado qualquer chuva!

Eu estava mais motivada a ensinar a eles como os métodos formais e especificar formalmente um sistema podem ajudá-los a raciocinar sobre soluções e encontrar casos de bordo do que fazê-los pensar que devem verificar formalmente todos os softwares que eles escrevem. Meu trabalho final foi um setup de RPG de mesa onde diferentes pedidos que os jogadores podiam fazer e diferentes configurações tinham que ser levados em conta, tentando imitar as dificuldades que enfrentamos em sistemas distribuídos tanto quanto possível. Isso foi bem-sucedido em ser difícil o suficiente para que eles tivessem que usar as ferramentas para encontrar casos de bordo e melhorar suas soluções para derrotar os monstros no final. Espero que, quando eles enfrentarem uma situação semelhante no trabalho um dia, eles se lembrarão de mim. Alguns deles já fizeram.

Há um interesse crescente em combinar IA com desenvolvimento de software. Você vê um papel para a IA em ajudar os desenvolvedores a escrever, validar ou até mesmo gerar especificações formais usando ferramentas como a Quint?

Um papel significativo, e isso já está acontecendo. A Ciência da Computação é maior do que escrever código, e a IA abre a porta para novas maneiras de usar métodos formais. LLMs são bons em escrever especificações da Quint a partir de descrições de linguagem natural de um sistema e até mesmo código existente. O Kit LLM da Quint tem agentes Claude Code que pegam uma descrição em inglês de um protocolo e produzem uma especificação da Quint que você pode executar e verificar imediatamente.

Ao mesmo tempo, a Quint também ajuda os desenvolvedores a confiar no código escrito com IA. Eu acredito firmemente que a confiança precisa vir do entendimento, não de alguns checkmarks mágicos. Trabalhar em uma especificação da Quint que impulsiona e verifica o código de implementação significa que os desenvolvedores ainda podem possuir e entender o comportamento do sistema, abordando a dívida cognitiva que o uso da IA pode criar e fornecendo maneiras mais assertivas de validar o código gerado.

Nós aproveitamos os LLMs como ferramentas de linguagem que escrevem definições precisas da Quint a partir da intenção de linguagem natural, e então damos as ferramentas da Quint para a IA para que ela possa realizar coisas que ela não pode fazer confiavelmente sozinha, como encontrar casos de bordo.

Olhando para o futuro, o que precisa acontecer para que os métodos formais sejam adotados como parte padrão do ciclo de vida do desenvolvimento de software?

Por um tempo agora, eu sei que as duas coisas de alto nível que a Quint precisa para mais adoção: custo mais baixo e valor mais alto. Eu acho que isso se aplica a muitas outras coisas também. Os métodos formais acabaram de receber um grande impulso em ambas as coisas, com a IA reduzindo significativamente o custo de escrever especificações formais e também criando o ambiente de falta de confiança e entendimento onde os métodos formais podem ser os mais impactantes e valiosos.

Com a IA mudando o que nossa profissão é, pelo menos em algum grau, eu espero que essa mudança seja em direção a escolhas de design de alto nível e correção de comportamento, tornando os métodos formais uma ferramenta do dia a dia; e não em direção a não entenderemos mais nenhum código ou sistema e passaremos todo o nosso tempo revisando o código gerado pela IA sem nenhuma ferramenta para nos ajudar a raciocinar sobre isso.

Obrigada pela entrevista esclarecedora; os leitores interessados em saber mais sobre essa linguagem de especificação executável para modelar e verificar sistemas complexos, incluindo sua ferramenta e como começar, podem explorar Quint.