La brecha entre spec e implementación: ahí viven los bugs

De vez en cuando aparece en los círculos de teoría de lenguajes de programación una afirmación: «una especificación suficientemente detallada es indistinguible del código». La implicación es provocadora: la línea entre describir lo que un programa debe hacer y hacerlo de verdad es más fina de lo que creemos. Si tu especificación es tan precisa que no deja ninguna ambigüedad, en la práctica ya has escrito el programa.

Esto no es solo filosofía. Tiene implicaciones prácticas en cómo construimos software, qué papel juegan las especificaciones y por qué la mayoría de los bugs no son errores de programación, sino huecos en la especificación. Entender dónde terminan las especificaciones y dónde empiezan las implementaciones cambia la forma en que piensas sobre las pruebas, los tipos y la corrección.

De dónde vienen realmente la mayoría de los bugs

Pregúntale a un desarrollador de dónde vienen los bugs y lo más probable es que diga «del código». Pero los estudios sobre defectos de software muestran otra cosa: la mayoría se origina en la brecha entre la intención y la implementación. El código hace exactamente lo que el desarrollador le dijo que hiciera. El problema es que le dijo que hiciera algo equivocado, porque la especificación, formal o informal, era ambigua, incompleta o se malinterpretó.

Un ejemplo clásico: una especificación dice «el sistema debe manejar peticiones concurrentes». ¿Qué significa «manejar»? ¿Procesarlas en orden? ¿Procesarlas a la vez? ¿Ponerlas en cola si son demasiadas? ¿Cuántas son «demasiadas»? ¿Qué pasa con las peticiones que llegan mientras la cola está llena? Estas preguntas no son detalles de implementación, son huecos en la especificación. Y cada pregunta sin respuesta es un bug potencial, porque el desarrollador la responderá de forma implícita con su implementación, y su respuesta podría no coincidir con lo que esperan los usuarios o los demás desarrolladores.

El espectro de precisión de las especificaciones

Las especificaciones existen en un espectro que va de lo informal a lo formal.

• Lenguaje natural. «El sistema de inicio de sesión debe ser seguro y fácil de usar». Esto apenas es una especificación, es un deseo. Cada palabra es ambigua. ¿Qué cuenta como «seguro»? ¿Qué cuenta como «fácil de usar»? Son juicios de valor disfrazados de requisitos.
• Lenguaje natural estructurado. «Cuando un usuario introduce una contraseña incorrecta tres veces en 10 minutos, bloquear la cuenta durante 30 minutos». Más precisa, pero sigue siendo ambigua. ¿Una contraseña «incorrecta» incluye los envíos vacíos? ¿Los tres intentos tienen que ser consecutivos? ¿La ventana de 10 minutos es deslizante o fija?
• Firmas de tipos. authenticate(username: string, password: string) -> Result<User, AuthError>. Esto especifica con precisión la interfaz de la función, pero no dice nada sobre su comportamiento. Conoces la forma de lo que entra y lo que sale, pero no la relación entre ambas cosas.
• Especificaciones basadas en propiedades. «Para todo par válido de usuario y contraseña en la base de datos, authenticate devuelve Ok(user) donde user.username == username». Esto restringe el comportamiento con más precisión usando cuantificadores lógicos.
• Especificación formal. Un modelo matemático completo del comportamiento del sistema: cada estado, cada transición, cada invariante. A este nivel, la especificación y la implementación son casi lo mismo.

Cuanto más te acercas a la especificación formal, menos espacio queda para la ambigüedad y, por tanto, para los bugs. Pero cada paso exige más esfuerzo y habilidades más especializadas. La pregunta práctica es: ¿hasta dónde conviene avanzar en este espectro para un proyecto concreto?

Los tipos como especificaciones ligeras

Los sistemas de tipos son la forma de especificación más extendida en la programación diaria. No describen el comportamiento, pero sí lo restringen. Una función que devuelve Option<User> en lugar de User especifica que puede no encontrar un usuario, y el compilador obliga a cada llamador a contemplar esa posibilidad.

