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.

Revisada por última vez contra el compilador en octubre de 2026.

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:

Puro por defecto.
Capabilities explícitas para los efectos.
Ownership lineal por defecto.
Nada de flujo de control oculto ni limpieza (cleanup) oculta.
Una gramática lo bastante chica como para parsearse con un solo token de lookahead.
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, que también se escriben i64/u64), enteros con tamaño i8/i16/i32 y u8/u16/u32, Float32 y Float64, Char y String. Una función sin tipo de retorno devuelve 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
arrays de tamaño fijo [T; N], que se arman con [a, b, c] o [x; N]
tipos de puntero a función como fn(Int) with(Console) -> Int, que llevan sus capabilities

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; },
}

Algunas declaraciones le ponen nombre a las cosas sin agregar maquinaria. newtype crea un tipo distinto con la misma representación, type es un alias común y const le pone nombre a un valor de tiempo de compilación. Las conversiones entre tipos numéricos siempre se escriben con as; nada se convierte de forma implícita:

newtype UserId = u64;
type Block = [u8; 64];
const MAX_USERS: Int = 1000;

fn first_word(b: Block) -> u32 {
    return (b[0] as u32 << 8) | b[1] as u32;
}

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.

Flujo de control y patrones

El flujo de control es chico y se ve entero: if/else, while, for, match, break, continue, return y defer. for es el ciclo de tres partes al estilo C, los ciclos pueden llevar etiquetas, y match e if pueden producir valores.

Los patrones cubren lo que hace falta para desarmar datos sin anidar: patrones OR, guards, rangos de enteros, if let, while let y let con desestructuración. Los literales de struct aceptan campos abreviados (field punning) y una actualización con ..base:

enum Shape {
    Circle { r: Int },
    Rect { w: Int, h: Int },
}

fn area(s: Shape) -> Int {
    let a: Int = match s {
        Shape::Circle { r } => 3 * r * r,
        Shape::Rect { w, h } if w == h => w * w,
        Shape::Rect { w, h } => w * h,
    };
    return a;
}

fn bucket(n: Int) -> Int {
    let b: Int = match n {
        0..=9 => 0,
        10 | 20 | 30 => 1,
        _ => 2,
    };
    return b;
}

fn or_zero(o: Option<Int>) -> Int {
    if let Option::Some { value } = o { return value; }
    return 0;
}

fn first_negative(xs: [Int; 8]) -> Int {
    let mut found: Int = -1;
    'scan: for (let mut i: Int = 0; i < 8; i = i + 1) {
        if xs[i] < 0 {
            found = i;
            break 'scan;
        }
    }
    return found;
}

struct Copy Point { x: Int, y: Int }

fn move_x(p: Point, x: Int) -> Point {
    return Point { x, ..p };
}

Los patrones no se anidan y no hay tuplas. Las dos cosas son a propósito: un patrón plano es fácil de leer y fácil de convertir en términos de prueba.

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: Handle = acquire();
defer destroy(f);

Acá Handle implementa el trait Destroy, que es lo que hace que destroy(f) sea la forma de consumirlo.

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:

// signatures only
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, Time, 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.

Podés ponerle nombre a un grupo de capabilities con cap, y una función genérica puede ser polimórfica sobre capabilities con <cap C>. Así es como el código de orden superior se mantiene honesto: el tipo del puntero a función dice qué necesita la función llamada, y el que llama lo hereda.

cap Logging = Console + Alloc;

fn log_line(n: Int) with(Logging) {
    println(n);
}

fn apply<cap C>(f: fn(Int) with(C) -> Int, x: Int) with(C) -> Int {
    return f(x);
}

apply(double, 4) con un double puro sigue siendo puro. apply(shout, 4) con un shout que necesita Console también necesita Console, y un llamador que no lo declara recibe un error de compilació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). Hoy eso es el malloc de libc; pasar un allocator de forma explícita está planificado.

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
qué funciones pueden hacer asignación de memoria es parte de la estructura del programa

La asignación en el stack no requiere Alloc.

Aritmética

La aritmética entera está chequeada. El overflow en +, - y *, la división o el resto por cero, un desplazamiento (shift) por el ancho en bits o más, y negar el valor mínimo terminan en un trap en tiempo de ejecución, en cualquier build. Indexar un array fuera de rango termina en un trap igual, y un índice que está fuera de rango como constante es un error de compilación.

Si querés aritmética modular o saturada, lo decís con una operación con nombre. #[overflow_checked] pide otra cosa: no cambia lo que hace el código, hace que el compilador genere una obligación de no overflow para cada operación, así podés probar que el trap nunca se dispara.

