Especificación de Concrete

Traducción automática del original en inglés, todavía sin revisar. Leer el original.

Esta página es el panorama vivo del lenguaje y la referencia de diseño de Concrete.

Existe para un trabajo distinto al de los ensayos de la serie. La serie argumenta a favor del diseño. Esta página registra en un solo lugar la forma del lenguaje, sus restricciones y el estado actual de la implementación.

Si querés la introducción editorial más corta, leé Por qué existe Concrete.

Estado

Concrete es real, pero está incompleto.

Hoy el proyecto tiene:

• un pipeline de compilación completo en Lean 4, desde el parseo hasta SSA y la generación de código nativo
• parseo LL(1) estricto
• diagnósticos estructurados en todos los pases semánticos
• seguimiento de capabilities (capacidades) y reportes de auditoría
• fronteras explícitas entre IR, incluyendo Core y SSA
• contratos en el código fuente (source contracts) (#[requires], #[ensures], invariantes de ciclo) compilados a obligaciones de prueba con ids estables
• un flujo de trabajo concrete prove que genera workspaces de pruebas en Lean y vincula los teoremas registrados con sus obligaciones
• reportes de estado de pruebas, bundles de pruebas, VC, trazabilidad, auditoría y diff que mantienen separadas las clases de evidencia
• un test runner integrado, un intérprete, un formateador y herramientas de apoyo como diff de snapshots y un reductor de casos de prueba
• una biblioteca estándar de bajo nivel que sigue creciendo

Lo que todavía no tiene:

• un kernel completamente formalizado y conectado de punta a punta con la implementación
• elaboración y generación de código verificadas
• un gestor de paquetes y un servidor LSP

Principios de diseño

Concrete se organiza alrededor de unas pocas restricciones duras:

1. Puro por defecto.
2. Capabilities explícitas para los efectos.
3. Ownership lineal por defecto.
4. Nada de flujo de control oculto ni limpieza (cleanup) oculta.
5. Una gramática lo bastante chica como para parsearse con un solo token de lookahead.
6. Un lenguaje lo bastante chico como para que los reportes y las pruebas sigan siendo manejables.

Pipeline de compilación

El pipeline actual del compilador es:

Source
  -> Parse
  -> Resolve
  -> Desugar
  -> Check
  -> Elab
  -> CoreCanonicalize
  -> CoreCheck
  -> Mono
  -> Lower
  -> SSAVerify
  -> SSACleanup
  -> EmitSSA
  -> clang / linker

EmitSSA produce LLVM IR, que clang compila y enlaza en un binario nativo. También hay un intérprete integrado como camino de ejecución alternativo, útil para correr programas sin un toolchain nativo y para contrastar el backend.

El punto arquitectónico es que Concrete tiene una frontera semántica real en Core IR y una frontera de backend real en SSA. El Core IR que pasa CoreCheck es un artefacto validado: los pases posteriores pueden asumir que sus invariantes se cumplen, y las herramientas de prueba se enganchan ahí. Eso hace que sea más fácil razonar sobre el compilador.

Tipos

Concrete incluye:

• escalares primitivos: Bool, Int y Uint (de 64 bits por defecto), enteros con tamaño i8/i16/i32 y u8/u16/u32, Float32 y Float64, Char, String, y el tipo unit ()
• registros con struct
• tipos de datos algebraicos con enum, con campos con nombre en las variantes
• tipos genéricos y traits con bounds
• punteros crudos *const T y *mut T para trabajo de bajo nivel y FFI
• referencias con &T y &mut T

La forma es convencional a propósito:

struct Copy Player { points: Int }

enum MyResult {
    Ok { value: Int },
    Err { error: Int },
}

trait Scorer {
    fn score(&self) -> Int;
}

impl Scorer for Player {
    fn score(&self) -> Int { return self.points * 2; }
}

fn evaluate<T: Scorer>(entity: &T) -> Int {
    return entity.score();
}

Copy aparece en la declaración del tipo, así que si un tipo es lineal o se puede copiar libremente se ve en el lugar donde se define. Los valores de un enum se desarman con match, que tiene que ser exhaustivo:

match r {
    MyResult::Ok { value } => { return value; },
    MyResult::Err { error } => { return error; },
}

La dirección de la biblioteca estándar es ordinaria a propósito, no mágica. El objetivo es achicar con el tiempo la superficie que el compilador conoce y dejar más del comportamiento visible para el usuario en código de biblioteca común.

Linealidad

Los valores con dueño son lineales por defecto. Un valor lineal tiene que consumirse exactamente una vez.

Eso significa que:

• olvidarse de un valor es un error de compilación
• usar un valor después de moverlo es un error de compilación
• destruir un valor dos veces es un error de compilación

La limpieza es explícita:

let f = open("data.txt")
defer destroy(f)

Esto es más estricto que el ownership afín de Rust. El objetivo es la visibilidad: el tiempo de vida de un recurso pasa a ser parte del programa en lugar de quedar escondido detrás del comportamiento implícito de Drop.

Copy es explícito y opcional (opt-in). Un tipo solo puede ser Copy si todos sus campos son Copy y no tiene obligaciones de destructor.

Borrowing

El borrowing (préstamo) le permite al código usar un valor sin consumirlo, preservando el ownership lineal del recurso subyacente.

En lugar de inferencia de lifetimes al estilo de Rust, Concrete usa bloques de borrow con alcance. Un bloque de borrow le pone nombre a la referencia y a la región en la que vive:

borrow owner as r in Region {
    // r: &T is available here; owner is frozen
}
// owner is usable again; r no longer exists

borrow mut owner as r in Region {
    // r: &mut T; exclusive access
}

Mientras el bloque está activo, el dueño está congelado: no se puede leer, mover ni volver a prestar. Al salir del bloque, el dueño se descongela y la referencia deja de existir.

Las reglas generales son:

• los borrows inmutables pueden coexistir
• los borrows mutables son exclusivos
• las referencias no pueden escapar de su región: el análisis de escape rechaza una referencia que vive más que su bloque
• las funciones que se pueden llamar de forma segura no pueden devolver referencias, ni directamente, ni anidadas dentro de agregados, ni a través de una instanciación genérica

Concrete mantiene este modelo léxico y explícito a propósito. Evita por completo la maquinaria de lifetimes a nivel de firma, sin parámetros de lifetime y sin reglas de elisión, pero lo logra aceptando una superficie de lenguaje más chica.

Capabilities

Las capabilities son permisos estáticos declarados en las funciones.

Ejemplos:

fn read_file(path: String) with(File) -> String
fn serve() with(Network, Alloc, Console) -> Int
fn hash(data: &Bytes) -> Digest

Una función sin anotación de capabilities es pura. Una función que hace asignación de memoria (allocation) tiene que declarar with(Alloc). Una función que toca archivos tiene que declarar with(File).

El conjunto concreto actual de capabilities es: File, Network, Clock, Env, Random, Process, Console, Alloc y Unsafe. Std es una macro para las capabilities seguras estándar, y los alias de capabilities definidos por el usuario se expanden antes de que el resto del compilador los vea.

Las capabilities se propagan de forma transitiva por el grafo de llamadas. Si f llama a g, y g requiere File, entonces f también tiene que requerir File.

Esto convierte a las capabilities en un contrato público real en lugar de una convención de documentación.

Asignación de memoria

La asignación de memoria se trata como un efecto de primera clase.

Si el código hace asignación en el heap, requiere with(Alloc). La elección del allocator se fija en el punto de llamada en lugar de quedar escondida de forma global.

Eso te da dos propiedades que la mayoría de los lenguajes no exponen de forma limpia:

• la asignación se puede auditar semánticamente
• la estrategia de allocator queda explícita en la estructura del programa

La asignación en el stack no requiere Alloc.

Modelo de confianza

Concrete separa las fronteras de confianza (trust boundaries) de bajo nivel en lugar de colapsarlas en una sola palabra clave amplia.

• Las capabilities expresan efectos semánticamente visibles.
• trusted fn y trusted impl marcan inseguridad interna a nivel de punteros detrás de una API segura.
• trusted extern fn es una excepción acotada para bindings externos auditados.
• with(Unsafe) marca fronteras externas o semánticamente peligrosas.

Esta separación importa porque “hace trucos con punteros internamente” y “puede llamar código externo arbitrario” no son el mismo tipo de riesgo.

Errores

Los errores son valores. Concrete usa Result<T, E> con propagación mediante ?:

fn read_config(path: String) with(File) -> Result<Config, FsError> {
    let f = open(path)?;
    defer destroy(f);
    return parse(f);
}

No hay excepciones ni caminos de unwinding ocultos.

defer se ejecuta al salir normalmente del alcance, incluyendo los returns tempranos que dispara ?.

El abort es aparte e inmediato. Queda fuera de la semántica normal de limpieza.

Contratos y pruebas

Las funciones pueden llevar contratos en el código fuente:

#[requires(0 <= n && n < 32)]
fn rotr(x: u32, n: u32) -> u32 {
    return (x >> n) | (x << (32 - n));
}

Un contrato es una afirmación, no una garantía. El compilador convierte cada afirmación en obligaciones de prueba con ids estables, y después les adjunta evidencia. Las precondiciones se asumen a la entrada de la función y se empujan a cada llamador; las postcondiciones se vuelven obligaciones de salida. Los ciclos llevan invariantes y variantes explícitos.

La evidencia está escalonada en lugar de ser binaria. Una obligación puede estar:

• descargada por un teorema de Lean registrado, verificado por el kernel
• cerrada por un procedimiento de decisión propio de Lean como omega o bv_decide, sin ningún solver SMT externo en la base trusted para esa obligación; bv_decide igual lleva la confianza en código nativo documentada en el inventario de axiomas
• reducida a verdadera por constant folding en un punto de llamada
• asumida, planificada o todavía faltante

El reporte de auditoría muestra la clase de evidencia de cada obligación. Nunca hay una única insignia verde.

concrete prove genera un workspace de pruebas en Lean para una función, vincula los teoremas registrados con sus obligaciones, y soporta replay para que las pruebas queden atadas al código fuente contra el que se escribieron.

Esta es la parte del lenguaje que conecta el argumento de los ensayos con código que corre: el compilador no solo acepta programas, emite los hechos sobre ellos a los que una prueba se puede enganchar.

Traits, módulos y FFI

Los traits son solo de dispatch estático. El lenguaje evita los trait objects y la mayor parte de la maquinaria implícita que suele hacer que los lenguajes de sistemas sean más difíciles de leer y de formalizar.

Los módulos usan imports y visibilidad explícitos. Los imports nombran cada símbolo que traen; todo es privado salvo que esté marcado pub:

import std.fs.{ open, FsError };

FFI existe, pero es deliberadamente acotado. Las declaraciones extern fn requieren tipos seguros para FFI (enteros, floats, Bool, Char, punteros crudos y structs con layout de C), y las fronteras externas se registran explícitamente a través del modelo de confianza:

extern fn malloc(size: u64) -> *mut u8;

Anti-features

Concrete evita a propósito una serie de funcionalidades conocidas:

• garbage collection
• asignación de memoria oculta
• destrucción implícita
• excepciones
• closures con captura oculta
• trait objects
• sobrecarga de operadores
• reflection y eval
• estado global implícito
• shadowing de variables
• comportamiento indefinido en código seguro

No son omisiones por descuido; son restricciones de diseño elegidas para mantener el lenguaje explícito, auditable y manejable de forma mecánica.

Lo que podés decir sobre los programas

Si el checker de Concrete acepta una función, muchas veces podés decir más que “pasa el type checker”.

Según la función, puede que puedas decir que:

• es pura
• no puede hacer asignación de memoria
• no puede llegar a la red
• sus fronteras de confianza son explícitas
• sus puntos de limpieza son visibles
• pertenece al fragmento elegible para pruebas
• sus obligaciones de contrato están descargadas, asumidas o todavía abiertas, con la clase de evidencia visible en el reporte de auditoría

Ese es el punto principal del lenguaje.

Preguntas abiertas

Varias áreas importantes todavía están sin terminar a propósito:

• modelo de concurrencia
• ampliar la conexión con las pruebas: los contratos, las obligaciones y concrete prove existen hoy, pero la mayoría de las obligaciones todavía terminan en pruebas de Lean escritas a mano en lugar de una descarga automática
• frontera del kernel verificado a largo plazo
• un gestor de paquetes y soporte para editores más allá del resaltado de sintaxis

Concrete no intenta esconder que está incompleto. El diseño y la implementación están pensados para converger con el tiempo.