Verificação

A última redefinição. Verificação formal costuma ser um mundo à parte — uma linguagem separada, uma ferramenta separada, uma chave tudo-ou-nada. Makoto a dobra dentro da mesma linguagem como um espectro que você sobe.

A ideia

“Verificação” na maior parte da indústria significa um de dois extremos. Ou você tem nada — o type checker pega erros de forma e todo o resto é um teste, um panic em runtime, ou um incidente em produção — ou você vai para o outro lado e adota um proof assistant (Coq, Agda, Lean, Idris), uma linguagem separada com um modelo mental separado, onde verificar qualquer coisa significa verificar naquele mundo e depois de algum jeito voltar. O meio é pouco povoado: um refinamento aqui, um linter ali, raramente compondo.

Makoto parte de uma premissa diferente: uma linguagem de sistemas que promete resiliência deve ao programador um jeito de declarar uma garantia e o compilador merecê-la — e esse jeito deve ser a mesma linguagem, invocado em fragmentos, cobrado por fragmento.

Como Makoto redefine

Verificação não é um modo; é uma escada. Toda garantia tem a mesma forma — uma obrigação sobre um predicado — e o compilador descarrega cada obrigação no degrau mais alto possível: irrepresentável no tipo se der, dobrada em comptime se os valores forem conhecidos, provada por um solver invocado se a aritmética exigir, checada em runtime se preciso, e, no fundo do poço, afirmada por um humano que assina por ela. A única lei é que uma obrigação que não pode ser cumprida num degrau cai para o degrau de baixo, nunca para fora da escada. Uma garantia nunca some em silêncio; ela degrada, visivelmente, para a forma honesta mais forte que sobra.

Dessa única imagem tudo o mais decorre. Disciplinas de posse (@must_consume, @consume_once), refinamentos (@where), protocolos de sessão (@protocol), cercas de efeito e terminação (@pure, @total), e tipos dependentes com provas (@proof) são todos degraus — cada um um decorador ou um tipo, cada um opt-in, cada um invisível ao código que não pede. Model checking (@spec) é a única peça que mora numa extensão, e a divisão é deliberada: a teoria da prova tem décadas e pertence ao core, enquanto o engine de um model checker é volátil e pertence atrás da fronteira da extensão.

O raciocínio

Três das próprias réguas de Makoto decidem a forma.

O teste opt-in (capítulo 01) é o porteiro. Um refinamento, uma prova, um protocolo — nenhum pode vazar para o código de quem não os usa. É por isso que cada um é invocado por um decorador ou um tipo, nunca tecido na gramática que todos leem: um .mko que não prova nada é idêntico a um escrito antes desta camada existir. É @supervisor de novo — sofisticação que está lá quando você busca e sumida quando não.

Unificar por conceito (capítulo 01) é por que a camada quase não adicionou vocabulário novo. Um refinamento é um contrato (@requires/@ensures, capítulo 07) que viaja com o tipo em vez da função, então reusa o próprio jeito do contrato de nomear um valor — referência-por-tipo, ou o slot nomeado de um retorno nomeado — em vez de inventar um it mágico. Posse no nível-de-tipo é a flow-analysis do @transfer (capítulo 02) elevada do parâmetro para o decl. Uma prova é um programa (Curry-Howard): uma função recursiva total cujo match é a indução, então não há keyword theorem nem linguagem de táticas no core. dual é um operador-de-tipo porque produz um tipo espelhado, não um decorador, que só anota. A camada cresceu generalizando o que já existia, não parafusando um segundo sistema.

Nomes honestos (capítulo 12) resolveram as palavras. Os termos acadêmicos são linear e affine; os decoradores são @must_consume e @consume_once, porque quem lê o código deve aprender a consequência pelo nome e encontrar a teoria uma vez, na doc — e porque eles formam família com o @consume existente, então todo o realm de memória-e-posse fala um dialeto só.