fn mix(a: u32, b: u32) -> u32 {
    return wrapping_add(a, b) ^ (a >> 3);
}

fn brighten(pixel: u8, boost: u8) -> u8 {
    return saturating_add(pixel, boost);
}

#[overflow_checked]
fn add_capacity(len: i32, extra: i32) -> i32 {
    return len + extra;
}

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>, y un error se propaga haciendo match y devolviendo vos mismo la rama Err. No hay ?:

fn read_config(path: &String, mode: &String) with(File, Alloc) -> Result<Config, FsError> {
    let f: File = match File::open(path, mode) {
        Result::Ok { value } => value,
        Result::Err { error } => { return Result::<Config, FsError>::Err { error: error }; },
    };
    defer close_file(f);
    return parse(&f);
}

close_file y parse son funciones comunes definidas en otro lado.

No hay excepciones ni caminos de unwinding ocultos.

defer se ejecuta en cada salida del alcance, incluyendo los returns tempranos.

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.

El vocabulario completo es más amplio que esa lista. Además de proved_by_lean y proved_by_kernel_decision, un reporte puede decir solver_trusted (la cerró un solver SMT externo, que ahora queda en la base trusted; se activa a propósito con --smt), tested_by_oracle, runtime_checked, enforced, assumed, trusted, partial, stale, vacuous (la afirmación vale solo porque su premisa es imposible), counterexample o unproven.

Las postcondiciones llaman result al valor de retorno y pueden referirse a una spec fn, una especificación sin cuerpo y sin código generado. Dentro de una función, assert(e); crea una obligación, assume(e); es una trampa que marca a la función como asumida en la auditoría, y ghost let liga un valor que existe solo para las pruebas y se borra antes de la generación de código:

spec fn rotr_spec(x: u32, n: u32) -> u32;

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

fn byte_at(a: [u8; 16], i: i32) -> u8 {
    assume(0 <= i);
    assert(i < 16);
    ghost let last: i32 = 15;
    return a[i];
}

fn count_to_ten() -> i32 {
    let mut acc: i32 = 0;
    #[invariant(0 <= i && i <= 10)]
    #[variant(10 - i)]
    for (let mut i: i32 = 0; i < 10; i = i + 1) {
        acc = acc + 1;
    }
    return acc;
}

Las pruebas también se vinculan en el código fuente. #[proof_by(...)] y #[ensures_proof(...)] nombran los teoremas de Lean, y #[proof_fingerprint("...")] registra el cuerpo contra el que se escribieron, así que si editás el cuerpo la prueba pasa a stale.

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.{ File, 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:

#[repr(C)]
struct Timespec { sec: i64, nsec: i64 }

extern fn malloc(size: u64) with(Alloc) -> *mut u8;
extern fn clock_gettime(clock: i32, out: *mut Timespec) with(Time) -> i32;

#[repr(C)] le da a un struct el layout de C. #[repr(packed)] y #[repr(align(N))] controlan el relleno (padding) y la alineación. Todo extern fn declara los efectos que ejerce el código foráneo, con with() si no tiene ninguno, y el compilador rechaza uno que no los declare. Llamar a un extern fn común requiere with(Unsafe) en el que llama, salvo que el que llama sea trusted.

Proyectos, tests y consultas

Un proyecto es un manifiesto Concrete.toml y un directorio src/. concrete build, concrete run y concrete test trabajan sobre él, y concrete fmt formatea un archivo. Las funciones de test se marcan con #[test] y devuelven 0 si pasan:

#[test]
fn test_bucket() -> i32 {
    if bucket(3) != 0 { return 1; }
    if bucket(20) != 1 { return 1; }
    return 0;
}

Cada hecho que conoce el compilador se puede leer como reporte (--report caps, authority, effects, contracts, vcs, audit, proof-status y más) o pedir como consulta en JSON:

concrete main.con --query why-capability:greet:Console
concrete main.con --query predictable:main

La primera responde con el camino de llamadas que explica por qué greet necesita Console. La segunda lista cada control del perfil predictable que main no pasa, con su ubicación en el código fuente.

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 (los punteros a función no llevan estado capturado)
trait objects
sobrecarga de operadores
reflection y eval
estado global implícito
shadowing de variables (decidido; hoy el compilador solo rechaza tapar un valor lineal que sigue vivo)
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. Las obligaciones de seguridad en tiempo de ejecución se cierran casi todas solas con procedimientos de decisión, pero las afirmaciones sobre valores todavía necesitan pruebas de Lean escritas a mano, y muchas todavía faltan
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.