// The type signature IS a specification.
// This function takes a user ID and might not find a user.
// The compiler ensures every caller handles the None case.
fn find_user(id: UserId) -> Option<User> { ... }
// Compare with the stringly-typed version:
// fn find_user(id: &str) -> User  // What if ID is invalid?
//                                  // What if user not found?
//                                  // Does it panic? Return null?
//                                  // The type tells you nothing.
// Richer types encode more specification:
enum WithdrawError {
InsufficientFunds { available: Money, requested: Money },
AccountFrozen { reason: String, until: DateTime },
DailyLimitExceeded { limit: Money, spent: Money },
}
fn withdraw(account: &Account, amount: Money) -> Result<Transaction, WithdrawError>
// The error type specifies exactly what can go wrong and what
// information is available when it does. This is specification
// through the type system.

Lenguajes como Rust, Haskell y TypeScript muestran cómo los sistemas de tipos expresivos reducen la brecha de especificación sin requerir formación en métodos formales. Los tipos algebraicos, las restricciones genéricas y el pattern matching exhaustivo especifican en conjunto gran parte del comportamiento del programa a nivel de tipos, y el compilador lo verifica automáticamente.

La idea clave: cada anotación de tipo es una especificación que se comprueba automáticamente. Cada parte del comportamiento que puedes codificar en el sistema de tipos es una clase de bugs que nunca tendrás.

Pruebas basadas en propiedades: especificar el comportamiento

Los tests unitarios son especificaciones basadas en ejemplos: «para esta entrada concreta, espera esta salida concreta». Son útiles, pero inherentemente incompletos, porque solo puedes probar los casos que se te ocurren. Las pruebas basadas en propiedades invierten esta idea: especificas propiedades que deben cumplirse para todas las entradas, y el framework de pruebas genera entradas aleatorias para encontrar violaciones.

from hypothesis import given, strategies as st
# Unit test: one example
def test_sort_specific():
assert sort([3, 1, 2]) == [1, 2, 3]
# Property-based test: specifies what sort MEANS
@given(st.lists(st.integers()))
def test_sort_properties(lst):
result = sort(lst)
# Property 1: output has same length as input
assert len(result) == len(lst)
# Property 2: output is ordered
for i in range(len(result) - 1):
assert result[i] <= result[i + 1]
# Property 3: output contains the same elements
assert sorted(result) == sorted(lst)
# These three properties together SPECIFY sorting.
# Any function that satisfies all three IS a sort function.
# The property-based test IS the specification.

Las tres propiedades de esa prueba no solo prueban el ordenamiento, sino que lo definen. Cualquier función que cumpla las tres propiedades es, por definición, un ordenamiento correcto. Esta es la idea de «la especificación como código» en su forma más práctica: escribes propiedades que definen el comportamiento correcto y dejas que el framework de pruebas verifique que tu implementación las cumple.

TLA+ y model checking

Para los sistemas donde los bugs son caros, como sistemas distribuidos, plataformas financieras o infraestructura crítica, las herramientas de especificación formal como TLA+ ofrecen garantías más fuertes. TLA+ (Temporal Logic of Actions) te permite especificar el comportamiento de un sistema como una máquina de estados y luego hacer model checking: explorar de forma exhaustiva todas las ejecuciones posibles para verificar que las invariantes se cumplen.

Amazon ha usado TLA+ para verificar algoritmos en S3, DynamoDB y otros servicios críticos de AWS. Han contado públicamente que encontraron bugs que habrían sido prácticamente imposibles de detectar con pruebas: bugs que solo aparecen con entrelazados específicos de operaciones concurrentes que ocurren una vez en millones de ejecuciones.

