Estoy trabajando en la especificación Concrete v2. La primera versión ya tiene código funcional y aprendimos mucho implementándolo. Ahora he añadido algunas características nuevas e interesantes que vienen de Zig, Austral, Lean/Coq. Estoy diseñando un lenguaje de sistemas basado en la verificación formal desde el principio, con algunas características interesantes. Funciones: - kernel formalizado en Lean 4 - tipos lineales (estilo austral, no afín de Rust) - préstamo sin anotaciones de por vida - capacidades para el seguimiento de efectos - asignador aprobado como capacidad (estilo Zig) - puro por defecto - ! para funciones impuras (de Roc) Cómo componen: Los tipos lineales son la base. Cada valor consumido exactamente una vez. Sin fugas, sin doble uso, sin uso tras gratis. Seguridad de memoria sin GC. Es más prolixo pero más concreto y claro que los tipos afines. Pedir prestado hace que la linealidad sea utilizable. Referencia temporalmente un valor sin consumirlo. Regiones léxicas en lugar de las anotaciones vitalicias de Rust. El compilador infiere lo que Rust te hace escribir. Las capacidades registran efectos. Una función que lee archivos lo declara. Una función que asigna lo declara. Sin declaración, no hay efectos, garantizado. grep with(Red) encuentra todas las funciones que tocan la red. El asignador como capacidad hace visible la asignación. El código sin (Alloc) demostrablemente nunca toca el heap. Tú controlas qué asignador sirve a qué ruta de código. Arena, pool, asignación de stacks, todo explícito. Por defecto, puro invierte el modelo habitual. Los efectos requieren declaración. El caso común (computación pura) no necesita anotación. El núcleo Lean lo une. Cuando el compilador dice que tu programa es seguro, esa afirmación está respaldada por pruebas.