Duchas frías sobre temas sobrevalorados (2017)

Las afirmaciones de que la tipificación estática, la verificación formal y otras técnicas de “bala de plata” reducen de forma fiable los errores de software reciben aquí un escrutinio intenso. Los comentaristas señalan evidencia empírica mixta o débil, la dificultad de diseñar buenos estudios sobre la productividad de los desarrolladores y el riesgo de extrapolar en exceso desde la experiencia personal o el hype. A lo largo del debate, lo comparan con modas de salud como las duchas frías y el uso de saunas, y sostienen que los sistemas complejos —tanto el cuerpo humano como los equipos de software— rara vez ceden ante prescripciones simples y universalmente correctas.

Exposición al frío, saunas y afirmaciones de salud

  • Algunos esperaban que el repositorio tratara sobre el método Wim Hof; los comentarios señalan problemas legales y acrobacias extremas como razones por las que él mismo podría necesitar una “ducha fría”.
  • Una opinión: los baños de hielo diarios y otros extremos similares son “antinaturales”, con la preocupación de que puedan acortar la esperanza de vida.
  • Contraargumento: el estrés térmico moderado (por ejemplo, saunas a 175°F) se asocia en estudios observacionales con una menor mortalidad por todas las causas, posiblemente mediante estrés cardiovascular y respuestas de choque térmico.
  • Otros cuestionan los factores de confusión (nivel socioeconómico, tiempo libre, estrés) y la calidad general de esos estudios, citando la crisis de reproducibilidad más amplia.
  • Contexto cultural: en algunas regiones las saunas son baratas, ubicuas y usadas en todos los niveles de ingresos; otros sostienen que una sauna de más de $1k o el acceso a un gimnasio de lujo claramente no es universal.

Duchas frías y beneficios subjetivos

  • Varias personas dicen hacer duchas de contraste caliente–frío o duchas puramente frías, describiendo:
    • Elevación del estado de ánimo a corto plazo, alerta, sensación de poder “hacerlo”.
    • Uso de técnicas de respiración específicas para volverlo más tolerable.
    • Un “reinicio” hedónico de la línea base, donde la incomodidad hace que el calor y la comodidad normales se sientan mucho mejor.
  • Sigue habiendo escepticismo sobre los beneficios para la salud a largo plazo; muchos lo presentan como un truco de estilo de vida o psicológico más que como una intervención probada de longevidad.

El “hype” de la tipificación estática y la evidencia

  • La “ducha fría” del repositorio sobre la tipificación estática: la literatura hasta ~2014 es mixta; las afirmaciones fuertes sobre reducción de errores no están claramente respaldadas.
  • Muchos sostienen que los tipos estáticos obviamente eliminan clases enteras de errores de tipo y mejoran el soporte del IDE y la documentación, especialmente para equipos y código de larga duración.
  • Otros enfatizan las compensaciones: más trabajo inicial, más código, posible sobreingeniería y “luchar contra el sistema de tipos”, especialmente en algunos ecosistemas Java.
  • La investigación citada en la discusión sugiere:
    • Beneficios claros para la documentación, la navegación y algunas clases de errores.
    • Impacto no concluyente en los “errores lógicos” y en la densidad total de defectos; confusión por diferencias de lenguaje y por el diseño de los estudios.
  • Sigue el desacuerdo sobre si el efecto es grande, pequeño o prácticamente imposible de medir.

Métodos formales y verificación

  • El material enlazado caracteriza la verificación formal como poderosa pero difícil, costosa y a menudo incapaz de detectar errores críticos.
  • Los comentarios añaden matices:
    • Demuestra conformidad con una especificación, que a su vez puede estar equivocada o cambiar constantemente.
    • Sigue siendo valiosa en contextos de seguridad crítica y para descubrir errores de especificación.
    • Se elogian los métodos “ligeros” (por ejemplo, model checking, pensamiento al estilo TLA+) por mejorar el diseño incluso sin pruebas completas.

Meta: investigación en ingeniería de software y hype

  • Muchos expresan un profundo escepticismo hacia la investigación empírica en ingeniería de software:
    • Medir “errores”, productividad o calidad es difícil; métricas como “errores por LOC” se consideran engañosas.
    • Estudios mal diseñados y factores de confusión no contabilizados pueden hacer que los datos sean peores que no tener ninguno.
  • Otros argumentan que los datos imperfectos aun así contienen señal y son mejores que las decisiones puramente anecdóticas.
  • Un tema recurrente: la ingeniería de software es joven; tanto la investigación como las “mejores prácticas” personales son provisionales, y muchas ideas populares (tipificación estática, TDD, métodos formales, trucos de salud milagrosos) merecen tanto entusiasmo como duchas frías regulares.