Me he dado cuenta de que me resulta mucho más fácil escribir pruebas matemáticas sin cometer errores, que escribir un programa de computadora sin errores.

Parece que esto es algo más extendido que solo mi experiencia. La mayoría de las personas cometen errores de software todo el tiempo en su programación, y tienen el compilador para decirles cuál es el error todo el tiempo. Nunca he oído hablar de alguien que haya escrito un gran programa informático sin errores de una sola vez y que tuviera plena confianza en que no tendría errores. (De hecho, casi ningún programa tiene errores, incluso muchos altamente depurados).

Sin embargo, las personas pueden escribir artículos completos o libros de pruebas matemáticas sin que ningún compilador les dé retroalimentación de que cometieron un error, y a veces sin siquiera recibir retroalimentación de otros.

Déjame ser claro. Esto no quiere decir que las personas no cometan errores en las pruebas matemáticas, pero incluso para los matemáticos con poca experiencia, los errores generalmente no son tan problemáticos y pueden resolverse sin la ayuda de algún "oráculo externo" como un compilador que apunta a su Error.

De hecho, si este no fuera el caso, me parece que las matemáticas apenas serían posibles.

Así que esto me llevó a hacer la pregunta: ¿Qué hay de diferente en escribir pruebas matemáticas impecables y escribir código informático sin fallas que haga que el primero sea mucho más manejable que el segundo?

Se podría decir que es simplemente el hecho de que las personas tienen el "oráculo externo" de un compilador que les señala sus errores lo que hace que los programadores sean vagos, impidiéndoles hacer lo necesario para escribir código rigurosamente. Esta opinión significaría que si no tuvieran un compilador, serían tan impecables como los matemáticos.

Puede encontrar esto persuasivo, pero según mi experiencia en la programación y la escritura de pruebas matemáticas, me parece intuitivamente que esto realmente no es una explicación. Parece que hay algo más fundamentalmente diferente en los dos esfuerzos.

Mi pensamiento inicial es que lo que podría ser la diferencia es que, para un matemático, una prueba correcta solo requiere que cada paso lógico sea correcto. Si cada paso es correcto, toda la prueba es correcta. Por otro lado, para que un programa no tenga errores, no solo todas las líneas de código deben ser correctas, sino que su relación con todas las demás líneas de código del programa también debe funcionar.

En otras palabras, si el paso en una prueba es correcto, cometer un error en el paso Y no arruinará el paso X nunca. Pero si una línea de código X se escribe correctamente, cometer un error en la línea Y influirá en el funcionamiento de la línea X , de modo que siempre que escribamos la línea X tengamos que tener en cuenta su relación con todas las demás líneas. Podemos usar la encapsulación y todas esas cosas para limitar esto, pero no se puede eliminar por completo.$X$$Y$$X$$X$$Y$$X$$X$

Esto significa que el procedimiento para verificar errores en una prueba matemática es esencialmente lineal en el número de pasos de prueba, pero el procedimiento para verificar errores en el código de la computadora es esencialmente exponencial en el número de líneas de código.

¿Qué piensas?

Nota: Esta pregunta tiene una gran cantidad de respuestas que exploran una gran variedad de hechos y puntos de vista. Antes de responder, léalas todas y responda solo si tiene algo nuevo que agregar. Las respuestas redundantes, o las respuestas que no respaldan opiniones con hechos, pueden eliminarse.

Permítanme ofrecer una razón y un concepto erróneo como respuesta a su pregunta.

La razón principal por la que es más fácil escribir (aparentemente) pruebas matemáticas correctas es que están escritas a un nivel muy alto. Suponga que puede escribir un programa como este:

function MaximumWindow(A, n, w):
    using a sliding window, calculate (in O(n)) the sums of all length-w windows
    return the maximum sum (be smart and use only O(1) memory)

Sería mucho más difícil equivocarse al programar de esta manera, ya que la especificación del programa es mucho más sucinta que su implementación . De hecho, cada programador que intenta convertir pseudocódigo a código, especialmente a código eficiente, encuentra este gran abismo entre la idea de un algoritmo y los detalles de su implementación . Las pruebas matemáticas se concentran más en las ideas y menos en los detalles.

La verdadera contraparte del código para las pruebas matemáticas son las pruebas asistidas por computadora . Estos son mucho más difíciles de desarrollar que las pruebas textuales habituales, y uno a menudo descubre varios rincones ocultos que son "obvios" para el lector (que generalmente ni siquiera los nota), pero no tan obvio para la computadora. Además, dado que la computadora solo puede llenar huecos relativamente pequeños en la actualidad, las pruebas deben elaborarse a un nivel tal que un humano que las lea extrañe el bosque por los árboles.

Una idea errónea importante es que las pruebas matemáticas a menudo son correctas. De hecho, esto es probablemente bastante optimista. Es muy difícil escribir pruebas complicadas sin errores, y los documentos a menudo contienen errores. Quizás los casos recientes más celebrados son el primer intento de Wiles de (un caso especial de) el teorema de modularidad (que implica el último teorema de Fermat), y varias lagunas en la clasificación de grupos simples finitos, incluidas más de 1000 páginas sobre grupos de cuasitina que fueron escrito 20 años después de que supuestamente se terminó la clasificación.

Un error en un artículo de Voevodsky le hizo dudar tanto de las pruebas escritas que comenzó a desarrollar la teoría del tipo de homotopía , un marco lógico útil para desarrollar formalmente la teoría de la homotopía, y en adelante utilizó una computadora para verificar todo su trabajo posterior (al menos según su propio trabajo). admisión). Si bien esta es una posición extrema (y actualmente poco práctica), sigue siendo el caso de que cuando se usa un resultado, se debe revisar la prueba y verificar si es correcta. En mi área hay algunos documentos que se sabe que están equivocados pero nunca se han retractado, cuyo estado se transmite de boca en oreja entre los expertos.

(Probablemente estoy arriesgando algunos votos negativos aquí, ya que no tengo tiempo / interés para hacer de esta una respuesta adecuada, pero encuentro que el texto citado (y el resto del artículo citado) a continuación es bastante perspicaz, también teniendo en cuenta que están escritos por un conocido matemático. Quizás pueda mejorar la respuesta más adelante).

La idea, que supongo que no es particularmente distinta de la respuesta existente, es que una "prueba" o argumento se comunica a una comunidad matemática, donde el propósito es convencerlos de que los detalles (tediosos) pueden llenarse, en principio, para obtener una prueba formal completamente especificada, sin hacerlo a menudo en absoluto. Una instancia crítica de esto es que puede usar los teoremas existentes simplemente estableciéndolos, pero la reutilización del código es mucho más desafiante en general. También considere pequeños "errores", que pueden hacer que un código sea completamente inútil (p. Ej., SEGFAULTs) pero puede dejar un argumento matemático en gran parte intacto (es decir, si el error puede ser contenido sin que el argumento colapse).

