Entrevista a Leslie Lamport (ACM Turing Award)
Entrevista a Leslie Lamport (ACM Turing Award)
Pionero en el campo de la especificación y verificación de sistemas concurrentes.
Esta entrevista fue originalmente realizada en inglés por email. Por tanto, primero se ofrece una traducción al español, y al final, se encuentra la versión original.
This interview was originally conducted in English by email. The Spanish translation is provided first, followed by the original version.
Leslie Lamport es uno de los padres de los sistemas concurrentes. En su legendario artículo Time, Clocks, and the Ordering of Events in a Distributed System (1978), presentó el concepto de relojes para coordinar eventos que suceden en distintos procesos. Sumado a su brillante capacidad para crear metáforas, que se manifiesta en trabajos como el algoritmo de la Panadería o el algoritmo de Paxos, está a la par de otros grandes nombres que han hecho aportes sobresalientes a los sistemas concurrentes, como Edsger Dijkstra y Tony Hoare. También es artífice de LaTeX, BibTeX y TLA+. Sus esfuerzos se vieron recompensado el año 2013, cuando se le concedió el ACM Turing Award. En la actualidad trabaja como investigador en Microsoft.
Si no conocen a Lamport, les sugiero primero mirar este video.
Lamport posee una personalidad peculiar, donde no esperas que te responda algo políticamente correcto solo porque suene bien. Y esta entrevista es una demostración de su honestidad.
¡Espero la disfruten!1
Versión traducida
Camilo: (1) En tu artículo «If You’re Not Writing a Program, Don’t Use a Programming Language» (2018) mencionaste que codear no es lo mismo que programar. Codear2 tiene que con elegir un lenguaje de programación e implementar programas. En cambio, programar tiene que ver con la corrección de algoritmo, diseñar un algoritmo que satisfaga algunas propiedades bien definidas usando el lenguaje de las matemáticas. ¿Por qué crees que hay esta falta de comprensión en los conceptos, falta de conocimiento matemático, la industria exige producir software demasiado rápido que impide pensar antes de programar?
Leslie: Sospecho que la mayoría de los programadores y las personas que los dirigen no tienen ni idea de que las matemáticas puedan ser útiles para pensar en los programas. (También sospecho que los matemáticos no tienen ni idea de que las matemáticas puedan ser útiles para pensar en los programas.) Por qué los informáticos no lo entienden parece ser complicado y yo no lo entiendo del todo.
Camilo: (2) Un planteamiento interesante fue lo que dijiste en «Why We Should Build Software Like We Build Houses» (2013), donde haces una analogía entre el desarrollo de software y la construcción de casas. Terminaste el artículo con una frase mítica: «Thinking doesn't guarantee that we won't make mistakes. But not thinking guarantees that we will.» («Pensar no garantiza que no cometamos errores. Pero no pensar garantiza que los cometeremos») ¿Crees que algún día se podrá construir software reduciendo sus errores hasta un mínimo? Lo digo porque algunos argumentan que, en sistemas grandes de software, dada su complejidad, hay muchas partes donde es impracticable aplicar una verificación formal total; así, muchos proyectos de software se terminan optando por metodologías de pruebas-error-corrección.
Leslie: No tengo una solución mágica para eliminar todos los errores. Sólo tengo un método para detectar errores de diseño de alto nivel en una clase importante de aplicaciones. Tiene la ventaja adicional de mejorar la calidad del diseño.
Camilo: (3) En muchas entrevistas has mencionado la importancia de aprender a escribir bien (lenguaje natural) porque eso te transforma en un mejor pensador. Esto se puede conectar con lo anterior: la importancia de pensar antes de actuar. En un mundo que avanza cada vez más rápido, y con herramientas de IA que generan texto (ChatGPT) y código automático (GitHub Copilot, por ejemplo) para acelerar la creación de software, ¿cómo los programadores del 2023 podrían aspirar a pensar mejor?
Leslie: No se puede construir nada que funcione sin pensar. He hablado mucho de cómo las matemáticas mejoran tu pensamiento.3 En un mundo que se mueve rápido, tienes que darte cuenta de que no dedicar suficiente tiempo a pensar no te va a ahorrar tiempo.
Camilo: (4) Leslie, tú tienes una formación matemática, y en una entrevista dijiste que el conocimiento de la teoría de la relatividad de Einstein te dio pistas en el diseño de algoritmos distribuidos, en particular, en el tema de la coordinación de eventos.4 Además de tus artículos donde planteas una solución mediante metáfora (pienso en Paxos). ¿Cuál es la importancia de la creatividad y del valor para romper el statu quo (esto último lo digo porque sé que sufriste cierto rechazo e incomprensión al presentar ciertos trabajos)?
Leslie: Nunca he sentido que hiciera falta valor para hacer lo que hice. Aparentemente requiere creatividad. No he tenido mucha experiencia con el rechazo. A veces me han ignorado, y a veces la persistencia ayuda.
Camilo: (5) ¿Podría explicar el estado actual y la importancia de TLA+ a los programadores que no están familiarizados con los lenguajes de especificación formal?
Leslie: El lenguaje y la teoría subyacente son esencialmente completos. Existen herramientas útiles, pero fueron creadas por un pequeño número de personas y no están pulidas. Si está diseñando un sistema grande, probablemente tenga que tratar con concurrencia y los aspectos del diseño que implican concurrencia deben especificarse con precisión y comprobarse si quiere que funcionen. Si estás escribiendo un programa que implica sincronización multiproceso, si no implementa un algoritmo que ha sido especificado con precisión y comprobado de alguna manera, entonces tu programa probablemente tendrá errores. TLA+ y sus herramientas son una forma de realizar la especificación y comprobación necesarias.
Camilo: (6) Con la llegada de sistemas de generan distintos recursos de manera automática a través de la IA ¿Cómo ves el futuro de la verificación formal y de la ciencia de la computación? ¿Seguirán sufriendo los informáticos por su debilidad en matemáticas o serán estas suplidas por asistentes «inteligentes»?
Leslie: No soy mejor que nadie para predecir el futuro. Sólo espero que se utilice para ayudar a la gente a escribir y comprobar descripciones matemáticas de lo que están haciendo, en lugar de permitirles dar descripciones difusas de lo que quieren hacer y producir programas que nadie puede entender.
Camilo: (7) Por último, ¿qué consejo darías a las personas que quieren ser informáticos, independientemente de su edad?
Leslie: No soy orientador y no puedo predecir el futuro, así que no soy competente para darles consejos.
Camilo: ¡Muchas gracias, Leslie, por tomarte el tiempo!
Original
Camilo: (1) In your article "If You're Not Writing a Program, Don't Use a Programming Language," (2018) you discussed the difference between coding and programming. While coding involves choosing a programming language and implementing a program, programming is also about ensuring correctness and designing an algorithm that meets specific criteria using the language of mathematics. Do you think computer scientists lack an understanding of concepts due to insufficient mathematical knowledge? Or is it because the industry demands software to be produced too quickly, preventing proper thinking before programming?
Leslie: I suspect that most programmers and the people who manage them have no idea that math might be of any use in thinking about programs. (I also suspect that mathematicians have no idea that math might be of any use in thinking about programs.) Why computer scientists don’t understand it seems to be complicated and I don’t completely understand it.
Camilo: (2) An interesting approach was what you said in "Why We Should Build Software Like We Build Houses" (2013), where you make an analogy between software development and building houses. You ended the article with a mythical sentence: "Thinking doesn't guarantee that we won't make mistakes. But not thinking guarantees that we will." Would it be possible to build software by reducing its errors to a minimum? I say this because some argue that in large software systems, given their complexity, there are many parts where applying a total formal verification is impracticable. After all, there are many layers with multiple technologies. Thus, many software projects end up being obtained by test-error-correction methodologies.
Leslie: I have no magic bullet to eliminate all errors. I just have a method for catching high-level design errors in an important class of applications. It has the extra advantage of improving the quality of the design.
Camilo: (3) In interviews, you stressed the importance of good writing (in natural language) as it improves thinking. It's connected to thinking before acting. In a world that moves fast and with AI tools that speed up software creation, how can programmers in 2023 improve their thinking?
Leslie: You can’t build anything that works without thinking. I’ve said a lot about how math improves your thinking. In a world that moves fast, you have to realize that not spending enough time thinking is not going to save you time.
Camilo: (4) Leslie, I understand your mathematical background and knowledge of Einstein's special relativity helped create the intuition necessary for you to design distributed algorithms, particularly regarding event coordination (using clocks). Additionally, you've proposed solutions using metaphors (such as Paxos). How important is creativity and courage in breaking the statu quo, given your experiences with rejection and misunderstanding?
Leslie: I have never felt that it took any courage to do what I did. It apparently requires creativity. I haven’t had much experience with rejection. I have sometimes been ignored, and sometimes persistence helps.
Camilo: (5) Could you explain the current status and importance of TLA+ to programmers unfamiliar with formal specification languages?
Leslie: The language and underlying theory are essentially complete. There are useful tools, but they were built by a small number of people and are not polished. If you’re designing a large system, it probably has to deal with concurrency and the aspects of the design that involve concurrency need to be specified precisely and checked if you want them to work. If you’re writing a program that involves multiprocess synchronization, if it doesn’t implement an algorithm that has been specified precisely and checked in some way, then your program will probably have bugs. TLA+ and its tools are a way to do the necessary specification and checking.
Camilo: (6) With the advent of systems that generate different resources automatically through AI, how do you see the future of formal verification and computer science? Will computer scientists continue to suffer from their weakness in mathematics, or will these weaknesses be replaced by "intelligent" assistants?
Leslie: I’m no better than anyone at predicting the future. I can just hope that it’s used to help people write and check mathematical descriptions of what they’re doing, rather than allowing them to give fuzzy descriptions of what they want to do and producing programs that nobody can understand.
Camilo: (7) Finally, what advice would you give to people who want to become computer scientists, regardless of their age? I wonder if they are making an error?
Leslie: I’m not a guidance counselor and can’t predict the future, so I am not competent to give them advice.
Camilo: Thank you very much, Leslie, for taking the time!
Para más información de Leslie Lamport y otros ganadores del premio ACM Turing, podría considerar adquirir mi libro: Mentes geniales. La vida y obra de 12 grandes informáticos. Disponible en Amazon.
También he dedicado un episodio del pódcast al trabajo de Lamport:
https://algoritmo.buzzsprout.com/758831/7223620
Personalmente no es la primera vez que me comunico con él, y en cada ocasión ha respondido a mis preguntas, por lo cual estoy agradecido.
La traducción al español fue realizada usando DeepL, añadiendo pequeños cambios. Las negritas, los enlaces y las notas a pie de páginas fueron añadidos por mí.
Lamport usa la palabra «coding» en vez de «programming» para hacer referencia a la actividad de escribir código sin pensar en el problema. Dado que no existe una distinción clara en español para ambas palabras usé «codear». También podría ser «codificar» dependiendo del contexto.
Su artículo “Time, Clocks, and the Ordering of Events in a Distributed System” del 1978 es uno de los más citados en la historia de la computación.