9 posts
A verificação Cleanroom exige gerar e descarregar obrigações de prova. Veja como os LLMs automatizam a anotação e a geração de VC para que você possa se concentrar nas provas realmente difíceis.
A engenharia de software Cleanroom exige que você prove que seu código está correto antes de compilá-lo. Isso soa nobre até você passar três horas escrevendo…
Passei 30 dias escrevendo explicações de design antes de pedir código a um LLM. Os resultados mudaram como penso sobre rubber-ducking.
A maioria dos desenvolvedores usa LLMs ao contrário. Descrevemos o que queremos em cinco palavras, recebemos 200 linhas de código e passamos a próxima hora…
Conversas com LLM contêm intenção, alternativas rejeitadas e código funcional. É exatamente isso que a documentação deveria ser. Veja como transformar um chat efêmero em documentos duráveis e pesquisáveis sem perder a narrativa.
Você passou quarenta e cinco minutos com Claude projetando um circuito de retry. Você explicou os modos de falha, rejeitou o backoff exponencial porque esconde…
Inspeções Fagan precisam de quatro a seis pessoas e duas horas para revisar 250 linhas. Um LLM pode cortar esse custo ao cuidar da preparação e da aplicação de checklist, mas não pode substituir os papéis humanos que encontram os defeitos mais caros.
Uma inspeção Fagan completa precisa de um moderador, um leitor, dois a quatro inspetores e o autor. A equipe gasta duas horas revisando aproximadamente 250…
Grandes modelos de linguagem escrevem código Rust surpreendentemente bom, mas quando você pede uma prova formal, eles alucinam invariantes e inventam sintaxe que nenhum verificador aceita. Veja o que eles realmente acertam, onde falham e como usá-los mesmo assim.
LLMs conseguem escrever Rust que compila e até passa em . O que não conseguem fazer de forma confiável é escrever uma prova formal de que o código está correto…
LLMs alucinam sintaxe porque fazem sampling de tokens probabilisticamente. O grammar-constrained decoding filtra o vocabulário a cada passo para que apenas tokens que preservem a validade sintática sejam emitidos.
Peça a um LLM para gerar um objeto JSON e ele eventualmente emitirá uma vírgula no final, uma quebra de linha não escapada dentro de uma string, ou um bare…
Você pode gerar design tokens a partir de descrições simples em inglês, mas apenas se tratar a descrição como uma DSL de contexto delimitado com contrato de schema e snapshot tests.
Sim, você pode descrever um tema em inglês e obter um design system funcional. O truque é que a descrição em inglês não é um prompt. É um arquivo fonte. E como…
Executar múltiplos LLMs em paralelo captura erros que qualquer modelo individual enviaria com confiança. Aqui está como construir um sistema de resolução de divergências que realmente funciona.
Você envia um prompt para o GPT-4o. Ele retorna um blob JSON com uma confiança de 0.97. Você envia o mesmo prompt para o Claude 3.5 Sonnet. Ele retorna um blob…
Programação N-version com LLMs não requer múltiplos modelos. Você pode extrair implementações diversas e corretas de um único modelo variando prompts, personas e restrições de raciocínio.
A programação N-version assume que a diversidade vem de autores diferentes. Com LLMs, isso significa modelos diferentes, provedores diferentes, talvez…