El estándar de corrección e integridad necesario para que un programa de computadora funcione es un par de órdenes de magnitud más alto que el estándar de pruebas válidas de la comunidad matemática. No obstante, los programas de computadora grandes, incluso cuando se han escrito y probado con mucho cuidado, siempre parecen tener errores. [...] La matemática tal como la practicamos es mucho más formal y precisa que otras ciencias, pero es mucho menos formal y precisa para su contenido que los programas de computadora. La diferencia tiene que ver no solo con la cantidad de esfuerzo: el tipo de esfuerzo es cualitativamente diferente. En grandes programas de computadora, se debe dedicar una tremenda proporción de esfuerzo a una miríada de problemas de compatibilidad: asegurarse de que todas las definiciones sean consistentes, desarrollar "bien" estructuras de datos que tienen una generalidad útil pero no engorrosa, que deciden sobre la generalidad "correcta" para las funciones, etc. La proporción de energía gastada en la parte de trabajo de un programa grande, a diferencia de la parte de contabilidad, es sorprendentemente pequeña. Debido a problemas de compatibilidad que casi inevitablemente se escapan de las manos porque las definiciones "correctas" cambian a medida que se agrega la generalidad y la funcionalidad, los programas de computadora generalmente deben reescribirse con frecuencia, a menudo desde cero.

SOBRE PRUEBAS Y PROGRESO EN MATEMÁTICAS (pp. 9-10), por WILLIAM P. THURSTON https://arxiv.org/pdf/math/9404236.pdf

Permítanme comenzar citando a EW Dijkstra:

"La programación es una de las ramas más difíciles de las matemáticas aplicadas; es mejor que los matemáticos más pobres sigan siendo matemáticos puros". (desde EWD498)

Aunque lo que Dijkstra quiso decir con 'programación' difiere bastante del uso actual, todavía hay algo de mérito en esta cita. Las otras respuestas ya han mencionado que se permite que el nivel de abstracción en matemáticas sea mucho mayor que en programación, lo que significa que podemos ignorar algunas partes difíciles si lo deseamos.

Sin embargo, creo que esto es simplemente una consecuencia de una diferencia más fundamental entre una prueba y un programa de computadora, que es su propósito .

El propósito principal de una prueba matemática es, entre otros, convencerse de que una afirmación matemática es correcta y, quizás aún más importante, lograr la comprensión . Por lo tanto, puede optar por trabajar solo en el mundo matemático, donde todo se crea de tal manera que se pueda alcanzar la comprensión diseño (aunque algunos estudiantes piden diferencias ...) Esto es precisamente lo que Dijkstra quiso decir con "matemáticos puros", aquellos que (casi) solo se ocupan de hechos matemáticos y de comprender sus propiedades.

Por lo tanto, no debería sorprenderse que la producción de pruebas correctas sea relativamente a prueba de fallas: es el objetivo de todo el "ejercicio". (Aún así, esto no significa que los errores no existan o apenas existan, errar es solo humano, dicen)

Ahora, si consideramos la programación, ¿cuál es nuestro propósito? Realmente no buscamos comprensión, queremos algo que funcione . ¿Pero cuándo algo "funciona"? Algo funciona cuando hemos creado con éxito algo que permite que alguna máquina extraña complete la tarea que queremos que haga y preferiblemente también bastante rápido.

Esta es, creo, la diferencia fundamental, ya que significa que nuestro objetivo no puede ser simplemente declarado como un teorema que nuestro programa "prueba", deseamos algo en el mundo real. (sea lo que sea), no algún artefacto matemático. Esto significa que no podemos alcanzar nuestro objetivo puramente teóricamente (aunque Dijkstra quiere que lo intentes de todas formas), ya que debemos apaciguar a la máquina, esperar que realmente sepamos qué tarea queremos que haga y también estar al tanto de cosas que ninguno consideró, que aún suceden. de alguna manera.

Por lo tanto, al final, no hay otra forma de intentarlo y simplemente fallar, arreglar, fallar e intentar nuevamente hasta que estemos algo satisfechos con el resultado.

Tenga en cuenta que su hipótesis de escribir pruebas sin fallas es más simple que los programas sin fallas (que de hecho son declaraciones diferentes, como señala @Ariel ), de hecho, pueden ser incorrectas, ya que las pruebas a menudo se construyen mediante prueba y error en algún nivel. Aún así, espero que esto arroje algo de luz sobre la pregunta implícita: "¿Cuál es realmente la diferencia entre probar algún teorema y escribir un programa?" (A lo que un observador descuidado de la correspondencia Curry-Howard podría decir: "¡Nada en absoluto!")

Como @wvxvw mencionó en los comentarios, los siguientes párrafos de 'notas sobre Programación Estructurada' (EWD249, página 21) son muy relevantes:

(...) Un programa nunca es un objetivo en sí mismo; El propósito de un programa es evocar cálculos y el propósito de los cálculos es establecer un efecto deseado. Aunque el programa es el producto final realizado por el programador, los posibles cálculos evocados por él, ¡la "creación" de los mismos se deja a la máquina! - son el verdadero tema de su oficio. Por ejemplo, cada vez que un programador declara que su programa es correcto, realmente hace una afirmación sobre los cálculos que puede evocar.

(...) En cierto sentido, la elaboración de un programa es, por lo tanto, más difícil que la elaboración de una teoría matemática: tanto el programa como la teoría son objetos estructurados e intemporales. Pero si bien la teoría matemática tiene sentido tal como está, el programa solo tiene sentido a través de su ejecución.

Lamport proporciona un motivo para el desacuerdo sobre la prevalencia de errores en las pruebas en Cómo escribir una prueba (páginas 8-9) :

Hace unos veinte años, decidí escribir una prueba del teorema de Schroeder-Bernstein para una clase introductoria de matemáticas. La prueba más simple que pude encontrar estaba en el clásico texto de topología general de Kelley. Como Kelley estaba escribiendo para un público más sofisticado, tuve que agregar una gran explicación a su prueba de media página. Había escrito cinco páginas cuando me di cuenta de que la prueba de Kelley estaba equivocada. Recientemente, quería ilustrar una conferencia sobre mi estilo de prueba con una prueba incorrecta convincente, así que recurrí a Kelley. No pude encontrar nada malo con su prueba; ¡obviamente parecía correcto! Leer y releer la prueba me convenció de que mi memoria había fallado o que era muy estúpida hace veinte años. Aún así, la prueba de Kelley era corta y serviría como un buen ejemplo, así que comencé a reescribirla como una prueba estructurada.

... El estilo se aplicó por primera vez a las pruebas de teoremas ordinarios en un artículo que escribí con Martin Abadi. Ya había escrito pruebas convencionales, pruebas que fueron lo suficientemente buenas como para convencernos a nosotros y, presumiblemente, a los árbitros. Reescribiendo las pruebas en un estilo estructurado, descubrimos que casi todos tenían errores graves, aunque los teoremas eran correctos. Cualquier esperanza de que las pruebas incorrectas no conduzcan a teoremas incorrectos se destruyó en nuestra próxima colaboración. Una y otra vez, haríamos una conjetura y escribiríamos un boceto de prueba en la pizarra, un boceto que fácilmente podría haberse convertido en una prueba convencional convincente, solo para descubrir, al intentar escribir una prueba estructurada, que la conjetura era falsa. Desde entonces, nunca he creído un resultado sin una prueba cuidadosa y estructurada.

