Estou trabalhando na especificação Concrete v2. A primeira versão já tem código funcionando e aprendemos muito ao implementá-la. Agora adicionei alguns recursos novos e interessantes que vêm do Zig, Austral, Lean/Coq. Estou criando uma linguagem de sistemas em torno da verificação formal desde o início, com algumas funcionalidades interessantes. Características: - kernel formalizado em Lean 4 - tipos lineares (estilo Austral, não afim de Rust) - empréstimos sem anotações vitalícias - capacidades para rastreamento de efeitos - alocador aprovado como capacidade (estilo Zig) - puro por padrão - ! para funções impuras (de Roc) Como eles compõem: Tipos lineares são a base. Cada valor consumido exatamente uma vez. Sem vazamentos, sem duplo grátis, sem uso após o livre. Segurança de memória sem GC. É mais prolixo, mas mais concreto e claro do que os tipos afins. Tomar empréstimo torna a linearidade utilizável. Referenciar temporariamente um valor sem consumi-lo. Regiões lexicais em vez das anotações de vida de Rust. O compilador infere o que o Rust faz você escrever. As capacidades acompanham os efeitos. Uma função que lê arquivos declara isso. Uma função que aloca declara isso. Sem declaração, não há efeitos, garantido. grep with(Network) encontra todas as funções que tocam a rede. O alocador como capacidade torna a alocação visível. Código sem with(Alloc) comprovadamente nunca toca o heap. Você controla qual alocador serve qual caminho de código. Arena, pool, alocação de stack, tudo explícito. Puro por padrão inverte o modelo usual. Efeitos exigem declaração. O caso comum (computação pura) não precisa de anotação. O kernel magro liga tudo. Quando o compilador diz que seu programa é seguro, essa afirmação é respaldada por provas.