El debate sobre efectos en Rust y el argumento de Concrete a favor de un lenguaje más chico

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

Nota de la serie: esta es la entrada principal de comparación con Rust en la serie sobre Concrete. Si recién llegás, empezá por Por qué existe Concrete. Si querés la referencia del lenguaje, usá la Especificación de Concrete.

Yosh Wuyts escribió hace poco sobre su “gran visión” para Rust, donde plantea tres direcciones que cree que el lenguaje debería seguir: efectos, tipos subestructurales más fuertes y tipos refinados (refinement types). El hilo de Hacker News que vino después se dividió de manera previsible: un bando vio tomar forma un lenguaje de sistemas más seguro y con más principios, mientras el otro vio ecos de Scala, de C++ y de un lenguaje que se vuelve más difícil de leer que el software que pretende aclarar.

Los dos bandos están viendo algo real, y creo que resolver la tensión entre ellos requiere algo distinto de agregarle más features a Rust. Ahí es donde entra Concrete.

#El diagnóstico es correcto

Olvidate de la sintaxis específica de Rust que propone Wuyts. La parte más fuerte de su post es el problema que identifica.

Rust ya tiene una colección creciente de “colores de funciones”: async, const, la posibilidad de fallar, los generators y muchas otras propiedades que el software de bajo nivel quiere rastrear. Cuantas más se acumulan, más se siente el lenguaje como una colección de casos especiales y no como un único modelo de lo que las funciones pueden y no pueden hacer.

El código de sistemas necesita expresar cosas como:

• esta función no puede hacer I/O
• esta función no puede desenrollar la pila
• esta función no puede asignar memoria
• esta función no puede llamar al host
• esta función es determinística

Estas cosas importan en la práctica. Código embebido, kernels, runtimes, infraestructura crítica, verificación formal y cualquier base de código donde las auditorías son parte del laburo.

Wuyts tiene razón en todo esto. Donde no estoy de acuerdo es con la solución. Esto no se arregla agregándoles más “colores” a las funciones dentro de Rust. Se arregla diseñando un lenguaje donde los efectos están incorporados desde el principio.

Para hacerlo más concreto, imaginate una función de bajo nivel que parsea una entrada, asigna un buffer y escribe en un archivo. En Rust, las propiedades relevantes terminan repartidas entre distintos mecanismos: async si cede el control, Result si falla, el comportamiento del allocator en la implementación, los permisos de I/O por convención y no en el tipo, y posiblemente más marcadores más adelante si el lenguaje crece en esa dirección. En Concrete, la misma pregunta se responde en un solo lugar: esta función es pura salvo que se declare lo contrario, y si asigna memoria y escribe un archivo su firma dice with(Alloc, File). La sintaxis exacta no importa acá. Lo que importa es que el seguimiento de efectos es un único modelo, no una pila de casos especiales.

El lenguaje se vuelve más simple cuando el modelo de efectos es consistente desde el principio.

#La objeción de la complejidad también es correcta

Los escépticos de Hacker News también tienen razón en que los lenguajes no se vuelven complejos solo porque tengan ideas poderosas, sino porque esas ideas se acumulan y las interacciones entre ellas se multiplican de maneras que nadie planeó.

Los efectos interactúan con async. Async interactúa con los traits. Los traits interactúan con los generics. Los generics interactúan con la inferencia. La inferencia interactúa con las macros. Las macros interactúan con los diagnósticos. Cada feature tiene sentido por separado, pero juntas pueden hacer que un lenguaje sea agotador de leer.

El comentario que me quedó grabado no fue “no quiero seguridad”. Fue algo más parecido a: quiero leer lógica de negocio sin sentir que cada línea es una obligación de prueba. Esta objeción va más directo a las concesiones (trade-offs) del lenguaje, porque un lenguaje puede volverse “más seguro” en un sentido técnico mientras se vuelve más difícil de entender en la práctica.

Tomo esta preocupación como una restricción de diseño para Concrete. Si una feature hace más grande al lenguaje sin hacer más fácil de leer el código común, no debería salir. Por eso Concrete les dice que no a cosas que los lenguajes mainstream mantienen por conveniencia:

• nada de flujo de control oculto
• nada de destrucción implícita
• nada de asignación de memoria (allocation) oculta
• nada de excepciones
• nada de closures con capturas ocultas
• nada de trait objects
• nada de sobrecarga de operadores
• nada de efectos definidos por el usuario
• nada de un sistema general de atributos

Hay un patrón común detrás de esa lista: cada ítem o le esconde trabajo al lector, o crea más de una forma de expresar el mismo comportamiento, o obliga al compilador y a las herramientas a razonar sobre más interacciones implícitas. Concrete elimina esas presiones en la frontera del lenguaje en lugar de administrarlas después. Este minimalismo es el pago de una apuesta: que las garantías más fuertes y la legibilidad pueden convivir, pero solo si el lenguaje se mantiene chico.

#Efectos y ownership: sí

Concrete coincide con Wuyts en dos de los tres ejes.

Nadie discute que los efectos pertenecen a un lenguaje de sistemas. La pregunta real es si diseñás un modelo para todos ellos de entrada o si los dejás acumularse como casos especiales. Rust en algún momento va a necesitar una solución real acá si sigue moviéndose en esta dirección, y este tipo de cosas es mucho más fácil de hacer bien en un lenguaje nuevo que en uno con una base instalada grande y un ecosistema de bibliotecas grande. Lo que importa es un único modelo de efectos que los maneje a todos.

