Filosofía de la ingeniería: Leslie Lamport, piensa antes de programar

Ideas Clave

• Piensa antes de programar, y deja el pensamiento por escrito. Una especificación es el equivalente en software al plano de un arquitecto: “no pensar garantiza que” cometeremos errores.
• El tiempo no es global; la causalidad es lo real. Sin un reloj compartido en el que se pueda confiar, dejas de preguntar cuándo ocurrió un evento y empiezas a preguntar qué causó qué.
• La relación «ocurrió-antes» y los relojes lógicos formalizan la causalidad. El orden parcial de Lamport – y el contador por proceso que lo implementa – es la semilla de los relojes vectoriales y de la resolución moderna de conflictos.
• Define la corrección con precisión y luego demuéstrala. La seguridad y la vivacidad, el consenso Paxos, la tolerancia a fallos bizantinos y el lenguaje de especificación TLA+ surgen todos de tratar la computación distribuida como matemática, no como folclore.

El Principio

“Un sistema distribuido es aquel en el que el fallo de una computadora cuya existencia ni siquiera conocías puede dejar inutilizable tu propia computadora.” – Leslie Lamport¹

Envió esa frase a un tablón de anuncios de su laboratorio en 1987, y es la oración más citada de la computación distribuida porque nombra aquello que la intuición se niega a creer.¹ Crees que estás ejecutando un programa en tu computadora. No es así. Lo estás ejecutando a lo largo de una población de máquinas cuya existencia no has enumerado, cuyos relojes discrepan, y cualquiera de las cuales puede fallar en el instante exacto que importa. El sistema que puedes sostener en tu cabeza y el sistema que realmente se ejecuta son sistemas distintos, y en la brecha entre ambos vive cada error de los sistemas distribuidos.

La obra de toda la vida de Lamport es la negativa a tapar esa brecha con optimismo. Su convicción es que los sistemas concurrentes y distribuidos son demasiado sutiles para razonarlos por intuición, así que los razonas con matemáticas, sobre el papel, antes de escribir una sola línea de código. “Pensar no garantiza que no cometamos errores”, le dijo a Wired en 2013. “Pero no pensar garantiza que los cometeremos.”² El pensamiento tiene que quedar por escrito, porque la escritura es donde el pensamiento descuidado queda al descubierto: “Para pensar, tienes que escribir. Si piensas sin escribir, solo crees que estás pensando.”³ Los arquitectos dibujan un plano antes de colocar un ladrillo; el equivalente en software es una especificación, y Lamport dedicó la segunda mitad de su carrera a argumentar que la razón por la que nuestros sistemas se rompen es que nos la saltamos.⁴

El paso más profundo tiene que ver con el tiempo mismo. En el mundo físico no existe un reloj global en el que puedas confiar para ordenar eventos entre máquinas, así que debes dejar de preguntar cuándo ocurrió algo y empezar a preguntar qué causó qué. La causalidad, no el reloj de pared, es la verdadera estructura de una computación distribuida.⁵ Casi todo lo que Lamport construyó se deriva de tomar ese único hecho en serio, y es la misma convicción que subyace bajo la puerta de evidencia: no tienes derecho a asumir el orden que desearías que fuera cierto; tienes que establecerlo.

Contexto

Leslie Lamport nació el 7 de febrero de 1941 en la ciudad de Nueva York.⁶ Obtuvo una licenciatura en matemáticas en el MIT en 1960, después una maestría y – en 1972 – un doctorado en matemáticas en Brandeis, con una tesis sobre singularidades en ecuaciones diferenciales parciales.⁶ No se formó como científico de la computación. Se formó como matemático, y nunca dejó de comportarse como tal. El rasgo que define su carrera es que llevó los estándares de las matemáticas – definiciones precisas, supuestos explícitos, demostraciones en lugar de pruebas – a un campo que en su mayoría programaba a tientas.

El trabajo se repartió a lo largo de cuatro instituciones. En Massachusetts Computer Associates, en los años setenta, hizo la reflexión fundacional sobre el ordenamiento de eventos. En SRI International (1977-1985) produjo el trabajo sobre los generales bizantinos. En el Systems Research Center de Digital Equipment Corporation (1985, continuando a través de la adquisición por Compaq hasta 2001) escribió Paxos y comenzó el trabajo de especificación. Desde 2001 hasta su jubilación a principios de 2025 estuvo en Microsoft Research.⁶ A lo largo de todo ello el método fue constante: encontrar un problema de la computación distribuida o concurrente que todos trataban como folclore, definirlo con la precisión suficiente para enunciar un teorema, y luego demostrar el teorema.