Una gran diferencia es que los programas generalmente se escriben para operar en entradas, mientras que las pruebas matemáticas generalmente comienzan a partir de un conjunto de axiomas y teoremas conocidos previamente. A veces tiene que cubrir múltiples casos de esquina para obtener una prueba suficientemente general, pero los casos y su resolución se enumeran explícitamente y el alcance del resultado se limita implícitamente a los casos cubiertos.

Compare esto con un programa de computadora, que debe proporcionar una salida 'correcta' para un rango de posibles entradas. Rara vez es posible enumerar todas las entradas y probarlas todas. Peor aún, ¿y si el programa interactúa con un ser humano y permite que su entrada modifique el funcionamiento? Los seres humanos son notoriamente impredecibles y el número de posibles aportes a un programa razonablemente grande con interacción humana crece a un ritmo prodigioso. Debe intentar prever todas las diferentes formas en que se puede usar un programa e intentar que todos esos casos de uso funcionen o al menos fallen de manera razonable, cuando el fracaso es la única opción. Y eso supone que incluso sabes cómo se supone que debe funcionar en todos esos oscuros casos de esquina.

Finalmente, un programa grande realmente no se puede comparar con una sola prueba, incluso una compleja. Probablemente, un programa grande es más parecido a recopilar y revisar una pequeña biblioteca de literatura, algunos de los cuales pueden tener errores con los que debe evitar. Para programas más en la escala de una sola prueba, que podría ser una implementación de algoritmo pequeño, digamos, los ingenieros de software experimentados pueden / los completan sin cometer errores, especialmente cuando se usan herramientas modernas que evitan / resuelven errores triviales comunes (como errores ortográficos) ) que son equivalentes a los primeros problemas que resolvería al corregir.

Dicen que el problema con las computadoras es que hacen exactamente lo que les dices.

Creo que esta podría ser una de las muchas razones.

Tenga en cuenta que, con un programa de computadora, el escritor (usted) es inteligente pero el lector (CPU) es tonto.
Pero con una prueba matemática, el escritor (usted) es inteligente y el lector (revisor) también es inteligente.

Esto significa que nunca puede darse el lujo de meterse en una situación de "bueno, ya sabes a qué me refiero " con una computadora. Hace exactamente lo que le dices, sin conocer tus intenciones.

Por ejemplo, digamos que este es un paso en alguna prueba:

$x^2+4x+3$$x+3$$x = -3$

Un problema que creo que no se abordó en la respuesta de Yuval es que parece que estás comparando diferentes animales.

$n$$n!$

La verificación de las propiedades semánticas de los programas es indecidible (teorema de Rice) y, de manera análoga, también es indecidible verificar si una declaración en la lógica de predicado de primer orden es verdadera. El punto es que no hay una diferencia real en la dureza de la forma en que estás viendo los problemas. Por otro lado, podemos razonar sobre las propiedades sintácticas de los programas (compiladores), y esto es análogo al hecho de que podemos verificar las pruebas. Los errores (el código no hace lo que quiero) son semánticos, por lo que debe compararlos con su contraparte correcta.

Fortaleceré a Yuval y diré que campos completos crecieron con la motivación de escribir pruebas matemáticas que pueden escribirse y verificarse en algún sistema formal, por lo que incluso el proceso de verificación no es en absoluto trivial.

¿Qué tiene de diferente escribir pruebas matemáticas impecables y escribir código informático impecable que haga que el primero sea mucho más manejable que el segundo?

Creo que las razones principales son la idempotencia (da los mismos resultados para las mismas entradas) y la inmutabilidad (no cambia).

¿Qué pasaría si una prueba matemática pudiera dar resultados diferentes si se leyera un martes o cuando el año avanzara hasta 2000 desde 1999? ¿Qué pasaría si parte de una prueba matemática fuera retroceder algunas páginas, reescribir algunas líneas y luego comenzar de nuevo desde ese punto?

Estoy seguro de que tal prueba sería casi tan propensa a errores como un segmento normal de código de computadora.

También veo otros factores secundarios:

1. Los matemáticos suelen ser mucho más educados antes de intentar escribir una prueba significativa / publicable. 1/4 de los desarrolladores profesionales homónimos comenzaron a codificar hace menos de 6 años (ver la encuesta SO 2017 ), pero supongo que la mayoría de los matemáticos tienen más de una década de educación formal en matemáticas.
2. Las pruebas matemáticas rara vez se mantienen al mismo nivel de escrutinio que el código de computadora. Un solo error tipográfico puede / romperá un programa, pero docenas de errores tipográficos pueden no ser suficientes para destruir el valor de una prueba (solo su legibilidad).
3. El diablo está en los detalles, y el código de la computadora no puede omitir los detalles. Las pruebas son libres de omitir los pasos que se consideran simples / rutinarios. Hay algunos buenos azúcares sintácticos disponibles en los idiomas modernos, pero estos están codificados y son bastante limitados en comparación.
4. Las matemáticas son más antiguas y tienen una base / núcleo más sólido. Ciertamente, hay una gran cantidad de subcampos nuevos y brillantes en matemáticas, pero la mayoría de los principios básicos se han utilizado durante décadas. Esto lleva a la estabilidad. Por otro lado, los programadores aún no están de acuerdo con la metodología básica de codificación (solo pregunte sobre el desarrollo ágil y su tasa de adopción).

Estoy de acuerdo con lo que Yuval ha escrito. Pero también tenga una respuesta mucho más simple: en la práctica, los ingenieros de software generalmente ni siquiera intentan verificar la corrección de sus programas, simplemente no lo hacen, por lo general ni siquiera escriben las condiciones que definen cuándo el programa es correcto.

Hay varias razones para ello. Una es que la mayoría de los ingenieros de software no tienen las habilidades para formular problemas matemáticos con claridad ni saben cómo escribir pruebas de corrección.

Otra es que definir las condiciones de corrección para un sistema de software complejo (especialmente uno distribuido) es una tarea muy difícil y que requiere mucho tiempo. Se espera que tengan algo que parece funcionar en cuestión de semanas.

Otra razón es que la corrección de un programa depende de muchos otros sistemas escritos por otros que nuevamente no tienen una semántica clara. Existe una ley de Hyrum que esencialmente dice que si su biblioteca / servicio tiene un comportamiento observable (que no forma parte de su contrato) alguien eventualmente dependerá de ello. Eso esencialmente significa que la idea de desarrollar software en forma modular con contratos claros como lemas en matemáticas no funciona en la práctica. Empeora en los idiomas en los que se usa la reflexión. Incluso si un programa es correcto hoy, podría romperse mañana cuando alguien realice una refactorización trivial en una de sus dependencias.

