Como se tornar um programador melhor fazendo pequenas provas na cabeça

• Para se tornar um programador melhor, é importante criar o hábito de fazer pequenas provas mentalmente ao escrever código
• Monotonicidade, imutabilidade, pré e pós-condições e invariantes são conceitos centrais nessas mini provas
• Ao projetar, considerar o alcance do impacto que uma mudança no código causa em todo o sistema (isolamento, firewall) ajuda muito a reduzir complexidade e risco
• Usar indução permite provar passo a passo a correção de funções ou estruturas recursivas
• Esse tipo de raciocínio é desenvolvido com prática e repetição, e o treino com provas matemáticas reais e resolução de problemas de algoritmo ajuda bastante

---

Introdução e ideia central

• O autor, ao ganhar experiência, passou naturalmente a adotar o hábito de “desenhar pequenas provas” para aumentar a precisão e a velocidade do código
• O processo de verificar e raciocinar mentalmente sobre o comportamento esperado durante a programação exige prática, mas, quando se domina, melhora visivelmente a qualidade do código
• O importante não é exatamente como fazer isso; é algo que pode ser praticado de várias formas, do jeito que melhor funcionar para cada pessoa

Monotonicidade (Monotonicity)

• Monotonicidade (monotonicity) é a propriedade de uma função ou código avançar em apenas uma direção
• Um exemplo é o checkpointing: as etapas do trabalho só avançam, sem voltar atrás para executar de novo o que já foi concluído
• No exemplo de LSM tree em comparação com B-tree, a LSM tree geralmente acumula espaço e só o reduz durante o processo de compactação
• Quando a monotonicidade é garantida, fica mais natural excluir ou prever certos estados complexos ou partes do resultado
• Imutabilidade (immutability) é um conceito parecido: como um valor definido uma vez nunca muda, é possível descartar a possibilidade de transições de estado

Pré e pós-condições (Pre- and post-conditions)

• Pré-condição (pre-condition) e pós-condição (post-condition) são afirmações que devem ser verdadeiras obrigatoriamente antes e depois da execução de uma função
• Ao escrever funções, acompanhar essas condições explicitamente ajuda no raciocínio lógico e nos testes
• Quando a pós-condição está bem definida, fica mais fácil derivar casos de teste unitário
• Adicionar assertions ao código para verificar essas condições e interromper cedo em situações inesperadas aumenta a previsibilidade e a segurança
• Às vezes é difícil até mesmo definir pré e pós-condições claras para uma função, e perceber isso por si só já traz bons insights

Invariantes (Invariants)

• Invariantes são propriedades que devem ser sempre verdadeiras em qualquer situação: antes, durante e depois da execução do código
• Um exemplo clássico de invariante é a equação contábil da contabilidade por partidas dobradas (total de créditos = total de débitos)
• Se você dividir o código inteiro em etapas menores e provar que cada etapa preserva o invariante, consegue garantir a integridade do todo
• Há abordagens que usam listeners ou métodos de ciclo de vida para manter invariantes (como construtores/destrutores em C++ e useEffect no React)
• Quando há poucas mudanças ou os caminhos são simples, verificar invariantes se torna muito mais fácil

Isolamento (Isolation)

• Um dos pontos centrais de um bom software é adicionar ou modificar funcionalidades sem tornar o sistema existente instável
• É preciso entender o “raio de impacto” (blast radius) de uma mudança no código e criar “firewalls” estruturais para minimizar a propagação desse impacto
• No exemplo real do serviço Nerve, é apresentada uma forma de projetar limites claros entre o planejador de consultas e o executor de consultas, impedindo que a parte alterada ultrapasse essa fronteira
• Evitar a propagação desnecessária de mudanças facilita a validação e a manutenção, além de aumentar a estabilidade
• Isso também está alinhado com a filosofia do OCP (Open-Closed Principle): expandir funcionalidades sem alterar o comportamento existente

Indução (Induction)

