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 ao desenvolvedor, 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 o explorem, 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 os 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 código que resolve o problema e funciona para aqueles exemplos. No entanto, após submeter para avaliação, o código é realmente testado com muitos mais exemplos além dos que eles mostram a você. 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, transformou a programação em um tipo de desafio com o qual 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 inteiro 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 Lógica Temporal de Ações (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 constantemente encontrava cenários em que nossas soluções falhavam. No entanto, eu era sempre a última linha de defesa contra esses cenários na maioria dos casos. Eu imaginei que devia haver uma maneira melhor, menos custosa, 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 as ferramentas não atendiam às expectativas básicas das pessoas. Nós mostrávamos aos 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 padronizado que é fácil para as 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 as usam. Ainda há um delta entre o que as ferramentas podem fazer e quão úteis elas parecem aos 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 problema é que a documentação está errada de maneiras que você não pode detectar 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 etapas que dispara isso. Isso muda quando e quão barato você pega um erro de design.

TLA+ sempre pôde fazer isso. 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 foi 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 mesmo de iniciar 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 integramos tudo nos 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 garantida. 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+ era 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 adicionais.

Na indústria de software, usamos arquivos markdown e quadros brancos. Talvez você possa comparar isso a tentar descrever textualmente um prédio. Isso funciona, mas você saberia se os tamanhos das paredes somam? A Quint oferece uma maneira de descrever sistemas em que você pode ser tão de alto nível quanto quiser 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 ao desenvolvedor?

A decisão-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 realmente difíceis de depurar. Nós fizemos uma escolha deliberada: ficar com o que a maioria das especificações realistas realmente precisa 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 execução. Os tipos são quase inteiramente inferidos e os efeitos são ocultados dos usuários, então isso adiciona valor sem 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 nos meus primeiros meses na Informal enquanto revisava algum papel do 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+ (já que 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 do feedback de usuários iniciais. Ainda há melhorias que 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, a ferramenta e a experiência geral do desenvolvedor da Quint?

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 mesmos 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.

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 para 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 em 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 vasta maioria deles nunca havia ouvido 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 sobre 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 para antes que eles experimentassem qualquer chuva!

Eu estava mais motivada a ensinar a eles como os métodos formais e a especificação formal de um sistema podem ajudá-los a raciocinar sobre soluções e encontrar casos de bordo do que a fazê-los pensar que devem verificar formalmente todos os softwares que já escreveram. 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 consideração, tentando imitar as dificuldades que enfrentamos em sistemas distribuídos o máximo possível. Isso teve sucesso em ser suficientemente difícil 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 de código Claude 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 os comportamentos 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 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 de forma confiável por conta própria, como encontrar casos de bordo.

Olhando para o futuro, o que precisa acontecer para que os métodos formais passem de uma adoção de nicho para uma parte padrão do ciclo de vida do desenvolvimento de software?

Para um tempo, 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 em que 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ós não entendendo mais nenhum código ou sistemas e passando todo o nosso tempo revisando o código gerado pela IA sem nenhuma ferramenta para nos ajudar a raciocinar sobre ele.

Obrigado pela entrevista esclarecedora; os leitores interessados em aprender 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.