El Trabajo

El tiempo, los relojes y la relación «ocurrió-antes»

“Time, Clocks, and the Ordering of Events in a Distributed System” apareció en Communications of the ACM en 1978, y está entre los artículos más citados de toda la ciencia de la computación: ganó el Premio Dijkstra en 2000 al trabajo más influyente de la computación distribuida.⁵⁶ Su idea es engañosamente pequeña. En un sistema distribuido no hay un reloj compartido y fiable, así que no puedes ordenar dos eventos comparando marcas de tiempo. Lo que sí puedes saber es si un evento pudo haber causado otro: el evento A ocurrió-antes que el evento B si A y B están en el mismo proceso con A primero, o si A es el envío de un mensaje y B su recepción. Encadena eso y obtienes la relación «ocurrió-antes»: la causalidad hecha formal.⁵

La consecuencia crucial y contraintuitiva es que «ocurrió-antes» es solo un orden parcial, no total. Dos eventos en procesos distintos sin ninguna cadena de mensajes entre ellos son genuinamente concurrentes: no hay hecho alguno sobre cuál sucedió primero, y cualquier sistema que finja lo contrario está inventando un orden que no existe.⁵ Lamport dio entonces el algoritmo hoy llamado universalmente reloj de Lamport: cada proceso mantiene un contador, lo incrementa en cada evento y marca con él cada mensaje saliente; un receptor adelanta su contador a uno más que el mayor entre su propio valor y la marca de tiempo del mensaje.⁷ Esa regla sencilla produce marcas de tiempo consistentes con la causalidad, y es la semilla de los relojes vectoriales, los vectores de versión y toda la maquinaria de resolución de conflictos de las bases de datos distribuidas modernas.

La razón por la que este artículo importa más allá de su algoritmo es que cambió la pregunta. Antes de Lamport, “¿a qué hora ocurrió esto?” se daba por respondible en un sistema distribuido. Después de Lamport, la respuesta honesta era “pregunta equivocada: pregunta qué lo causó”. Ese replanteamiento es la razón por la que se le atribuye haber convertido la computación distribuida en una ciencia y no en un oficio artesanal.

Paxos, el consenso y las máquinas de estados replicadas

Si no hay un reloj global y las máquinas fallan, ¿cómo logra alguna vez un grupo de computadoras ponerse de acuerdo en algo: qué transacción se confirmó, quién tiene el bloqueo, cuál es la siguiente entrada del registro? Esa pregunta es el problema del consenso, y la respuesta de Lamport es Paxos, el algoritmo en el corazón de casi todo sistema tolerante a fallos construido desde entonces. Lo emparejó con el enfoque de la máquina de estados replicada: si cada réplica parte del mismo estado y aplica la misma secuencia de comandos en el mismo orden, se mantienen idénticas, de modo que todo el problema de mantener consistente un sistema distribuido se reduce a ponerse de acuerdo sobre el orden de los comandos, que es exactamente lo que Paxos proporciona.⁶

La historia de cómo se publicó Paxos es la fábula admonitoria más célebre del campo. Lamport lo redactó como “The Part-Time Parliament”, presentando el algoritmo como el procedimiento legislativo de una ficticia isla griega antigua llamada Paxos, con legisladores que llevaban transliteraciones pseudogriegas de los nombres de sus colegas.⁸ La broma fue una catástrofe. Los revisores pensaron que no hablaba en serio; el artículo fue rechazado por insignificante; quienes asistieron a sus charlas recordaban la puesta en escena al estilo Indiana Jones y no el algoritmo.⁸ Quedó sin publicar durante años. El editor de Communications of the ACM finalmente lo publicó en ACM Transactions on Computer Systems en 1998, todavía envuelto en la parábola.⁸ Cuando el campo siguió ignorándolo, Lamport por fin se rindió y escribió “Paxos Made Simple” en 2001, despojándolo de lo griego para revelar lo que insistía en que era un algoritmo genuinamente sencillo por debajo.⁸ La lección que extrajo no fue “la gente es tonta”. Fue que incluso una idea correcta e importante fracasa si oscureces el razonamiento: la presentación es parte del trabajo, no algo aparte.

El problema de los generales bizantinos