E a decisão core-versus-extensão repousa na régua do capítulo 11 e da seção 20 do design doc: o estável fica no core, o volátil vira extensão. Teoria de tipos dependentes é estável desde os anos 1970 e roda em quatro linguagens de produção; é core. O engine de um model checker — busca limitada, heurísticas de state-explosion, pontes para ferramentas externas — vira com o estado da arte; é extensão. A liberdade pré-1.0 de crescer o core é gasta no que ainda será verdade em vinte anos, e negada ao que não será.

Por que não as alternativas

• Por que não o borrow checker do Rust? Porque é o anti-exemplo contra o qual a linguagem inteira é construída (capítulo 00): uma disciplina de verificação que vaza para toda assinatura, paga por todos, sempre. Makoto mantém a garantia (um recurso usado o número certo de vezes) e paga por ela só nos tipos que pedem, porque shared-nothing (capítulo 04) torna a análise local — sem lifetimes para threadar.
• Por que não uma linguagem de prova separada, ou um tipo de arquivo .mkop? O primeiro instinto foi isolar a camada de prova atrás da própria extensão de arquivo, como a UI é isolada. Mas a UI merece um tipo de arquivo por volatilidade e uma gramática radicalmente diferente (markup); a camada de prova não é nem uma coisa nem outra — ela só adiciona ao sistema de tipos, e sua teoria é estável. O que de fato precisa de isolamento não é a sintaxe (uma fronteira de arquivo) e sim a soundness (uma cerca semântica): provas só são consistentes sobre um fragmento total, puro e estritamente-positivo. Essa cerca é @proof, opt-in-por-uso — não um arquivo que todos precisam saber que existe.
• Por que não o modelo Bend/Kind — provar tudo, rodar num runtime nativo de prova? Porque isso é tudo-ou-nada no degrau de cima, e paga o custo do degrau de cima em todo lugar. A escada de Makoto deixa um programa provar os 5% críticos, refinar o próximo pedaço, checar o resto em runtime, e deixar o grosso intocado — e as partes provadas apagam para funções comuns com os índices sumidos, então não há imposto de proof-runtime no código que as chama.

A dor concreta

O acesso a índice que era “obviamente dentro do bound” até o dia em que não era. Os dois endpoints de canal, cada um esperando receber, e o processo que travou em vez de crashar honestamente. A transação commitada num braço de um if e silenciosamente esquecida no outro. A função comptime que loopou para sempre e levou o compilador junto (um bug real que a campanha achou). O erro de unidade que jogou uma sonda num planeta. Cada um é uma obrigação que ninguém tinha onde declarar, então ficou sem checagem até falhar. O trabalho da escada é dar a cada uma delas um degrau.

O modelo mental

Uma garantia é uma obrigação sobre um predicado, e o compilador a descarrega no degrau mais alto possível — irrepresentável se puder, provada se precisar, checada se não puder ser provada, assinada por você no último caso. Você sobe a escada uma obrigação por vez, e nada que você não invoca jamais te custa.

A fricção aceita

Provas custam tempo de autoria — o termo tedioso, a indução escrita à mão — e esse custo é real; a aposta (a do capítulo 11, e a virada da indústria) é que tempo de autoria num kernel crítico é mais barato que os incidentes que ele previne, e que o custo cai só no fragmento que o invocou. Duas fricções menores são nomeadas de propósito. @total vira obrigatório em qualquer função comptime usada num tipo — uma obrigação nova onde antes não havia — porque uma prova unsound é pior que nenhuma prova; é o preço de o kernel ser confiável. E o topo ergonômico da camada — táticas, o bloco @by — é deliberadamente diferido para o self-hosting, porque fazê-lo direito precisa do próprio AST do compilador como library, e com ele vêm três problemas permanentes ditos em voz alta em vez de descobertos tarde: higiene de macro, o AST como contrato público, e atribuição de erro através da expansão. A camada entrega sem eles, e é escrita para que eles a embrulhem depois sem retrabalho.

Volta ao índice