• Muitos programas incluem funções recursivas ou estruturas recursivas, e a indução é uma ferramenta poderosa para formalizar o raciocínio sobre elas
• Para provar passo a passo o funcionamento e a correção de uma função recursiva, é preciso verificar separadamente o caso base (base case) e o passo indutivo (inductive step)
• O texto usa como exemplo o processo de simplificação de nós em uma AST (árvore sintática), mostrando como argumentos indutivos em cada etapa provam a preservação dos invariantes e o funcionamento correto
• Quando o raciocínio indutivo se torna natural, escrever e validar código recursivo fica muito mais intuitivo e fácil
• Também vale comparar isso com tentativas de validação global (holistic), para refletir sobre qual abordagem parece mais natural

Proof-affinity como métrica de qualidade

• O autor defende a ideia de que um bom código é aquele em que é possível fazer pequenas provas mentalmente
• Quando o código tem estruturas como monotonicidade, imutabilidade, condições claras, divisão por invariantes, limites de firewall e uso de indução, ele de fato se torna mais fácil de provar e, por isso, tende a ter qualidade maior
• Se o código é difícil de entender e de validar, isso sugere a necessidade de refatoração ou de repensar sua estrutura
• Nesse contexto, o autor propõe o termo proof-affinity em vez de “provabilidade”
• Proof-affinity não é o único elemento da qualidade de software, mas é um facilitador muito importante para compreender, expandir, testar e manter código

Como evoluir

• Esse tipo de raciocínio lógico precisa de prática acumulada para passar a ser aplicado naturalmente, quase sem perceber
• Escrever provas (matemáticas) com frequência e desenvolver a capacidade de inferência lógica é essencial
• Resolver problemas de algoritmos (como os cursos da EdX de Stanford, Leetcode etc.) também é um ótimo campo de treino; focar em problemas que exigem implementação cuidadosa e raciocínio de prova, e não apenas truques, traz mais resultado
• Em vez de ajustar a resposta várias vezes até acertar, é importante praticar chegar o mais perto possível da resposta correta já na primeira tentativa
• Ao transformar isso em hábito, a capacidade de projetar sistemas lógicos e a qualidade do código melhoram bastante

[GN⁺]

Comentários no Hacker News

• Há um exemplo simples, mas surpreendente, que se encaixa perfeitamente neste tema: a busca binária. Existem variações para a esquerda e para a direita, mas, se você não pensar sobre o invariante do loop, é muito difícil implementá-la corretamente. Este texto explica a abordagem por invariantes e mostra um exemplo de código em Python correspondente. Jon Bentley, autor de Programming Pearls, pediu a programadores da IBM que implementassem uma busca binária comum, e 90% tinham bugs. Na maioria das vezes, eram erros que levavam a loops infinitos. Naquela época também era preciso prevenir overflow de inteiro manualmente, então dá para entender até certo ponto, mas ainda assim é uma proporção surpreendente

  • Depois de ver isso, comecei a usar busca binária como pergunta de entrevista. Cerca de 2/3 dos candidatos, inclusive alguns bem conhecidos, não conseguiam fazer uma implementação que funcionasse corretamente em 20 minutos. Especialmente em casos fáceis, muitos acabavam em loop infinito. Os que conseguiam, implementavam rápido. Uma das causas do problema é que muita gente aprende com uma interface errada. A explicação da Wikipédia também diz para “inicializar L com 0 e R com n-1”, o que define um intervalo com R incluso. Na prática, porém, na maioria dos algoritmos de strings, é melhor usar um limite superior exclusivo, ou seja, R igual a n. Eu gostaria de testar essa hipótese diretamente. Queria pedir para muitas pessoas escreverem com protótipos de função e valores iniciais diferentes, e comparar quantos bugs aparecem ao usar limite superior inclusivo, exclusivo e abordagem por comprimento

  • Na verdade, a busca binária é praticamente o exemplo clássico mais difícil quando se trata de gerenciar índices. Junto com o algoritmo de partição de Hoare, é um dos algoritmos básicos mais difíceis de codificar com exatidão e sem erros

  • Como teste, pedi ao Claude Sonnet que escrevesse um código Python de busca binária sem bugs

  def binary_search(arr, target):
      left = 0
      right = len(arr) - 1
      while left <= right:
          mid = left + (right - left) // 2
          if arr[mid] == target:
              return mid
          elif arr[mid] < target:
              left = mid + 1
          else:
              right = mid - 1
      return -1
  

  Também confirmei vários casos de teste com um array de exemplo

  • Sabendo que bugs em busca binária são famosos por causa de más práticas ensinadas como modelo, me desafiei a colocar no livro a minha primeira implementação sem bugs. Escrevi com extremo cuidado, mas ainda assim havia um bug, o que é até engraçado. Felizmente, graças ao sistema de feedback antecipado da Manning, consegui corrigir antes da impressão

  • Eu sempre implemento busca binária à esquerda/direita guardando “o melhor valor até agora”. É o estilo de lower_bound e upper_bound do C++. Na estrutura while (l < r), encontro o ponto médio, verifico a posição atual e ajusto o intervalo de forma apropriada. Por exemplo, no caso de upper_bound, elevo o limite esquerdo, e no de lower_bound, reduzo o limite direito. Faz tempo que não resolvo LeetCode e minha cabeça está meio travada, então o formato pode estar meio ruim

