- Para convertirte en un mejor programador, es importante desarrollar el hábito de imaginar pequeñas pruebas mentalmente al escribir código
- Monotonicidad, inmutabilidad, precondiciones y postcondiciones, e invariantes son conceptos clave al hacer estas mini pruebas
- Diseñar considerando el alcance del impacto que un cambio de código tiene en todo el sistema (aislamiento, firewall) ayuda mucho a reducir la complejidad y el riesgo
- La inducción permite demostrar paso a paso la corrección de funciones o estructuras recursivas
- Este tipo de pensamiento se desarrolla con práctica y repetición, y ayuda mucho entrenarse con pruebas matemáticas reales y resolución de problemas de algoritmos
Introducción e idea central
- El autor fue desarrollando de forma natural, a medida que ganó experiencia, el hábito de “dibujar pequeñas pruebas” para mejorar la precisión y la velocidad de su código
- El proceso de verificar y razonar mentalmente el comportamiento esperado mientras se programa requiere práctica, y cuando se domina, la calidad del código mejora de forma notable
- Lo importante no es exactamente cómo hacerlo, sino practicarlo de distintas maneras hasta encontrar la que mejor funcione para cada persona
Monotonicidad (Monotonicity)
- La monotonicidad se refiere a la propiedad de una función o de un código de avanzar en una sola dirección
- Un ejemplo es el checkpointing, donde las etapas del trabajo solo avanzan hacia adelante y no se vuelve atrás para reejecutar trabajo que ya terminó
- En el ejemplo de árboles LSM frente a árboles B, los árboles LSM tienen la característica de que el espacio en su mayor parte se acumula, y solo disminuye durante el proceso de compactación
- Cuando la monotonicidad está garantizada, se pueden descartar o predecir de manera natural ciertos estados complejos o algunos resultados posibles
- La inmutabilidad (immutability) es un concepto similar: como un valor nunca cambia una vez establecido, se puede excluir la posibilidad de cambios de estado
Precondiciones y postcondiciones (Pre- and post-conditions)
- Las precondiciones (pre-condition) y postcondiciones (post-condition) son afirmaciones que deben ser verdaderas antes y después de ejecutar una función
- Seguir estas condiciones de forma explícita al escribir una función ayuda al razonamiento lógico y a las pruebas
- Cuando las postcondiciones están claramente definidas, es más fácil derivar casos de prueba unitarios
- Agregar assertions al código para verificar estas condiciones y detener la ejecución de forma temprana ante situaciones inesperadas mejora la previsibilidad y la seguridad
- A veces ni siquiera es fácil asignar precondiciones o postcondiciones claras a una función, y descubrir eso por sí mismo también aporta información valiosa
Invariantes (Invariants)
- Un invariante es una propiedad que debe ser siempre verdadera en cualquier situación: antes, durante y después de la ejecución
- Un ejemplo representativo es la ecuación contable de la contabilidad por partida doble (total de créditos = total de débitos)
- Si se divide todo el código en pasos pequeños y se demuestra que cada paso preserva el invariante, se puede garantizar la integridad del conjunto
- Existen formas de mantener invariantes usando listeners o métodos del ciclo de vida (como constructores/destructores en C++ o
useEffect en React)
- Cuando hay pocos cambios o los caminos son simples, verificar invariantes es mucho más fácil
Aislamiento (Isolation)
- Uno de los núcleos del buen software es agregar o modificar funcionalidades sin volver inestable al sistema existente
- Hay que identificar el “radio de impacto” (blast radius) de un cambio y crear “firewalls” estructurales para minimizar hasta dónde se propagan sus efectos
- Con el ejemplo real del servicio Nerve, se presenta una forma de diseñar límites claros entre el planificador de consultas y el ejecutor de consultas, de modo que las partes modificadas no crucen esa frontera
- Evitar la propagación innecesaria de cambios facilita la verificación y el mantenimiento, y mejora la estabilidad
- Esto también está alineado con la filosofía del OCP (Open-Closed Principle): extender funcionalidades sin cambiar el comportamiento existente
Inducción (Induction)
- Muchos programas incluyen funciones recursivas o estructuras recursivas, y la inducción es una herramienta poderosa para establecer su lógica
- Para demostrar paso a paso el comportamiento y la corrección de una función recursiva, hay que verificar por separado el caso base (base case) y el paso inductivo (inductive step)
- Se pone como ejemplo el proceso de simplificación de nodos en una estructura AST (árbol de sintaxis), mostrando cómo una argumentación inductiva por etapas demuestra la conservación de invariantes y el comportamiento correcto
- Cuando este pensamiento inductivo se internaliza, escribir y verificar código recursivo se vuelve mucho más intuitivo y sencillo
- También vale la pena comparar este enfoque con intentos de verificación globales (holistic) y reflexionar sobre cuál resulta más natural
Proof-affinity como métrica de calidad
- El autor sostiene que el buen código es aquel sobre el que se pueden “dibujar pequeñas pruebas” mentalmente
- Si el código tiene estructuras como monotonicidad, inmutabilidad, condiciones claras, partición de invariantes, límites tipo firewall y uso de inducción, entonces efectivamente es más fácil de demostrar, y por lo tanto también es de mayor calidad
- Si el código es difícil de entender y verificar, eso sugiere la necesidad de refactorizar o replantear la estructura
- En este contexto, propone el término proof-affinity en lugar de “demostrabilidad”
- La proof-affinity no es el único factor de calidad del software, pero sí un catalizador muy importante para entender, extender, probar y mantener código
Cómo mejorar tus habilidades
- Esta forma de pensamiento lógico solo se aplica de manera natural e inconsciente cuando se acumula suficiente práctica
- Es fundamental escribir pruebas (matemáticas) con frecuencia y desarrollar la capacidad de razonamiento lógico
- Resolver problemas de algoritmos (como los cursos de EdX de Stanford, Leetcode, etc.) también es un muy buen campo de entrenamiento; enfocarse en problemas que requieran implementación cuidadosa y pensamiento demostrativo, y no solo trucos, puede dar mejores resultados
- Más que corregir el resultado varias veces hasta acertar, es importante practicar cómo acercarse a la respuesta correcta desde el primer intento
- A través de esta formación de hábitos, el diseño de sistemas lógicos y la calidad del código pueden mejorar enormemente
1 comentarios
Opinión de Hacker News
Hay un ejemplo perfecto para este tema, simple pero sorprendente: la búsqueda binaria. Hay variantes izquierda/derecha, pero si no piensas en el invariante del bucle, es muy difícil implementarla bien. Este artículo explica el enfoque basado en invariantes y muestra un ejemplo de código en Python. Jon Bentley, autor de Programming Pearls, les pidió a programadores de IBM que implementaran una búsqueda binaria común y 90% tenía bugs. La mayoría caía en bucles infinitos. En esa época también había que prevenir manualmente el integer overflow, así que se entiende un poco, pero igual es una proporción sorprendente
Empecé a usar búsqueda binaria como pregunta de entrevista después de ver esto. Cerca de 2/3 de candidatos bien conocidos no pudieron hacer una implementación que funcionara correctamente en menos de 20 minutos. En particular, muchos caían en bucles infinitos en casos fáciles. Quienes sí lo lograban la implementaban rápido. Una de las causas es que mucha gente aprende con una interfaz equivocada. Incluso Wikipedia explica "inicializa L en 0 y R en n-1", pero eso usa un rango con R inclusivo. En la práctica, en la mayoría de algoritmos de strings es mejor no incluir el límite superior, es decir, usar R = n. Me gustaría probar esta hipótesis directamente: hacer que mucha gente la escriba con distintos prototipos de función y valores iniciales, y comparar cuántos bugs aparecen al usar límite superior inclusivo, exclusivo o enfoque por longitud
En realidad, la búsqueda binaria es casi el ejemplo por excelencia de lo complicado que puede ser manejar índices. Junto con el algoritmo de partición de Hoare, es uno de los algoritmos básicos más difíciles de codificar con precisión sin cometer errores
Como prueba, le pedí a Claude Sonnet que escribiera código Python de búsqueda binaria sin bugs
También verifiqué varios casos de prueba con arreglos de ejemplo
Sabiendo que los bugs en búsqueda binaria son famosos por culpa de malas prácticas convertidas en modelo, me propuse incluir en un libro mi primera implementación sin bugs. La escribí con muchísimo cuidado, pero aun así tenía un bug, lo cual da risa. Por suerte, gracias al sistema de feedback previo de Manning, pude corregirlo antes de imprimir
Yo siempre implemento la búsqueda binaria izquierda/derecha recordando "el mejor valor hasta ahora". Es el estilo de
lower_boundyupper_bounden C++. En una estructurawhile (l < r), encuentro el punto medio, reviso la posición actual y ajusto el rango según corresponda. Por ejemplo, enupper_boundsubo el límite izquierdo, y enlower_boundbajo el derecho. Hace tiempo que no hago leetcode y ando algo atontado, así que el formato puede estar medio desordenadoCreo que conocí una idea parecida hace mucho en un curso de posgrado. Desde casi el final de la licenciatura empecé a rendir exámenes de matemáticas solo con bolígrafo. No sé bien por qué, pero mis notas siempre eran altas, y era porque resolvía todo de una sola pasada, habiendo construido por completo el proceso en mi cabeza antes de escribirlo. Eso reducía mucho los errores. Cuando programo, también suelo empezar solo después de haber diseñado la solución con bastante completitud en la cabeza
Para ser un mejor programador, hay que crear el hábito de escribir pequeñas pruebas dentro del código Las pruebas y las definiciones de tipos son justamente ejemplos de eso Sobre todo, conviene abordar las cosas en este orden: primero las pruebas, luego los tipos y al final el código Lo ideal es crear pruebas para cada acceptance criteria y escribir pruebas donde la entrada/salida quede claramente explicada Si es una API, puedes crear primero una especificación completa con OpenAPI o GraphQL, incluyendo todas las propiedades y tipos. En runtime puedes validar los datos con base en esa especificación, y esa misma especificación sirve como prueba de que la app se comporta según lo definido En resumen, es importante asegurar mediante OpenAPI/GraphQL, pruebas y tipos, una prueba de que el sistema realmente funciona como fue pensado Si diseñas bien la especificación desde el inicio, puedes cambiar la implementación del código con flexibilidad y seguir demostrando su corrección a partir de la especificación La especificación es más importante que el código mismo
Aprendí fundamentos de ciencias de la computación teórica en la universidad y coincido con la idea central del artículo. Llevarlo a la práctica no es fácil Además de las precondiciones y postcondiciones, técnicas de prueba de CS como el loop invariant y la inducción estructural son muy poderosas Recomiendo loop invariant, structural induction y también las notas del curso CSC236H de UofT (notas del curso)
Estas notas de CSC236 son excelentes, y el profesor David Liu también es muy buena onda perfil del profesor
¡Mencionaron a UofT! Me da gusto
La idea de "hacer pequeñas pruebas mentalmente sobre el código" es un principio tan importante que debería ser obvio. Siempre deberías tener presente una proposición simple sobre lo que hace cada parte del código
Esto es fácil en proyectos greenfield (cuando tú mismo escribiste todo el código hace poco), pero se siente mucho más difícil en codebases reales donde varios desarrolladores tocan distintas funciones o estado global
Un desarrollador realmente bueno tiene la capacidad de hacer que un sistema evolucione gradualmente hacia esa dirección. El código del mundo real es un desastre, pero lo importante es ir reduciendo poco a poco los huecos en los invariantes y crear una estructura de código que permita que los siguientes desarrolladores también los reconozcan y mantengan. La documentación ayuda, pero en mi experiencia la estructura del código pesa todavía más
De hecho, esa es la razón decisiva por la que el estado global es peligroso. Para probar la corrección del código, necesitas conocer el programa entero. Si conviertes variables globales en valores inmutables, o las pasas como argumentos de función, o las manejas con una clase wrapper que encapsule el estado, entonces basta con identificar claramente a los llamadores de esa función. Si además agregas más restricciones dentro de la función con assertions y similares, la dificultad de la prueba baja muchísimo. Muchos programadores ya toman este tipo de decisiones, solo que lo hacen por instinto, sin pensar conscientemente en la prueba
El código donde varios desarrolladores administran estado global puede compararse con un paciente con "cáncer metastásico". Es mucho más difícil de tratar, y a veces se puede salvar dependiendo de la suerte y de condiciones externas
Como dice el artículo, este tipo de código tiene mucha más probabilidad de generar bugs, y también mayor riesgo de introducir bugs adicionales durante el mantenimiento. Muestra que el camino correcto es escribir desde el inicio con una estructura que permita probar la corrección
Al leer esto pensé en cómo estoy constantemente replanteándome mi manera de programar y tratando de redefinirla hacia algo mejor. Me pregunto si desarrolladores como John Carmack también sienten, con el tiempo, que su código anterior se quedaba corto y que siguen desarrollando un sentido de cómo hacerlo "mejor"
La idea de que el código debe poder probarse apareció por primera vez cuando Dekker resolvió el problema de mutual exclusion en 1959. Una anécdota interesante al respecto aparece en el texto EWD1303 de Dijkstra (enlace original). También puede verse el trabajo posterior de Dijkstra como una continuación de esa intuición
Es realmente difícil escribir pruebas correctas. La verificación de programas tampoco es algo fácil. En mi opinión, intentar hacer pruebas manuales no es eficiente. Si escribes código idiomático para ese lenguaje y ese codebase, casi no hace falta pensar en invariantes ni en precondiciones/postcondiciones. Lo que R. Pike y B. W. Kernighan enfatizan en "The Practice of Programming" —"simplicidad, claridad, generalidad"— tiene un efecto enorme en la práctica. Un poco relacionado, aunque ya es otro tema: si haces competitive programming, de verdad necesitas dominar técnicas para garantizar la corrección del código si quieres pasar al siguiente nivel
No puedo estar de acuerdo con esto. Creo que lo que dice el autor no es que hagas una prueba formal completa, sino que te obligues a pensar qué propiedades lógicas están garantizadas por tu código, por ejemplo los invariantes. Ese proceso es la mejor manera de entender el código y perderle el miedo a su complejidad
Aquí más bien parece que se invirtieron causa y efecto. Si abordas el problema pensándolo con cuidado, como resultado el código naturalmente se vuelve claro y limpio. La lógica tiene que estar clara para que el diseño del código también lo esté. Pero creer que por escribir código bonito la corrección vendrá sola no tiene sentido. Claro, mientras más limpio esté el código, menos bugs habrá en code reviews y similares. Hay que recordar que la forma sigue a la función
El concepto más básico de una prueba es "la razón por la que esto está bien". No se trata de evitar errores triviales, sino de verificar de raíz si la dirección que estás tomando es la correcta
Para la corrección del código no existe ningún sustituto aparte de escribirlo correctamente. Aunque sea difícil, hay que escribirlo bien sí o sí
Si le das la vuelta completa al primer párrafo, lo que obtienes es que, con abstracciones adecuadas (es decir, código idiomático para el lenguaje/codebase), la verificación de programas se vuelve más fácil. En una abstracción adecuada no necesitas preocuparte por loop invariants y similares, así que la prueba se deriva directamente de la corrección del código
La mutabilidad e inmutabilidad (
mutable/immutable) también son propiedades importantes. Mantener el estado lo más inmutable posible reduce la complejidad no solo en multithreading, sino también al razonar sobre el estado del programaEn los 80, cuando era estudiante de pregrado en Carnegie Mellon, me enseñaron estos principios con mucha claridad. Después me ayudaron muchísimo en la vida. Recuerdo especialmente el momento en que entendí la equivalencia entre recursión e inducción; desde entonces pude abordar algoritmos recursivos de forma limpia, en vez de solo "probar cosas hasta que salga la respuesta"