Estoy trabajando en la especificación de Concrete v2. La primera versión ya tiene código funcional y aprendimos mucho al implementarla. Ahora he añadido algunas características nuevas e interesantes que provienen de Zig, Austral, Lean/Coq. Estoy diseñando un lenguaje de sistemas en torno a la verificación formal desde el principio con algunas características interesantes. Características: - núcleo formalizado en Lean 4 - tipos lineales (estilo Austral, no el afín de Rust) - préstamo sin anotaciones de tiempo de vida - capacidades para el seguimiento de efectos - asignador pasado como capacidad (estilo Zig) - puro por defecto - ! para funciones impuras (de Roc) Cómo se componen: Los tipos lineales son la base. Cada valor consumido exactamente una vez. Sin fugas, sin doble liberación, sin uso después de liberar. Seguridad de memoria sin GC. Es más verboso pero más concreto y claro que los tipos afines. El préstamo hace que la linealidad sea utilizable. Referenciar temporalmente un valor sin consumirlo. Regiones léxicas en lugar de las anotaciones de tiempo de vida de Rust. El compilador infiere lo que Rust te obliga a escribir. Las capacidades rastrean efectos. Una función que lee archivos lo declara. Una función que asigna lo declara. Sin declaración significa sin efectos, garantizado. grep con(Network) encuentra cada función que toca la red. El asignador como capacidad hace visible la asignación. El código sin with(Alloc) no toca nunca la pila. Controlas qué asignador sirve qué camino de código. Asignación de arena, de pool, de pila, todo explícito. Puro por defecto invierte el modelo habitual. Los efectos requieren declaración. El caso común (cálculo puro) no necesita anotación. El núcleo de Lean lo une todo. Cuando el compilador dice que tu programa es seguro, esa afirmación está respaldada por una prueba.