Tikhon Jelvis ya ha proporcionado una respuesta magnífica.
Agregaré un pequeño detalle que la mayoría de los programadores desconocen: la correspondencia de Curry Howard.
Existe una equivalencia entre programas de computadora y pruebas matemáticas.
Para algunos lenguajes (lenguajes funcionales totales o, más genéricamente, cálculos lambda mecanografiados), la equivalencia significa que un tipo de función representa un teorema y la existencia de la implementación de la función es una prueba de ese teorema. Más generalmente, en algunos idiomas, un tipo es una afirmación y un valor de ese tipo es testigo de la verdad de esa afirmación.
(Nota: no estoy siendo formal aquí, estoy tratando de hacer que el concepto sea generalmente accesible incluso sin conocimiento matemático).
Si entrecierra un poco los ojos, verá cómo esto implica que se puede hacer MUCHO en términos de “detección de errores” porque el lenguaje le permite codificar declaraciones formales y sus pruebas. Estas declaraciones formales pueden muy bien ser “sobre el programa” en sí.
- ¿Por qué falla la búsqueda de amplitud primero si el gráfico tiene bordes que son de costos no unitarios?
- ¿Cuáles son algunas de las características que ofrecen los motores de búsqueda como Bing, DuckDuckGo y Baidu, pero no Google?
- ¿Pueden ayudarme con respecto a la siguiente topología?
- ¿Es correcto que XNOR y XOR se comporten igual si tienen un número impar de entradas y se complementan si tienen un número par de entradas?
- ¿Cuál es la diferencia entre una estructura de datos y un tipo de datos abstracto?
Incluso en idiomas con un sistema de tipos demasiado débil para tener pruebas formales (como Haskell), el sistema de tipos puede ser lo suficientemente poderoso como para que pueda razonar sobre el código simplemente mirando los tipos. En Haskell, a menudo puede ver el tipo de función y saber qué hace la función sin ver ninguna documentación y sin mirar la implementación. La razón es que no se pueden codificar “errores” (no escribirían) y todas las implementaciones posibles de esa función hacen exactamente lo mismo.
Esto no es 100% cierto, pero casi: las implementaciones hacen lo mismo O no terminan O lanzan una excepción, y lanzar una excepción o no terminar se considera más o menos un error, en Haskell.