• Acho que conheci um conceito parecido numa disciplina de pós-graduação há muito tempo. Perto do fim da graduação, eu fazia provas de matemática só de caneta. Não sei bem por quê, mas minhas notas eram sempre altas, e era porque eu resolvia tudo de uma vez, só depois de ter desenhado completamente o processo mentalmente. Isso reduzia muito os erros. Quando programo, também começo só depois de ter planejado tudo de forma razoavelmente completa na cabeça

• Para se tornar um programador melhor, é preciso criar o hábito de escrever pequenas provas no código Testes e definições de tipos são exatamente exemplos disso Eu abordo especialmente na ordem: primeiro testes, depois tipos, por último código É desejável criar testes para cada critério de aceitação e escrever testes com entrada/saída claramente descritas Se for uma API, dá para criar primeiro uma especificação completa com OpenAPI ou GraphQL, incluindo todas as propriedades e tipos. Em tempo de execução, é possível validar dados com base nessa especificação, e a própria especificação se torna uma prova de que a aplicação funciona conforme o especificado Resumindo, é importante garantir, por meio de OpenAPI/GraphQL, testes e tipos, uma prova de que o sistema realmente funciona como pretendido Se a própria especificação for bem projetada desde o início, a implementação do código pode mudar com flexibilidade e ainda assim a especificação prova a correção A especificação é mais importante que o próprio código

  • As cinco propriedades mencionadas no texto podem ser expressas em um bom sistema de tipos. Desse modo, boa parte da especificação vira código, e o compilador garante a correção. O futuro da programação deveria caminhar para tornar essa abordagem algo natural Os sistemas de tipos de OpenAPI e GraphQL são pobres demais; para chegar a esse futuro, ainda seriam necessários uns 50 anos de evolução

• Aprendi fundamentos de ciência da computação teórica na universidade e concordo com a ideia do texto. Não é fácil colocá-la em prática Além de pré-condições e pós-condições, técnicas de prova em CS como invariante de loop (loop invariant) e indução estrutural (structural induction) são extremamente poderosas Recomendo os links de loop invariant e structural induction, junto com as notas da disciplina CSC236H da UofT (notas da aula)

  • Essas notas da CSC236 são excelentes, e o professor David Liu também é muito bom perfil do professor

  • UofT foi mencionada! Fico feliz em ver isso

