Desenvolvedor recria Terraform em Lean 4: se compila, deploya

O projeto

O desenvolvedor NGrislain passou dois fins de semana construindo infra, uma ferramenta de infraestrutura como código escrita em Lean 4 que replica o ciclo do Terraform: você declara os recursos desejados, a ferramenta observa o que as contas de nuvem realmente contêm e reconcilia a diferença. O projeto cobre três nuvens (AWS, Scaleway e Google Cloud), catorze tipos de recursos, com cerca de 15.000 linhas de Lean em 107 commits. Não é software de produção, e o objetivo do texto é discutir o que um sistema de tipos real oferece a uma ferramenta de IaC.

Onde os erros são pegos

A diferença em relação ao Terraform está em onde os erros aparecem. Referências a recursos inexistentes, campos obrigatórios ausentes, serviços que a nuvem não tem, tamanhos de instância inválidos e regiões onde a nuvem não atua viram erros de compilação. Já nome de bucket duplicado por outra pessoa, quota, capacidade e consistência eventual permanecem problemas de execução. O autor resume a promessa com honestidade: compilar não garante que o apply vá funcionar - garante apenas quais falhas ainda estão em jogo.

O que o Terraform não consegue dizer

Em HCL, referências como aws_security_group.web.id são resolvidas no grafo do Terraform, mas o campo não é obrigatório (removê-lo gera uma instância no grupo padrão em vez de erro) e .id é uma string, então nada impede passar um id de subnet. Na versão em Lean, a referência carrega a nuvem e o tipo do recurso no próprio tipo: omitir o campo, nomear um grupo fora do arquivo ou passar um bucket não compila. Um recurso com campo obrigatório faltante nem chega a existir como valor - o que sobra é uma função esperando argumento.

Tamanho de instância e região também deixam de ser strings. O tipo de instância é um par família/tamanho verificado por by decide, cobrindo 257 combinações válidas - incluindo casos que uma lista curada erraria, como o salto do gen-7 Intel. Localidades são nomes neutros mapeados por nuvem (paris vira eu-west-3 na AWS e fr-par na Scaleway), e o conjunto de locais legais para uma frota é computado, não mantido à mão - a lista cresceu sozinha quando a Scaleway abriu Milão.

Segredos e valores desconhecidos

Segredos têm um tipo com apenas duas fontes (variável de ambiente ou valor composto), sem Repr ou serialização JSON - a impressão manual mostra <redacted>. Um plano é verificado quanto à sanidade da fonte, e envolver um literal em map para disfarçá-lo não passa na checagem.

Terraform tem uma regra (um valor desconhecido pode preencher um campo, mas não pode decidir quantos recursos existem) sem conseguir enunciá-la uma vez só - ela aparece atributo por atributo como erro em tempo de plan. Em Lean, a linguagem de expressões tem cinco construtores, e deliberadamente não há como ramificar sobre um valor desconhecido. Assim, uma declaração nunca pode ter um número desconhecido de servidores, e o plano é sempre computável. Um atalho de interpolação de strings esconde a restrição sem relaxá-la.

Por que tipos dependentes ajudam

O autor lista quatro ganhos: tipos que mencionam valores (região da AWS e da Scaleway são tipos distintos); o compilador executa verificações suas via Assert, em vez de um linter separado que pode discordar; uma tabela única de lugares serve para autocomplete, checagem e asserções, sem divergir como o código Go do provider, a documentação e a memória; e um recurso pela metade nunca é um valor com nulos. A frase-síntese: o conjunto do que se pode escrever pode ser aproximado do conjunto do que se pode implantar. Um detalhe considerado essencial: tabelas antigas não devem travar o usuário, e Region.raw/InstanceType.raw aceitam strings como saída de emergência.

O que roda e os limites

A CI executa cinco declarações em sequência nas três nuvens (12 recursos na AWS, 12 na Scaleway, 10 no Google Cloud), incluindo escalonar e destruir. Postgres gerenciado e muitos caminhos de atualização não rodam. O autor reconhece que tipos não resolveram tudo: rastrear recursos criados é uma questão de eventos, não de bem-formação, e ele precisou redescobrir por que o estado do Terraform é remoto. Um erro real - uma descrição com apóstrofo rejeitada pela AWS - mostra que o sistema de tipos só checa restrições que você pensou em escrever.

Conclusão

A resposta a "devo usar isso?" está na diferença de escala: catorze tipos de recursos contra milhares do Terraform, três nuvens contra centenas de providers, sem registro de módulos, state locking ou fluxo de equipe. Para infraestrutura real nesta semana, use Terraform. O que vale levar para uma ferramenta séria é mais estreito: fazer do estado desejado um valor de tipo estreito, deixar o compilador rodar suas verificações e dar a toda tabela de consulta uma saída deliberadamente feia. As 15.000 linhas restantes são clientes HTTP - e é essa a parte com bugs.