En la práctica, lo que suele suceder es que tienen pruebas. Las pruebas actúan como lo que se espera del programa. Cada vez que se encuentra un nuevo error, agregan pruebas para detectarlo. Funciona hasta cierto punto, pero no es una prueba de corrección.

Cuando las personas no tienen las habilidades para definir la corrección o escribir programas correctos, ni se espera que lo hagan, y hacerlo es bastante difícil, no sorprende que los softwares no sean correctos.

Pero tenga en cuenta también que al final, en mejores lugares, la ingeniería de software se realiza mediante revisión de código. Ese es el autor de un programa tiene que convencer al menos a otra persona de que el programa funciona correctamente. Ese es el punto en el que se hacen algunos argumentos informales de alto nivel. Pero nuevamente, por lo general, no ocurre nada parecido a una definición clara y rigurosa de corrección o prueba de corrección.

En matemáticas, las personas se centran en la corrección. En el desarrollo de software, hay muchas cosas que un programador debe tener en cuenta y hay compensaciones entre ellas. Tener un software libre de errores o incluso una buena definición de corrección (con requisitos que cambian con el tiempo) es ideal, pero tiene que ser intercambiado con otros factores y uno de los más importantes es el tiempo dedicado a desarrollarlo. desarrolladores Entonces, en la práctica, en mejores lugares, el objetivo y los procesos están mitigando el riesgo de errores tanto como sea posible en lugar de hacer que el software esté libre de errores.

Ya hay muchas buenas respuestas, pero aún hay más razones por las que las matemáticas y la programación no son lo mismo.

1 Las pruebas matemáticas tienden a ser mucho más simples que los programas de computadora. Considere los primeros pasos de una prueba hipotética:

Deja que un sea un entero

Deje b ser un número entero

Sea c = a + b

Hasta ahora la prueba está bien. Convirtámoslo en los primeros pasos de un programa similar:

Deje a = input ();

Deje b = input ();

Sea c = a + b;

Ya tenemos una miríada de problemas. Suponiendo que el usuario realmente ingresó un número entero, tenemos que verificar los límites. Es un mayor que -32768 (o cualquiera que sea el int min en su sistema es)? Es una de menos de 32767? Ahora tenemos que verificar lo mismo para b . Y como hemos agregado a y b, el programa no es correcto a menos que a + bes mayor que -32768 y menor que 32767. Esas son 5 condiciones separadas de las que un programador debe preocuparse y que un matemático puede ignorar. El programador no solo tiene que preocuparse por ellos, sino que tiene que decidir qué hacer cuando no se cumple una de esas condiciones y escribir código para hacer lo que haya decidido que es la forma de manejar esas condiciones. La matemática es simple. La programación es difícil.

2 El interlocutor no dice si se refiere a errores en tiempo de compilación o errores en tiempo de ejecución, pero a los programadores generalmente no les importan los errores en tiempo de compilación. El compilador los encuentra y son fáciles de arreglar. Son como errores tipográficos. ¿Con qué frecuencia las personas escriben varios párrafos sin errores la primera vez?

3 Entrenamiento.Desde muy pequeños se nos enseña a hacer matemáticas, y enfrentamos las consecuencias de errores menores una y otra vez. Un matemático capacitado tuvo que comenzar a resolver problemas de álgebra de varios pasos, generalmente en la escuela intermedia y tuvo que hacer docenas (o más) de estos problemas cada semana durante un año. Una sola señal negativa caída causó que todo un problema estuviera mal. Después del álgebra, los problemas se hicieron más largos y más difíciles. Los programadores, por otro lado, generalmente tienen una capacitación mucho menos formal. Muchos son autodidactas (al menos inicialmente) y no recibieron capacitación formal hasta la universidad. Incluso a nivel universitario, los programadores tienen que tomar bastantes clases de matemáticas, mientras que los matemáticos probablemente tomaron una o dos clases de programación.

Me gusta la respuesta de Yuval, pero quería hablar un poco de ella. Una razón por la que puede resultarle más fácil escribir pruebas matemáticas puede reducirse a cuán platónica es la ontología matemática. Para ver a qué me refiero, considere lo siguiente:

• Las funciones en matemáticas son puras (todo el resultado de llamar a una función está completamente encapsulado en el valor de retorno, que es determinista y se calcula completamente a partir del valor de entrada).
• Las matemáticas no tienen mutación o reasignación (cuando necesita modelar tales cosas, se utilizan funciones y secuencias).
• La matemática es referencialmente transparente (por ejemplo, sin punteros, sin noción de llamada por nombre versus llamada por valor) y los objetos matemáticos tienen semántica de igualdad extensional (si "dos" cosas son iguales en todas las formas observables, entonces de hecho son la misma cosa).

Si bien es discutible si las restricciones anteriores facilitan o no la escritura de un programa, creo que existe un amplio acuerdo de que las restricciones anteriores facilitan el razonamiento sobre un programa. Lo principal que hace al escribir una prueba de Matemáticas es la razón de la prueba que está escribiendo actualmente (ya que, a diferencia de la programación, nunca tiene que duplicar el esfuerzo en Matemáticas ya que las abstracciones son gratuitas), por lo que generalmente vale la pena insistir en Restricciones anteriores.

Las pruebas matemáticas fundamentales no equivalen a una aplicación del mundo real, diseñada para satisfacer las necesidades de los seres humanos vivos.

Los humanos cambiarán sus deseos, necesidades y requisitos sobre lo que posiblemente sea diario en el ámbito de los programas de computadora.

¿Qué tiene de diferente escribir pruebas matemáticas impecables y escribir código informático impecable que haga que el primero sea mucho más manejable que el segundo?

Con un requisito tan claro como un problema matemático, se podría escribir un programa sin fallas. Probar que el algoritmo de Dijkstra puede encontrar la ruta más corta entre dos puntos en un gráfico no es lo mismo que implementar un programa que acepte entradas arbitrarias y encuentre los puntos más cortos entre dos puntos.

Hay problemas de memoria, rendimiento y hardware para administrar. Ojalá no pudiéramos pensar en eso cuando escribimos algoritmos, que podríamos utilizar construcciones puras y funcionales para gestionar esto, pero los programas de computadora viven en el mundo "real" del hardware, mientras que la prueba matemática reside en ... "teoría".

O, para ser más sucinto :

Mirándolo desde otro ángulo, en un entorno no académico, a menudo se reduce a dinero.

Como las otras publicaciones afirman bien, Math es una especificación abstracta única, por lo tanto, una prueba debe funcionar consistentemente dentro de esa especificación para ser probada. Un programa de computadora puede operar en muchas implementaciones de la especificación abstracta de las matemáticas, es decir, la forma en que un lenguaje o el fabricante de hardware implementa las matemáticas de coma flotante puede ser ligeramente diferente de otro, lo que puede causar ligeras fluctuaciones en los resultados.