En 1982, junto con Robert Shostak y Marshall Pease, Lamport publicó “The Byzantine Generals Problem”, que dio al campo su lenguaje para el tipo de fallo más difícil.⁶ Un componente que se cae es fácil comparado con uno bizantino: un componente que no se detiene sino que miente, enviando información distinta y contradictoria a distintos pares, ya sea por un error, por corrupción o por malicia. El planteamiento del artículo: las divisiones de un ejército, cada una al mando de un general, deben acordar un único plan – atacar o retirarse – por mensajero, mientras que un subconjunto desconocido de generales son traidores que tratan activamente de impedir el acuerdo. Lamport demostró el umbral exacto de cuántos traidores puede tolerar un sistema y aun así llegar a un acuerdo, convirtiendo “¿y si un nodo miente?” de una vaga inquietud en un teorema con una cota establecida.

Ese teorema es la raíz intelectual de todo sistema que tiene que seguir funcionando mientras algunos de sus participantes son adversarios, y es la razón por la que, décadas después, la palabra bizantino ocupa el centro del consenso en blockchain. Lamport no se propuso habilitar las criptomonedas; se propuso definir, con exactitud, qué significa la tolerancia a fallos cuando “fallo” incluye la traición.

TLA+ y la especificación (y, sí, LaTeX)

El hilo conductor de la carrera de Lamport es la convicción de que debes especificar antes de programar, y TLA+ es esa convicción convertida en herramienta. La Lógica Temporal de Acciones (Temporal Logic of Actions) es un lenguaje para escribir una descripción matemática precisa de lo que se supone que debe hacer un sistema: sus estados, los pasos entre ellos y las propiedades que siempre debe satisfacer (seguridad: nunca ocurre nada malo) y que finalmente debe lograr (vivacidad: algo bueno acaba ocurriendo), dos conceptos que él formalizó.⁶ Escribes la especificación, y un verificador de modelos explora el espacio de estados para encontrar el sutil entrelazado que rompe tu invariante: el error que nunca habrías encontrado con pruebas, porque solo aparece cuando tres máquinas hacen tres cosas en un orden que jamás imaginaste. Su argumento es el del plano del arquitecto: dibujas el edificio antes de verter el hormigón, y una especificación de software es ese mismo plano, escrito en matemáticas porque las matemáticas son el lenguaje más preciso que tenemos.⁴

Y hay un monumento más silencioso. A principios de los años ochenta, basándose en el TeX de Donald Knuth, Lamport escribió LaTeX, el sistema de macros que se convirtió en la forma por defecto en que los científicos y matemáticos componen sus documentos, la razón por la que toda una generación de artículos y tesis tiene el aspecto que tiene.⁶ Es un artefacto característico de Lamport: necesitaba escribir su propio trabajo con precisión, así que construyó la herramienta que permitía a todos hacerlo. El instinto que produjo TLA+ – una notación que obliga a la precisión – es el mismo instinto que produjo LaTeX.

El Método

El método es una sola idea aplicada sin tregua durante cincuenta años: el pensamiento es el trabajo, y el pensamiento debe quedar por escrito antes que el código.

Razona sobre la causalidad, no sobre el tiempo. No hay un reloj global en el que puedas confiar, así que deja de ordenar los eventos por cuándo sucedieron y ordénalos por qué causó qué. La relación «ocurrió-antes», no el reloj de pared, es la verdadera estructura, y aceptar que dos eventos son genuinamente concurrentes es más honesto que inventar un orden.⁵

Especifica antes de programar. Para cualquier cosa sin una solución establecida, detente y piensa primero, y el pensar es independiente del programar. Escribe el plano – la especificación – en matemáticas, porque las matemáticas son simples y precisas allí donde la prosa es vaga.⁴ “No pensar garantiza que” cometeremos errores.²

Escribe para averiguar si estás pensando. La escritura es la prueba de si un pensamiento es real. “Si piensas sin escribir, solo crees que estás pensando.”³ Una especificación que no puedes poner por escrito es una idea que todavía no tienes de verdad.

Define el fallo con exactitud. “¿Y si un nodo miente?” es folclore hasta que lo enuncias como los generales bizantinos y demuestras la cota de tolerancia. Las definiciones precisas convierten las inquietudes en teoremas.⁶

La presentación es parte de la corrección. Paxos fue correcto durante años antes de que nadie pudiera usarlo, porque la parábola griega enterró la idea. Un resultado correcto que nadie puede entender no ha terminado de ser ingeniado.⁸

Cadena de Influencia

Quiénes lo formaron

