En 1992, Leslie Lamport, conocido por sus trabajos en sistemas distribuidos y por haber creado LaTeX, publicó una nota titulada "Types Considered Harmful", en la que defendía que los lenguajes de especificación debían basarse en formalismos no tipados (una suerte de teoría de conjuntos) en lugar de en formalismos tipados. Según argumentaba, los sistemas no tipados eran más flexibles y los errores de tipo se detectaban igualmente durante la verificación. El artículo, enviado a TOPLAS, fue rechazado por los dos revisores: el autor de este relato (anónimo en el texto) y David McAllester. Sin embargo, el editor Andrew Appel propuso transformar la pieza en un artículo técnicamente riguroso manteniendo el espíritu original, y el revisor aceptó la coautoría con Lamport. Tras un accidentado proceso editorial —el nuevo editor envió el manuscrito a revisores que también lo rechazaron— el trabajo acabó publicándose con una nota invitando al debate.
Casi tres décadas después, la tesis de Lamport no se sostiene: los sistemas de tipos han madurado y respaldan proyectos verificados a escala industrial, como el compilador CompCert, el microkernel seL4 o el Nitro Isolation Engine de Amazon. Además, incluso el propio lenguaje TLA+ de Lamport incorporó restricciones de tipo en su implementación. Los formalismos conjuntistas, señalan, siguen arrastrando problemas como la ausencia de sobrecarga de notación y una mayor propensión al error, difícil de corregir mediante verificación. El relato, entre técnico y autobiográfico, repasa además la maestría tipográfica de Lamport en TeX y los avatares de la revisión por pares en informática teórica.