Como tal, 'probar' un programa de computadora antes de escribirlo implicaría probar la lógica a nivel de hardware, nivel de sistema operativo, nivel de controlador, lenguaje de programación, compilador, quizás intérprete, etc., para cada combinación posible de hardware que el programa posiblemente podría ejecutarse y cualquier información concebible que pueda ingerir. Probablemente encontrará este nivel de preparación y comprensión en misiones espaciales, sistemas de armas o sistemas de control de energía nuclear, donde el fracaso significa decenas de miles de millones de dólares perdidos y potencialmente muchas vidas perdidas, pero no mucho más.

Para su programador y / o negocio 'cotidiano', es mucho, mucho más rentable aceptar un cierto nivel de precisión en el código mayormente correcto y vender un producto utilizable, y los desarrolladores pueden corregir los errores retroactivamente a medida que se descubren durante su uso.

Creo que su razonamiento es válido, pero su aporte no lo es. Las pruebas matemáticas simplemente no son más tolerantes a fallas que los programas, si ambas están escritas por humanos. Dijkstra ya fue citado aquí, pero ofreceré una cotización adicional.

Sin embargo, debemos organizar los cálculos de tal manera que nuestros poderes limitados sean suficientes para garantizar que el cálculo establezca el efecto deseado. Esta organización incluye la composición del programa y allí nos enfrentamos con el siguiente problema de tamaño, a saber. la longitud del texto del programa, y ​​deberíamos dar a este problema también un reconocimiento explícito. Deberíamos estar conscientes del hecho de que la medida en que podemos leer o escribir un texto depende en gran medida de su tamaño. [...]

Es en el mismo estado de ánimo que me gustaría llamar la atención del lector sobre el hecho de que la "claridad" ha pronunciado aspectos cuantitativos, un hecho que muchos matemáticos, curiosamente, parecen desconocer. Un teorema que establece la validez de una conclusión cuando se cumplen diez páginas llenas de condiciones no es una herramienta conveniente, ya que todas las condiciones deben verificarse siempre que se recurra al teorema. En la geometría euclidiana, el teorema de Pitágoras es válido para tres puntos A, B y C, de modo que a través de A y C se puede dibujar una línea recta ortogonal a una línea recta a través de B y C. ¿Cuántos matemáticos aprecian que el teorema sigue siendo aplicable cuando algunos o todos los puntos A, B y C coinciden? Sin embargo, esto parece en gran parte responsable de la conveniencia con la que se puede utilizar el Teorema de Pitágoras.

Resumiendo: como ser humano de ingenio lento, tengo una cabeza muy pequeña y es mejor que aprenda a vivir con ella y a respetar mis limitaciones y darles todo el crédito, en lugar de tratar de ignorarlas, ya que este último esfuerzo vano será castigado por el fracaso.

Esto está ligeramente editado los últimos tres párrafos del primer capítulo de la Programación estructurada de Dijkstra.

Tal vez para reformular esto, para aplicar mejor a su pregunta: la corrección es en gran medida una función del tamaño de su prueba. La corrección de las pruebas matemáticas largas es muy difícil de establecer (muchas "pruebas" publicadas viven en el limbo de la incertidumbre ya que nadie las verificó realmente). Pero, si compara la corrección de los programas triviales con las pruebas triviales, es probable que no haya una diferencia notable. Sin embargo, los asistentes de prueba automatizados (en un sentido más amplio, su compilador de Java también es un asistente de prueba), permiten que los programas ganen al automatizar mucho trabajo preliminar.

Como otras respuestas han mencionado en sus respuestas (quiero dar más detalles), pero una gran parte del problema es el uso de la biblioteca. Incluso con la documentación perfecta (tan común como el código sin errores), es imposible transferir el conocimiento completo de una biblioteca a cada programador que use la biblioteca. Si el programador no comprende perfectamente su biblioteca, puede cometer errores al usarla. A veces, estos pueden provocar errores críticos que se descubren cuando el código no funciona. Pero para errores menores, estos pueden pasar desapercibidos.

Una situación similar sería si un matemático utilizara pruebas y lemas existentes sin comprenderlos completamente; sus propias pruebas probablemente serían defectuosas. Si bien esto puede sugerir una solución es aprender perfectamente cada biblioteca que uno usa; Esto lleva prácticamente mucho tiempo y puede requerir conocimientos de dominio que el programador no tiene (sé muy poco de la secuenciación de ADN / síntesis de proteínas; sin embargo, puedo trabajar con estos conceptos usando bibliotecas).

En pocas palabras, la ingeniería de software (ingeniería en general realmente) se basa en encapsular diferentes niveles de abstracción para permitir que las personas se concentren en áreas más pequeñas del problema en el que se especializan. Esto permite que las personas desarrollen experiencia en su área, pero también requiere una excelente comunicación entre cada capa Cuando esa comunicación no es perfecta, causa problemas.

Trataré de ser original después de todas esas excelentes respuestas.

Los programas son pruebas

El isomorfismo de Curry-Howard nos dice que los tipos en su programa son los teoremas y el código real es su prueba.

Es cierto que esta es una vista muy abstracta y de alto nivel. El problema que usted probablemente quiere decir es que escribir un código típico es más difícil porque tiene un nivel demasiado bajo. En la mayoría de los casos, "necesita decirle a la máquina qué hacer". O, para ver esto de otra manera: los matemáticos son realmente buenos en la abstracción.

Como nota al margen: "La música de las corrientes" es uno de los puentes más bellos entre ambos. Básicamente configura las cosas para poder decir "Quiero esto de esa manera" y la máquina hace esto mágicamente exactamente como lo desea.

Ninguna de las muchas otras respuestas señala lo siguiente. Las pruebas matemáticas operan en sistemas informáticos imaginarios que tienen memoria infinita y potencia informática infinita. Por lo tanto, pueden mantener números arbitrariamente grandes con una precisión infinita y no perder precisión en ningún cálculo.

$\pi$

No es. Las pruebas matemáticas son exactamente tan defectuosas por naturaleza, es solo que sus lectores son más permisivos que un compilador. Del mismo modo, los lectores de un programa de computadora se dejan engañar fácilmente para creer que es correcto, al menos hasta que intentan ejecutarlo.

Por ejemplo, si intentamos traducir una prueba matemática a un lenguaje formal como ZFC, también contendrá errores. Esto se debe a que estas pruebas pueden ser realmente largas, por lo que nos vemos obligados a escribir un programa para generar la prueba. Poca gente se mete en problemas, bajo su propio riesgo, aunque hay una investigación activa en la formalización de pruebas fundamentales.

Y de hecho, las matemáticas pueden obtener BSOD! ¡No sería la primera vez!

Esta idea ortodoxa de que todas las pruebas matemáticas que han sido suficientemente verificadas son esencialmente correctas o pueden corregirse es la misma que motiva su proyecto de software en el trabajo: siempre y cuando nos mantengamos en la hoja de ruta, eliminaremos todos los errores y características completas: es un proceso iterativo que conduce a un producto final definitivo.

Aquí está el otro lado. Mire, ya tenemos la financiación, validamos el concepto de negocio, todos los documentos están aquí para que los lea. ¡Solo necesitamos que ejecutes y es algo seguro!