En cuanto al ownership, Rust es afín: los valores se pueden usar como mucho una vez. Eso evita el use-after-free en código seguro, pero todavía te permite olvidarte de los valores por completo. Concrete va más lejos. Los valores con dueño son lineales por defecto, lo que significa que se tienen que usar exactamente una vez. Si querés evitar fugas de recursos en tiempo de compilación en lugar de esperar lo mejor en tiempo de ejecución, “como mucho una vez” no alcanza. En Concrete, el compilador no hace drop de los recursos por vos en silencio. La limpieza (cleanup) es explícita con destroy y defer, y si un valor lineal no se consume, el programa no compila. Esto es más estricto que Rust, y más cercano en espíritu a Austral. También cuesta más. Los programadores tienen que escribir los caminos de limpieza de forma más explícita, las APIs tienen menos margen para tapar decisiones de ownership y algunos patrones comunes se vuelven más ceremoniosos. Creo que es un precio aceptable, pero es un precio real.

#Tipos refinados: no

El desacuerdo principal son los tipos refinados, y acá me pongo del lado de los escépticos.

Los tipos refinados son poderosos. Los pattern types y los view types son ingeniosos. Pueden eliminar chequeos en tiempo de ejecución, expresar conocimiento parcial y hacer legales más borrows. Todo cierto. Pero empujan al lenguaje desde “el compilador verifica reglas de recursos y efectos” hacia “el compilador espera que los programadores codifiquen hechos sobre sus programas en los tipos”. Ese es un tipo de lenguaje muy distinto del que Concrete intenta ser.

Para ser preciso, quiero decir que Concrete no debería poner esta maquinaria en el lenguaje núcleo. Eso es distinto de decir que las técnicas de refinamiento son inútiles. Pueden seguir teniendo su lugar en herramientas de prueba externas, en bibliotecas orientadas a verificación o en obligaciones generadas que están por encima del lenguaje propiamente dicho. Pero no pertenecen al centro de un lenguaje cuyo trabajo principal es mantenerse chico, explícito y revisable.

Hay tres razones por las que Concrete no los pone en el lenguaje núcleo.

Primero, los tipos refinados aumentan muchísimo lo que el type checker tiene que probar. Cambian la naturaleza de lo que se espera que verifique el compilador, y ese cambio afecta a todo el lenguaje.

Segundo, hacen que el código sea más difícil de leer. Cada restricción metida en una firma de tipos compite por atención con lo que el código realmente hace. Los programadores pueden manejar tipos refinados sin problema. Pero la atención es limitada, y las firmas de tipos deberían ayudarte a entender una función, no convertirse en acertijos por sí mismas.

Tercero, van en contra de uno de los objetivos de Concrete: ser amigable para la generación y la revisión por máquinas. Los sistemas de refinamiento son el lugar donde el código generado, la revisión humana y las herramientas de prueba empiezan a tirar para lados distintos.

Entonces el desglose es:

• efectos explícitos: sí
• ownership más fuerte: sí
• tipos refinados en el lenguaje núcleo: no

Los tipos refinados son útiles en el contexto adecuado. También son caros, y no creo que ese costo pertenezca al núcleo de un lenguaje construido alrededor de la idea de que la legibilidad y el razonamiento formal deberían ayudarse en lugar de competir.

#Más chico, no más inteligente

Si leés el post de Wuyts y pensás “esto es Rust volviéndose más académico”, puede parecer que Concrete va todavía más lejos. Está escrito en Lean, habla de kernels, de soundness y de linealidad, y usa lenguaje formal a propósito.

Pero Concrete va en la dirección opuesta: un lenguaje más chico con reglas más estrictas. Esa diferencia importa. Un lenguaje se vuelve difícil de leer cuando su teoría se hace más profunda, cuando hay demasiadas formas de escribir lo mismo, cuando se acumulan comportamientos implícitos y cuando demasiados estilos son todos técnicamente válidos.

Concrete consigue garantías más fuertes quitando opciones en lugar de agregarlas:

• un solo modelo de efectos
• un solo modelo de ownership
• nada de trabajo invisible
• un kernel chico
• una gramática lo bastante simple como para parsearla con un token de lookahead

Si Concrete fracasa, va a fracasar por otras razones. Convertirse en C++ por acumulación de features es justamente el modo de falla que el lenguaje está construido para evitar.

#La línea divisoria

Este debate no es realmente sobre “teoría de tipos contra pragmatismo”. Se reduce a algo más específico: ¿un lenguaje de sistemas debería conseguir garantías más fuertes volviéndose más expresivo, o volviéndose más acotado y más explícito?

Rust intenta seguir siendo expresivo mientras agrega más garantías. Eso tiene sentido para un lenguaje mainstream con un ecosistema grande. Concrete toma el otro camino. Si una garantía necesita más maquinaria oculta, más interacciones entre features o más inferencia, prefiero no tenerla. Si una garantía viene de hacer el lenguaje más explícito, más uniforme y más chico, entonces la quiero.

La programación de sistemas necesita mejores herramientas para rastrear efectos y administrar recursos. Los escépticos tienen razón en que la complejidad del lenguaje también es un riesgo, y en que las features del sistema de tipos se vuelven contraproducentes cuando hacen que el lenguaje sea más difícil de tener en la cabeza. Concrete acepta el primer punto y trata el segundo como una restricción dura.

Si Rust se está preguntando cómo volverse más seguro sin volverse ilegible, mi opinión es que eso se vuelve mucho más fácil cuando el lenguaje está dispuesto a decirles que no a más cosas. Concrete no intenta ganarle a Rust en expresividad. Intenta ganarle en restricción.

#Para seguir mirando

• Rich Hickey, Simple Made Easy (Strange Loop). El argumento canónico de que lo simple, en el sentido de no enredado, le gana a lo fácil, que es todo el argumento a favor de un lenguaje más chico dicho con otro vocabulario.