Las matemáticas mismas. La formación de Lamport fue un doctorado en matemáticas, no en ciencias de la computación, y toda la forma de su contribución es la importación de los estándares matemáticos – definiciones, axiomas, demostraciones – a un campo que había estado programando por intuición.⁶ (Influencia formativa)

Los problemas de tolerancia a fallos de los sistemas reales de los años setenta. El trabajo de SRI en sistemas fiables para aeronaves y el horror práctico de las máquinas que fallan en mitad de un protocolo le dieron problemas concretos – fallos bizantinos, consenso – que exigían el tratamiento formal que estaba hecho para dar.⁶ (Influencia directa)

Edsger Dijkstra. La convicción de que la corrección se establece por demostración y no por pruebas, y de que los programas concurrentes deben razonarse formalmente, es de Dijkstra antes que de Lamport. El premio que Lamport ganó por su artículo sobre los relojes lleva el nombre de Dijkstra. (Influencia directa)

A quiénes formó él

Toda base de datos distribuida, plataforma en la nube y blockchain. Los relojes lógicos sustentan la resolución de conflictos en los almacenes distribuidos; Paxos (y su descendiente Raft) es el núcleo de consenso de Chubby y Spanner de Google, de ZooKeeper, etcd y la capa de coordinación de esencialmente toda nube. El resultado de los generales bizantinos es el piso teórico bajo Bitcoin y todo protocolo de consenso tolerante a fallos desde entonces.

Los métodos formales en la industria. Amazon Web Services usa célebremente TLA+ para especificar y verificar S3, DynamoDB y otros servicios fundamentales antes de lanzarlos, encontrando errores sutiles en el diseño y no en producción. El argumento del plano de Lamport pasó de herejía a práctica.

El vocabulario del campo. «Ocurrió-antes», seguridad y vivacidad, máquinas de estados replicadas, consistencia secuencial, fallo bizantino: estas no son contribuciones de Lamport al lenguaje de los sistemas distribuidos; en gran medida son ese lenguaje.

El hilo conductor

Edsger Dijkstra sostenía que demuestras la corrección de un programa antes de ejecutarlo – que las pruebas muestran la presencia de errores, nunca su ausencia – y Lamport es el heredero directo, llevando la demostración-antes-de-ejecutar de los programas secuenciales al mundo mucho más difícil de la concurrencia, donde el error que no puedes someter a prueba es la regla y no la excepción. Barbara Liskov convirtió el razonamiento formal sobre el comportamiento de los programas en una primitiva de trabajo con la abstracción de datos y la sustituibilidad; Lamport convirtió el razonamiento formal sobre el comportamiento del sistema a lo largo del tiempo en el estándar, especificando no lo que garantiza un objeto sino lo que un sistema concurrente entero debe hacer siempre y, finalmente, hacer. Y Donald Knuth llevó el rigor matemático al análisis de algoritmos y, casi como un apunte al margen, construyó TeX para que ese trabajo pudiera plasmarse con precisión, una rima casi exacta con Lamport, que construyó LaTeX sobre él por la misma razón e hizo de la especificación misma un acto matemático. Tres matemáticos que se negaron a dejar que “parece que funciona” contara como saber. (Puente de la serie)

Lo Que Me Llevo de Esto

La lección que conservo es que el pensamiento es el trabajo, y el pensamiento no es real hasta que queda por escrito. El argumento del plano de Lamport es incómodo porque es correcto: la razón por la que un sistema se rompe en producción casi nunca es que el código se escribiera mal, es que nadie especificó qué se suponía que debía hacer realmente el sistema bajo concurrencia y fallos, así que no había un enunciado contra el cual contrastar el código. La disciplina consiste en escribir la especificación antes que la implementación, en un lenguaje lo bastante preciso como para que sus contradicciones se vuelvan visibles. Ese es el mismo estándar que la calidad como única variable: la pregunta nunca es “¿pasa esto el camino feliz?”, sino “¿he enunciado, con exactitud, qué debe ser siempre cierto, y demostrado que el diseño lo honra?”. Es la razón por la que me apoyo tanto en escribir el PRD antes que el código; un PRD es una especificación de Lamport con ropa de trabajo.

