Estou a trabalhar na especificação do Concrete v2. A primeira versão já tem código funcional e aprendemos muito ao implementá-la. Agora adicionei algumas novas funcionalidades interessantes que vêm do Zig, Austral, Lean/Coq. Estou a desenhar uma linguagem de sistemas em torno da verificação formal desde o início, com algumas funcionalidades interessantes. Funcionalidades: - núcleo formalizado em Lean 4 - tipos lineares (estilo Austral, não o afim do Rust) - empréstimo sem anotações de tempo de vida - capacidades para rastreamento de efeitos - alocador passado como capacidade (estilo Zig) - puro por padrão - ! para funções impuras (do Roc) Como se compõem: Os tipos lineares são a base. Cada valor consumido exatamente uma vez. Sem vazamentos, sem duplo free, sem uso após free. Segurança de memória sem GC. É mais verboso, mas mais concreto e claro do que tipos afins. O empréstimo torna a linearidade utilizável. Referenciar temporariamente um valor sem consumi-lo. Regiões lexicais em vez das anotações de tempo de vida do Rust. O compilador infere o que o Rust faz você escrever. As capacidades rastreiam efeitos. Uma função que lê arquivos declara isso. Uma função que aloca declara isso. Sem declaração significa sem efeitos, garantido. grep com(Network) encontra cada função que toca na rede. O alocador como capacidade torna a alocação visível. Código sem with(Alloc) provavelmente nunca toca no heap. Você controla qual alocador serve qual caminho de código. Arena, alocação em pool, alocação em pilha, tudo explícito. Puro por padrão inverte o modelo usual. Efeitos requerem declaração. O caso comum (cálculo puro) não precisa de anotação. O núcleo Lean junta tudo. Quando o compilador diz que o seu programa é seguro, essa afirmação é respaldada por prova.