No nos sentimos demasiado por Hilbert , él sabía en lo que se estaba metiendo. Es solo negocios.

¡Si quiere estar realmente seguro, tome todo caso por caso y saque sus propias conclusiones!

Veo dos razones importantes por las que los programas son más propensos a errores que las pruebas matemáticas:

1: Los programas contienen variables u objetos dinámicos que cambian con el tiempo, mientras que los objetos matemáticos en las pruebas son normalmente estáticos. Por lo tanto, la notación en matemáticas se puede usar como soporte directo del razonamiento (y si a = b, este sigue siendo el caso) cuando esto no funciona en los programas. Además, este problema empeora cuando los programas son paralelos o tienen múltiples hilos.

2: Matemáticas a menudo asume objetos relativamente bien definidos (gráficos, múltiples, anillos, grupos, etc.), mientras que la programación trata con objetos muy desordenados y bastante irregulares: aritmética de precisión finita, pilas finitas, conversiones de caracteres enteros, punteros, basura que necesita recolección , etc ... Por lo tanto, la recopilación de condiciones relevantes para la corrección es muy difícil de tener en cuenta.

Debe distinguir dos "categorías" diferentes:

• pseudo-pruebas (o pseudo-código) - eso es lo que ves en los libros. Está escrito en lenguaje natural (por ejemplo, en inglés). Eso es lo que debes usar para aprender Matemáticas (o Algoritmos).
• pruebas formales (o código formal): lo escribe cuando necesita que su prueba (o código) sea verificable mecánicamente (o ejecutable). Dicha representación no requiere ninguna "inteligencia humana". Se puede verificar (o ejecutar) mecánicamente, siguiendo algunos pasos predefinidos (generalmente realizados por computadoras hoy en día).

Hemos estado usando pseudocódigo por miles de años (por ejemplo, el algoritmo Euclids). Escribir código formal (en lenguajes formales como C o Java) se volvió extremadamente popular y útil después de la invención de las computadoras. Pero, lamentablemente, las pruebas formales (en lenguajes formales como Principia Mathematica o Metamath) no son muy populares. Y dado que todos escriben pseudo-pruebas hoy, las personas a menudo discuten sobre nuevas pruebas. Los errores en ellos se pueden encontrar años, décadas o incluso siglos después de la "prueba" real.

No puedo encontrar la referencia, pero creo que Tony Hoare dijo una vez algo en las siguientes líneas: La diferencia entre verificar un programa y verificar una prueba es que una prueba se puede verificar dos líneas a la vez.

En una palabra: localidad.

Las pruebas se escriben para que puedan verificarse fácilmente. Los programas están escritos para que puedan ejecutarse. Por esta razón, los programadores generalmente omiten información que sería útil para alguien que revisa el programa.

Considere este programa, donde x es de solo lectura

    assume x >= 0
    p := 0 ;
    var pp := 0 ;
    while( x >= pp + 2*p + 1 ) 
    {
        var q := 1 ;
        var qq := q ;
        var pq := p ;
        while(  pp + 4*pq + 4*qq <= x )
        {
            q, pq, qq := 2*q, 2*pq, 4*qq ;
        }
        p, pp := p + q, pp + 2*pq + qq ;
    }
    assert  p*p <= x < (p+1)*(p+1)

Es fácil de ejecutar, pero difícil de verificar.

Pero si vuelvo a agregar las afirmaciones que faltan, puede verificar el programa localmente simplemente comprobando que cada secuencia de asignaciones es correcta con respecto a sus condiciones previas y posteriores y que, para cada ciclo, la condición posterior del ciclo está implícita en el invariante y la negación de la guardia de bucle.

    assume x >= 0
    p := 0 ;
    var pp := 0 ; 
    while( x >= pp + 2*p + 1 ) 
        invariant p*p <= x 
        invariant pp == p*p
        decreases x-p*p 
    {
        var q := 1 ;
        var qq := q ; 
        var pq := p ; 
        while(  pp + 4*pq + 4*qq <= x )
            invariant (p+q)*(p+q) <= x
            invariant q > 0 
            invariant qq == q*q 
            invariant pq == p*q 
            decreases x-(p+q)*(p+q)
        {
            q, pq, qq := 2*q, 2*pq, 4*qq ;
        }
        assert (p+q)*(p+q) <= x and pp==p*p and pq==p*q and qq==q*q and q>0
        p, pp := p + q, pp + 2*pq + qq ;
    }
    assert  p*p <= x < (p+1)*(p+1)

Volviendo a la pregunta original: ¿Por qué escribir pruebas matemáticas es más a prueba de fallas que escribir código de computadora? Dado que las pruebas están diseñadas para que sus lectores las verifiquen fácilmente, sus autores las verifican fácilmente y, por lo tanto, los autores alertas tienden a no cometer (o al menos mantener) errores lógicos en sus pruebas. Cuando programamos, a menudo fallamos en escribir la razón por la cual nuestro código es correcto; el resultado es que es difícil tanto para los lectores como para el autor de un programa verificar el código; el resultado es que los autores cometen (y luego guardan) errores.

Pero hay esperanza. Si, cuando escribimos un programa, también escribimos la razón por la que creemos que el programa es correcto, entonces podemos verificar el código a medida que lo escribimos y así escribir menos código con errores. Esto también tiene la ventaja de que otros pueden leer nuestro código y verificarlo por sí mismos.

Podríamos preguntar si es más difícil en la práctica o en principio , escribir pruebas o escribir código.

En la práctica, probar es mucho más difícil que codificar. Muy pocas personas que han tomado dos años de matemáticas de nivel universitario pueden escribir pruebas, incluso triviales. Entre las personas que han tomado dos años de CS a nivel universitario, probablemente al menos el 30% puede resolver FizzBuzz .

Pero, en principio , hay razones fundamentales por las que es al revés. Las pruebas se pueden verificar, al menos en principio, para verificar que sean correctas a través de un proceso que no requiere juicio ni comprensión alguna. Los programas no pueden, ni siquiera podemos decir, a través de cualquier proceso prescrito, si un programa se detendrá.

Solo una pequeña porción de las afirmaciones matemáticas que son verdaderas puede demostrarse prácticamente. Más significativamente, sería imposible construir un conjunto no trivial (*) de axiomas matemáticos que permitiría probar todas las afirmaciones verdaderas. Si solo se necesita escribir programas para hacer una pequeña fracción de las cosas que se podrían hacer con las computadoras, sería posible escribir un software que sea probablemente correcto, pero a menudo se pide a las computadoras que hagan cosas más allá del rango de lo que es probablemente correcto El software puede lograr.

(*) Es posible definir un conjunto de axiomas que permitirían enumerar todas las declaraciones verdaderas y, por lo tanto, probarlas, pero generalmente no son muy interesantes. Si bien es posible categorizar formalmente conjuntos de axiomas en aquellos que son o no, relativamente hablando, no triviales, el punto clave es que la existencia comprobable de declaraciones que son verdaderas pero no se pueden probar no es un defecto en un conjunto de axiomas. Agregar axiomas para hacer comprobables las declaraciones existentes verdaderas pero no demostrables causaría que otras declaraciones se vuelvan verdaderas pero sin ellas demostrables.