En el mundo en el que construyo ahora – agentes, bucles de herramientas, sistemas multiagente – la lección de Lamport es la que casi todo el mundo se salta, y paga por ello. Un sistema de agentes es un sistema distribuido: procesos independientes, sin reloj global, mensajes que llegan desordenados o que no llegan, y componentes que fallan en silencio o, peor, mienten. Los errores nunca están en las instrucciones que le das al modelo; están en el ordenamiento: dos agentes actuando sobre un estado obsoleto, una llamada a herramienta cuyo resultado llega después de la decisión que lo necesitaba, un par de eventos “concurrentes” que el orquestador fingió ordenar. La disciplina de Lamport es dejar de confiar en la intuición del reloj de pared, razonar explícitamente sobre la causalidad y el fallo, y escribir qué debe ser siempre cierto antes de conectar nada. La convicción de que especificas antes de construir, de que razonas sobre un sistema en lugar de hurgar en él, ese es el hilo conductor desde un artículo de 1978 sobre relojes hasta una infraestructura de agentes de 2026, y es exactamente por lo que trato el rendimiento y la corrección de un sistema como una propiedad que diseñas desde dentro, nunca una que esperas depurar más tarde.

Preguntas Frecuentes

¿Cuál es la filosofía de ingeniería de Leslie Lamport?

La convicción de Lamport es que los sistemas concurrentes y distribuidos son demasiado sutiles para razonarlos por intuición, así que debes pensar con matemáticas, sobre el papel, antes de escribir código, igual que un arquitecto dibuja un plano antes de colocar un ladrillo. El plano del software es una especificación, escrita en matemáticas porque las matemáticas son el lenguaje más preciso disponible.⁴ Por debajo de eso hay una postura ante el tiempo: en un sistema distribuido no hay un reloj global en el que confiar, así que la verdadera estructura de una computación es la causalidad – qué causó qué – no cuándo ocurrieron las cosas.⁵ “Pensar no garantiza que no cometamos errores”, dijo, “pero no pensar garantiza que los cometeremos.”²

¿Qué es un reloj de Lamport y la relación «ocurrió-antes»?

La relación «ocurrió-antes» es la formalización de Lamport de la causalidad en un sistema distribuido: el evento A ocurrió-antes que el evento B si están en el mismo proceso con A primero, o si A envía un mensaje y B lo recibe, o por encadenamiento de esos casos.⁵ Es solo un orden parcial: dos eventos en procesos distintos sin ningún mensaje que los conecte son genuinamente concurrentes, y ningún sistema correcto puede afirmar que uno sucedió primero.⁵ Un reloj de Lamport implementa esto con un contador por proceso: lo incrementas en cada evento, marcas con él cada mensaje saliente, y al recibirlo adelantas tu contador a uno más que el mayor entre tu propio valor y la marca de tiempo del mensaje.⁷ El resultado es un conjunto de marcas de tiempo consistentes con la causalidad, el fundamento de los relojes vectoriales y de la resolución moderna de conflictos en sistemas distribuidos.

¿Qué son Paxos y el problema de los generales bizantinos?

Paxos es el algoritmo de Lamport para el consenso – lograr que un grupo de máquinas poco fiables y posiblemente con fallos se pongan de acuerdo sobre un único valor, como el siguiente comando en un registro replicado – y sustenta la capa de coordinación de casi todos los sistemas distribuidos modernos. Célebremente, lo publicó primero como una parábola sobre un ficticio parlamento griego (“The Part-Time Parliament”, ACM TOCS 1998); la broma oscureció tanto la idea que con el tiempo la reescribió como “Paxos Made Simple” en 2001.⁸ El problema de los generales bizantinos (Lamport, Shostak y Pease, 1982) define el modo de fallo más difícil – componentes que no se limitan a caerse sino que mienten, enviando información contradictoria – como generales que tratan de acordar un plan mientras los traidores entre ellos sabotean el acuerdo, y demuestra cuántos traidores puede tolerar un sistema.⁶ Es la raíz teórica del consenso en blockchain.

¿Por qué ganó Leslie Lamport el Premio Turing?

La ACM concedió a Lamport el Premio Turing A.M. 2013 “por sus contribuciones fundamentales a la teoría y la práctica de los sistemas distribuidos y concurrentes, en particular la invención de conceptos como la causalidad y los relojes lógicos, la seguridad y la vivacidad, las máquinas de estados replicadas y la consistencia secuencial.”⁶ La mención capta la amplitud de su obra: convirtió la computación distribuida de folclore en una ciencia con definiciones y demostraciones precisas, dio al campo gran parte de su vocabulario, creó el lenguaje de especificación TLA+ para hacer de “especificar antes de programar” una disciplina práctica y – basándose en el TeX de Knuth – escribió LaTeX, el sistema de composición tipográfica que se volvió estándar en toda la ciencia y las matemáticas.⁶

Fuentes