• A ideia de “fazer pequenas provas mentalmente sobre o código” é um princípio tão importante que deveria ser óbvio. Você deveria sempre ter em mente uma proposição simples sobre o que cada parte do código faz

  • Esse espírito é fácil em projetos greenfield, quando você mesmo escreveu todo o código recentemente, mas parece muito mais difícil em codebases reais, onde vários desenvolvedores mexem em funções diversas e em estado global

    • Um desenvolvedor realmente bom sabe evoluir o sistema gradualmente nessa direção. O código do mundo real é bagunçado, mas é importante reduzir aos poucos os buracos nos invariantes e criar uma estrutura de código que ajude os próximos desenvolvedores a perceber e manter esses invariantes. Documentação ajuda, mas, na minha experiência, a própria estrutura do código tem um papel ainda maior

    • Na verdade, esse é o motivo decisivo de estado global ser perigoso. Para provar a correção do código, você precisa conhecer o programa inteiro. Se transformar variáveis globais em valores imutáveis, passá-las como argumentos de função ou gerenciar o estado com classes wrapper, então basta entender claramente os chamadores daquela função. Se você adicionar mais restrições dentro da função com assertions e afins, a dificuldade da prova cai nitidamente. Muitos programadores já tomam essas decisões, mas fazem isso por instinto, sem pensar conscientemente em provas

    • Código em que vários desenvolvedores administram estado global pode ser comparado a um paciente com “câncer metastático”. É muito mais difícil de tratar, e às vezes só dá para salvar dependendo da sorte e de condições externas

    • Como o artigo diz, esse tipo de código tem muito mais chance de gerar bugs, e também aumenta a probabilidade de bugs adicionais durante a manutenção. Isso mostra que o caminho muito mais correto é escrever desde o início com uma estrutura passível de prova

    • Ao ler este texto, pensei em como estou sempre repensando minha forma de programar e tentando redefini-la em direção a algo melhor. Fico curioso se desenvolvedores como John Carmack também sentem, com o tempo, que seu código antigo era insuficiente e que existe uma percepção de como fazer “melhor” cada vez mais

• A ideia de que o código precisa ser demonstrável surgiu pela primeira vez quando Dekker resolveu o problema de exclusão mútua em 1959. Há uma história interessante sobre isso no texto EWD1303 de Dijkstra (link original). Dá para ver a pesquisa posterior de Dijkstra como uma continuação dessa percepção

• Escrever uma prova correta é realmente difícil. Verificação de programas também não é fácil. Na minha opinião, tentar fazer provas manualmente não é eficiente. Se você escrever código idiomático para a linguagem e a codebase em questão, raramente precisará se preocupar com invariantes ou pré/pós-condições. A ênfase em “simplicidade, clareza e generalidade” de R. Pike e B. W. Kernighan em "The Practice of Programming" tem um efeito enorme na prática. Como algo um pouco relacionado, mas diferente, ao fazer programação competitiva você definitivamente precisa dominar técnicas que garantam a correção do código para passar ao próximo nível

  • Não concordo com isso. Acho que o autor do texto não está falando de prova formal completa, mas de sempre pensar nas propriedades lógicas garantidas pelo seu código, como invariantes. Esse processo é o melhor caminho para entender o código e perder o medo do que ele faz

  • Aqui, na verdade, parece que causa e efeito foram invertidos. Se você aborda o problema pensando com cuidado, o resultado naturalmente será um código claro e limpo. A lógica precisa ser clara para que o desenho do código também seja claro. Mas acreditar que escrever código bonito, por si só, fará a correção aparecer é absurdo. Claro, quanto mais limpo o código, menos bugs tendem a aparecer em code review e afins. É importante lembrar que a forma segue a função

  • O conceito mais básico de prova é “qual é a justificativa de que isso está certo?”. Não é apenas para evitar erros triviais, mas para verificar se a direção está correta em um nível fundamental

  • Para a correção do código, não existe substituto além de escrever o código corretamente. Mesmo sendo difícil, ele precisa ser escrito corretamente de qualquer jeito

  • Se invertermos completamente o primeiro parágrafo, uma abstração apropriada — isto é, código idiomático para a linguagem/codebase — facilita a verificação do programa. Com abstrações apropriadas, não há necessidade de pensar em invariantes de loop e afins, então a prova decorre diretamente da correção do código

• Mutabilidade e imutabilidade (mutable/immutable) também são propriedades importantes. Manter o estado o mais imutável possível reduz a complexidade não só em multithreading, mas também ao raciocinar sobre o estado do programa

  • O artigo original já inclui esse ponto

• Nos anos 80, aprendi esses princípios de forma clara durante a graduação em Carnegie Mellon. Depois disso, eles me ajudaram muito ao longo da vida. Em especial, lembro do momento em que aprendi a equivalência entre recursão e indução, e passei a abordar algoritmos recursivos de forma elegante, em vez de simplesmente “tentar coisas até sair a resposta”

  • Assisti a essa aula recentemente e tive uma percepção ainda maior ao estudar programação funcional