1. Los programas de computadora se prueban en el mundo real. Un error técnico complicado en una prueba matemática larga, que solo un número limitado de personas puede entender, tiene una buena posibilidad de permanecer sin ser detectado. Es probable que el mismo tipo de error en un producto de software produzca un comportamiento extraño que los usuarios comunes noten. Por lo tanto, la premisa podría no ser correcta.

2. Los programas de computadora realizan funciones útiles del mundo real. No tienen que ser 100% correctos para hacer esto, y los altos estándares de corrección son bastante caros. Las pruebas solo son útiles si realmente prueban algo, por lo que omitir la parte '100% correcta' no es una opción para los matemáticos.

3. Las pruebas matemáticas están claramente definidas. Si una prueba es defectuosa, el autor ha cometido un error. Muchos errores en los programas de computadora ocurren porque los requisitos no se comunicaron correctamente o hay un problema de compatibilidad con algo de lo que el programador nunca ha oído hablar.

4. Muchos programas de computadora no pueden probarse como correctos. Podrían resolver problemas definidos informalmente como reconocer caras. O pueden ser como un software de predicción del mercado de valores y tener un objetivo formalmente definido, pero involucran demasiadas variables del mundo real.

Una gran parte de las matemáticas como actividad humana ha sido el desarrollo de lenguajes específicos de dominio en los que la verificación de pruebas es fácil para un humano.

La calidad de una prueba es inversamente proporcional a su longitud y complejidad. La longitud y la complejidad a menudo se reducen desarrollando una buena notación para describir la situación en cuestión sobre la que estamos haciendo una declaración, junto con los conceptos auxiliares que interactúan dentro de la prueba particular en consideración.

Este no es un proceso fácil, y la mayoría de las pruebas presenciadas por personas alejadas de la investigación se encuentran en campos matemáticos (como álgebra y análisis) que han tenido cientos, si no miles, de años durante los cuales la notación de ese campo ha tenido sido refinado hasta el punto en que el acto de escribir las pruebas se siente como una brisa.

Sin embargo, a la vanguardia de la investigación, particularmente si trabaja en problemas que no están en campos con notación bien establecida o bien desarrollada, apostaría a la dificultad de que incluso una prueba correcta se acerque a la dificultad de escribir un programa correcto. Esto se debe a que también tendría que escribir al mismo tiempo el análogo de un diseño de lenguaje de programación, entrenar su red neuronal para compilarlo correctamente, intentar escribir la prueba en eso, quedarse sin memoria, intentar optimizar el lenguaje, itera tu cerebro aprendiendo el idioma, vuelve a escribir la prueba, etc.

Para reiterar, creo que escribir pruebas correctas puede abordar la dificultad de escribir programas correctos en ciertas áreas de las matemáticas, pero esas áreas son necesariamente jóvenes y poco desarrolladas porque la noción misma de progreso en matemáticas está íntimamente ligada a la facilidad de la prueba. verificación.

Otra forma de redactar el punto que quiero destacar es que, al final del día, tanto los lenguajes de programación como las matemáticas están diseñados para que los programas de computadora y las pruebas, respectivamente, sean posibles de compilar. Es solo que la compilación de un programa de computadora se realiza en una computadora y garantiza la corrección sintáctica que generalmente tiene poco que ver con la corrección del programa en sí, mientras que "compilar" una prueba es realizada por un humano y garantiza la corrección sintáctica que es lo mismo que corrección de la prueba.

Honestamente, estás comparando manzanas y naranjas aquí. A prueba de fallas y sin errores no son lo mismo.

Si un programa compara los números 2y 3dice eso 2 is greater than 3, entonces podría deberse a una implementación defectuosa:

# Buggy implementation
function is_a_greater_than_b(a,b):
  return b > a

Sin embargo, el programa todavía está libre de fallas. Al comparar dos números ay b, siempre podrá decirle sib es más grande que el a. Simplemente no es lo que usted (el programador) debía pedirle a la computadora que hiciera.

a) Porque los programas de computadora son mucho más grandes que las pruebas de matemáticas

a.1) Creo que se usa más gente durante la escritura de programas informáticos complejos que durante la escritura de pruebas matemáticas. Significa que el margen de error es mayor.

b) Porque los CEO / Accionistas se preocupan más por el dinero que por corregir pequeños errores , mientras que usted (como desarrollador) tiene que hacer sus tareas para cumplir con algunos requisitos / plazos / demostraciones

c) Debido a que puedes ser programador sin un conocimiento "profundo" en comp sci, mientras tanto sería difícil hacerlo en matemáticas

Adicionalmente:

NASA:

Este software está libre de errores. Es perfecto, tan perfecto como lo han logrado los seres humanos. Considere estas estadísticas: las últimas tres versiones del programa, cada una de 420,000 líneas de largo, tuvieron solo un error cada una. Las últimas 11 versiones de este software tuvieron un total de 17 errores.

Aproveche la actualización del software para permitir que el transbordador navegue con satélites de posicionamiento global, un cambio que involucra solo el 1.5% del programa, o 6,366 líneas de código. Las especificaciones para ese cambio abarcan 2.500 páginas, un volumen más grueso que una guía telefónica. Las especificaciones para el programa actual llenan 30 volúmenes y corren 40,000 páginas.

https://www.fastcompany.com/28121/they-write-right-stuff

Niveles Básicos:

Para las matemáticas, tenemos:
2 + 3 = 5

Aprendí sobre eso cuando era muy, muy joven. Puedo ver los elementos más básicos: dos objetos y tres objetos. Excelente.

Para la programación de computadoras, la mayoría de las personas tienden a usar un lenguaje de alto nivel. Algunos lenguajes de alto nivel pueden incluso "compilarse" en uno de los lenguajes de alto nivel inferiores, como C. C puede traducirse al lenguaje ensamblador. El lenguaje ensamblador luego se convierte en código de máquina. Mucha gente piensa que la complejidad termina allí, pero no es así: las CPU modernas toman el código de la máquina como instrucciones, pero luego ejecutan "microcódigo" para ejecutar esas instrucciones.

Esto significa que, en el nivel más básico (que trata con las estructuras más simples), ahora estamos lidiando con un microcódigo, que está incrustado en el hardware y que la mayoría de los programadores ni siquiera usan directamente, ni actualizan. De hecho, no solo la mayoría de los programadores no tocan el microcódigo (0 niveles más altos que el microcódigo), la mayoría de los programadores no tocan el código de la máquina (1 nivel más alto que el microcódigo), ni siquiera el ensamblaje (2 niveles más altos que el microcódigo) ( excepto, tal vez, por un poco de entrenamiento formal durante la universidad). La mayoría de los programadores pasarán tiempo solo 3 o más niveles más altos.