La especificación en TLA+ de un protocolo de consenso como Raft suele tener unas pocas cientos de líneas. Describe cada transición de estado legal, cada invariante (por ejemplo, «como máximo un líder por término») y cada propiedad de seguridad. El model checker explora después miles de millones de caminos de ejecución posibles, verificando que ninguno viole una invariante. Es una especificación realmente cercana al código: lo bastante precisa como para traducirla mecánicamente a una implementación.

Diseño por contrato

El Diseño por Contrato (DbC) de Bertrand Meyer ocupa un punto medio práctico. Cada función especifica precondiciones (lo que debe ser cierto antes de llamarla), postcondiciones (lo que la función garantiza al devolver el control) e invariantes (lo que siempre debe ser cierto para el objeto). Estos contratos se comprueban en tiempo de ejecución durante el desarrollo y, opcionalmente, se desactivan en producción por rendimiento.

def transfer(from_account, to_account, amount):
"""Transfer money between accounts.
Preconditions:
amount > 0
from_account.balance >= amount
from_account != to_account
Postconditions:
from_account.balance == old(from_account.balance) - amount
to_account.balance == old(to_account.balance) + amount
from_account.balance + to_account.balance ==
old(from_account.balance) + old(to_account.balance)
"""
# The postconditions above fully specify what this function does.
# The last postcondition (conservation) catches a class of bugs
# (money created or destroyed) that unit tests might miss.
assert amount > 0, "Transfer amount must be positive"
assert from_account.balance >= amount, "Insufficient funds"
assert from_account != to_account, "Cannot transfer to same account"
from_account.balance -= amount
to_account.balance += amount

La postcondición de conservación, que el total de dinero antes y después de la transferencia es el mismo, es el tipo de invariante que detecta bugs que los tests unitarios rara vez cubren. Especifica una propiedad fundamental del sistema (el dinero no se crea ni se destruye) que cualquier implementación correcta debe cumplir.

Recomendaciones prácticas

La especificación formal completa no es práctica para la mayoría del software. Pero puedes reducir mucho la brecha de especificación con técnicas que encajan en un flujo de desarrollo normal.

1. Usa el sistema de tipos a fondo. Codifica las restricciones como tipos siempre que sea posible. Prefiere NonEmptyList frente a List cuando la lista no debería estar vacía. Usa wrappers newtype para distinguir UserId de OrderId, aunque ambos sean strings. Cada restricción que codificas en tipos es una restricción que el compilador comprueba gratis.
2. Escribe pruebas basadas en propiedades para la lógica central. Identifica las invariantes que tu sistema debe mantener y expresalas como tests de propiedades. Incluso unas pocas propiedades bien elegidas detectan bugs que miles de tests basados en ejemplos se pierden.
3. Especifica las fronteras. Las especificaciones más importantes están en los límites del sistema: contratos de API, esquemas de base de datos, formatos de mensajes. Usa OpenAPI, Protocol Buffers o JSON Schema para que sean verificables por máquina.
4. Usa TLA+ o Alloy para sistemas concurrentes críticos. Si estás diseñando un algoritmo de consenso, un lock distribuido o un sistema de transacciones financieras, el coste de la especificación formal es pequeño comparado con el de los bugs sutiles de corrección en producción.
5. Escribe la especificación antes que los tests. Si no puedes definir con precisión cómo es el comportamiento correcto, no puedes verificarlo. Dedicar 30 minutos a escribir una especificación clara de lo que debe hacer una función (todos los casos, incluidos los extremos) suele revelar problemas de diseño antes de escribir una sola línea de código.

La afirmación de que «una especificación suficientemente detallada es código» no es del todo correcta. Es más preciso decir que una especificación suficientemente detallada elimina el espacio para los bugs. La brecha entre especificación e implementación es donde vive la ambigüedad, y la ambigüedad es donde se reproducen los bugs. Cada técnica que reduce esa brecha (tipos, propiedades, contratos, métodos formales) hace tu software más correcto. No porque evite los errores de programación, sino porque previene los errores de especificación de los que suelen nacer.