Ideias & Insights

Explorando desenvolvimento AI-first, guardrails de código e a arquitetura da descartabilidade.

model-checkingllmrustformal-proofs

LLMs conseguem gerar código Rust. Provas formais são um problema completamente diferente.

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…
model-checkingtemporal-logicformal-methodsverification

Você pode verificar código com model checking sem aprender temporal logic

Bounded model checkers como Kani e relational model finders como Alloy permitem verificar propriedades com assertions e constraints ordinários. Você abre mão de provas de liveness por uma curva de aprendizado medida em horas, não em semanas.

Você não precisa aprender lógica temporal linear para usar um model checker. Ferramentas como Kani, CBMC e Alloy permitem verificar propriedades com assertions…
model-checkingrustverificationformal-methods

Você pode provar que seu código Rust está correto sem escrever uma única prova, mas o espaço de estados é a conta

Ferramentas de model checking como Kani permitem verificar propriedades de Rust com assertions em vez de provas formais. O problema é o que acontece quando seus loops não têm limites pequenos.

Você pode provar que seu código Rust está correto sem escrever uma única prova. A ferramenta que faz isso se chama model checker, e para Rust o mais prático no…
model-checkingdistributed-systemstlaplusprotocol-design

Você não pode fazer unit test de um protocol distribuído, mas pode fazer model checking

Bugs distribuídos são caros de corrigir após o deploy. O model checking permite que você os encontre antes de escrever uma única linha de código de implementação. Veja como fazer isso com TLA+.

Você não pode fazer unit test de um protocol distribuído. Um unit test executa um processo em uma máquina em uma ordem. Seu protocol executa dez processos em…
dsls-bounded-contextinfrastructureconfig-managementdevops

Copiar arquivos `.env` entre ambientes não é uma estratégia de configuração

Como equipes de infraestrutura gerenciam configuração entre dev, staging e production usando DSLs por contexto que tornam as diferenças entre ambientes explícitas e com segurança de tipos.

Seu ambiente de staging funciona. Seu ambiente de production não. A diferença entre os arquivos deles tem 400 linhas, e metade dessas linhas são comentários em…
dsls-bounded-contextllmconstrained-generationgrammar

Grammar-constrained decoding: forçando LLMs a emitir sintaxe válida em cada token

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…
dsls-bounded-contextdesign-systemsllmthemes

Traduzir do inglês para um tema é fácil. Torná-lo determinístico é o verdadeiro problema.

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…
dsls-bounded-contextdslparser-combinatorstypescript

Deixa o arquivo de gramática de lado: escreve o teu parser DSL em TypeScript simples

Os geradores de parsers são excessivos para a maioria das DSLs de contexto limitado. Os combinadores de parsers permitem-te construir um parser funcional na mesma linguagem da tua aplicação, sem código gerado e sem passos de build.

Se alguma vez abriste um arquivo de gramática Yacc e te perguntaste por que construir uma linguagem exige aprender uma segunda linguagem, não estás sozinho. Os…