Además, si nos fijamos en la Asamblea (que es el nivel más bajo que normalmente obtienen las personas), cada paso individual generalmente es comprensible para las personas que han recibido capacitación y tienen los recursos para interpretar ese paso. En este sentido, el ensamblaje es mucho más simple que un lenguaje de nivel superior. Sin embargo, el ensamblaje es tan simple que realizar tareas complejas, o incluso tareas mediocres, es muy tedioso. Los idiomas de nivel superior nos liberan de eso.

En una ley sobre "ingeniería inversa", un juez declaró que incluso si el código puede manejarse teóricamente un byte a la vez, los programas modernos involucran millones de bytes, por lo que algunos tipos de registros (como copias de código) deben hacerse solo para tal un esfuerzo por ser factible (Por lo tanto, el desarrollo interno no se consideró una violación de la regla generalizada de "no hacer copias" de la ley de derechos de autor). (Probablemente estoy pensando en hacer cartuchos Sega Genesis no autorizados, pero puedo estar pensando en algo que se dijo durante el caso de Game Genie. )

Modernización:

¿Ejecutas código destinado a 286s? ¿O ejecutas código de 64 bits?

Las matemáticas usan fundamentos que se extienden por milenios. Con las computadoras, las personas generalmente consideran que la inversión en algo que tiene dos décadas es un desperdicio inútil de recursos. Eso significa que las matemáticas pueden probarse mucho más a fondo.

Estándares de herramientas usadas:

Un amigo que tenía una capacitación en programación de computadoras más formal que yo me enseñó que no existe un compilador de C sin errores que cumpla con las especificaciones de C. Esto se debe a que el lenguaje C básicamente asume la posibilidad de usar memoria infinita con el propósito de una pila. Obviamente, un requisito tan imposible tuvo que ser desviado cuando la gente trató de hacer compiladores utilizables que funcionaran con máquinas reales que son un poco más finitas por naturaleza.

En la práctica, he descubierto que con JScript en Windows Script Host, he podido lograr mucho bien usando objetos. (Me gusta el entorno porque el conjunto de herramientas necesario para probar el nuevo código está integrado en las versiones modernas de Microsoft Windows). Al usar este entorno, descubrí que a veces no hay documentación fácil de encontrar sobre cómo funciona el objeto. Sin embargo, usar el objeto es tan beneficioso que lo hago de todos modos. Entonces, lo que haría es escribir código, que puede tener errores como un nido de avispas, y hacerlo en un entorno bien protegido donde pueda ver los efectos y aprender sobre los comportamientos del objeto mientras interactúo con él.

En otros casos, a veces solo después de haber descubierto cómo se comporta un objeto, descubrí que el objeto (incluido con el sistema operativo) tiene errores y que es un problema conocido que Microsoft ha decidido intencionalmente que no se solucionará .

En tales escenarios, ¿confío en OpenBSD, creado por programadores expertos que crean nuevos lanzamientos a tiempo, de manera regular (dos veces al año), con un famoso registro de seguridad de "solo dos agujeros remotos" en más de 10 años? (Incluso tienen parches de erratas para problemas menos graves). No, de ninguna manera. No confío en un producto con una calidad tan alta, porque estoy trabajando para una empresa que brinda soporte a empresas que suministran a las personas máquinas que usan Microsoft Windows, así que eso es en lo que mi código necesita trabajar.

La practicidad / usabilidad requiere que trabaje en las plataformas que la gente encuentra útiles, y esa es una plataforma que es famosa por su seguridad (a pesar de que se han realizado enormes mejoras desde los primeros días del milenio en que los productos de la misma compañía eran mucho peores) .

Resumen

Existen numerosas razones por las cuales la programación de computadoras es más propensa a errores, y eso es aceptado por la comunidad de usuarios de computadoras. De hecho, la mayoría del código está escrito en entornos que no tolerarán esfuerzos sin errores. (Algunas excepciones, como el desarrollo de protocolos de seguridad, pueden recibir un poco más de esfuerzo en este sentido). Además de las razones comúnmente pensadas de las empresas que no quieren invertir más dinero y pierden plazos artificiales para hacer felices a los clientes, existe el impacto de La marcha de la tecnología que simplemente establece que si pasa demasiado tiempo, estará trabajando en una plataforma obsoleta porque las cosas cambian significativamente dentro de una década.

De golpe, puedo recordar que me sorprendió lo cortas que eran algunas funciones muy útiles y populares, cuando vi un código fuente para strlen y strcpy. Por ejemplo, strlen puede haber sido algo así como "int strlen (char * x) {char y = x; while ( (y ++)); return (yx) -1;}"

Sin embargo, los programas informáticos típicos son mucho más largos que eso. Además, una gran cantidad de programación moderna utilizará otro código que puede probarse menos a fondo, o incluso se sabe que tiene errores. Los sistemas de hoy son mucho más elaborados de lo que se puede pensar fácilmente, excepto al descartar muchas de las minucias como "detalles manejados por niveles inferiores".

Esta complejidad obligatoria, y la certeza de trabajar con sistemas complejos e incluso incorrectos, hacen que la programación de computadoras sea mucho más verificable que muchas matemáticas donde las cosas tienden a reducirse a niveles mucho más simples.

Cuando desglosas las cosas en matemáticas, llegas a piezas individuales que los niños pueden entender. La mayoría de la gente confía en las matemáticas; al menos aritmética básica (o, al menos, contando).

Cuando realmente desglosas la programación de la computadora para ver lo que sucede debajo del capó, terminas con implementaciones rotas de estándares y códigos rotos que finalmente se ejecutan electrónicamente, y esa implementación física está solo un paso por debajo del microcódigo que la mayoría de los informáticos capacitados en universidades no usan No se atreva a tocar (si es que lo saben).

He hablado con algunos programadores que están en la universidad o recién graduados que se oponen directamente a la idea de que se puede escribir un código libre de errores. Han descartado la posibilidad, y aunque reconocen que algunos ejemplos impresionantes (que he podido mostrar) son algunos argumentos convincentes, consideran que tales muestras son trematodos raros no representativos, y aún descartan la posibilidad de poder contar en tener tales estándares más altos. (Una actitud muy, muy diferente a la base mucho más confiable que vemos en matemáticas).

Las pruebas matemáticas describen "qué" conocimiento y programas describen "cómo" conocimiento ".

Escribir programas es más complejo porque el programador tiene que razonar sobre todos los diferentes estados que pueden surgir y cómo el comportamiento del programa cambia como resultado. Las pruebas usan razonamiento categórico o categórico para probar cosas sobre otras definiciones.

La mayoría de los errores son causados ​​por procesos que entran en estados que el programador no anticipó. En un programa, generalmente tiene miles o, en un sistema grande, millones de posibles variables que no son datos estáticos, pero en realidad transforman la forma en que se ejecuta el programa. Todas estas interacciones juntas crean comportamientos imposibles de anticipar, especialmente en una computadora moderna donde hay capas de abstracción que cambian debajo de ti.

En una prueba, no hay estado cambiante. Las definiciones y los objetos de discusión son fijos. Probar requiere pensar en el problema en general y considerar muchos casos, pero esos casos están fijados por definiciones.