¿Por qué escribir pruebas matemáticas es más a prueba de fallas que escribir código de computadora?

190

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.XYXXYXX

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.

usuario56834
fuente
3
¿Conoce las pruebas de corrección de los programas, tanto en papel como mecanizados en demostradores de teoremas? Ambos existen y contradicen su actualización. Es cierto que la programación como se enseña comúnmente tiene poco que ver con la programación con pruebas de corrección.
Blaisorblade
76
Me recuerda una cita de Knuth, creo que "¡Cuidado con el código anterior! Solo probé que era correcto, nunca lo probé"
Hagen von Eitzen
Los comentarios no son para discusión extendida; Esta conversación se ha movido al chat .
Gilles
77
Búscame una prueba matemática escrita a mano que tenga 100 millones de líneas y no tenga "errores", y te daré todo lo que tengo.
Davor
Los programas funcionales pueden ser mucho más fáciles de escribir que las pruebas, sin embargo, tan pronto como entra el estado ... la dificultad explota ...
aoeu256

Respuestas:

226

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.

Yuval Filmus
fuente
Los comentarios no son para discusión extendida; Esta conversación se ha movido al chat .
DW
1
¿Es posible que en el futuro se utilicen asistentes de prueba para verificar tanto el código como la prueba? Tal vez es hora de aprender un Agda ? (lo siento ...)
Alex Vong
3
@AlexVong Un problema con eso es que escribir una especificación formal para código no trivial (para que pueda verificar que el código realmente cumple con la especificación) es casi imposible. Por ejemplo, ¿te imaginas lo complicada que sería una especificación formal para un navegador (incluida toda la interacción del usuario, todos los formatos de archivo y protocolos compatibles, etc.)?
svick
2
@svick Tienes razón, para la interacción del usuario, a veces ni siquiera está claro cuál debería ser el comportamiento correcto. Por lo tanto, deberíamos centrarnos en algo con una especificación formal adecuada (por ejemplo, prueba, compilador).
Alex Vong
1
En efecto. Esa también podría ser una explicación de por qué muchas personas considerarían que la codificación en idiomas de nivel inferior es mucho más tediosa y menos divertida que la codificación en lenguajes abstractos de alto nivel. Aunque eso también puede diferir según la persona, por supuesto (algunos incluso podrían disfrutar construyendo circuitos electrónicos / hardware de muy bajo nivel más que escribiendo software que se ejecute en ellos. Además, el código de nivel inferior puede ser irremplazable en muchos casos y escribirlo bien puede ser una habilidad / hazaña escasa digna de mención por sí sola).
xji
77

(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

Omar
fuente
3
El punto sobre la "reutilización de código" es bastante apropiado. Traducir una larga prueba del ruso al inglés requiere bastante tipeo ; pero traducir un gran programa de computadora de, digamos, C ++ a Java, requiere bastante reflexión . Además, resucitar una prueba de 3000 años en griego antiguo es igual de fácil; Resucitar un programa de 30 años en PL / 1 es casi tan difícil o más difícil.
Quuxplusone
2
El ejemplo del griego antiguo también me hizo darme cuenta: los programadores de computadoras usan una tonelada de jerga local y coloquialismos, como (void*)1y open('/dev/null'), que ni siquiera pueden ser portátiles entre diferentes subculturas, y mucho menos traducibles al idioma de destino. (El lector solo tiene que asimilar su semántica aproximada a fuerza de una larga experiencia). Creo que las pruebas matemáticas contienen menos de este tipo de "jerga". Si una prueba usa una palabra, su significado universal real debe ser deducible por el lector de alguna manera. ¡Los programas de computadora ni siquiera tienen significados universales!
Quuxplusone
1
+1, porque como constructivista , la presunción desenfrenada de un distinto de un valor arbitrariamente grande me vuelve loco. Esto se eleva de una falacia de nivel de valor a una falacia lógica cuando los matemáticos comienzan a hablar de series infinitas y luego hacen argumentos basados ​​en esas series, produciendo un error a la par con un 0 oculto. falacia. 0 00 0
Nat
@ Nat, ¿puedes elaborar? No lo entiendo
Gregory Magarshak
@GregoryMagarshak Esta respuesta demostró un caso en el que asumir que el infinito es válido en la construcción de series conduce a una falacia, que describía como algo así como oculto- falacia0 00 0(laversión"disfrazada" más abajo en la sección de Wikipedia). Un matemático clásico podría decir que el error fue suponer que una serie infinita converge, aunque un constructivista describiría la falacia como una presunción incondicional del infinito.
Nat
55

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.

Lagarto discreto
fuente
2
Solo soy un laico; ¿A qué se refería realmente Dijkstra con "programación"?
Ovi
2
@Ovi No estoy exactamente seguro, pero la principal diferencia es que habla sobre la resolución de problemas algorítmicos (no triviales) más que las tareas de programación 'generales', es decir, ciertamente no está hablando de algún programa CRUD que necesite conectar algunos arquitecturas existentes u otros componentes, etc. Más información sobre la opinión de Dijkstra sobre programación se puede ver en esta respuesta
Lagarto discreto
3
¡Vota por citar a Dijkstra, pero elegiste el lugar equivocado! Ha escrito mucho sobre este problema en los primeros párrafos de Programación Estructurada. No quisiera alterar su respuesta enviando una cita diferente, ¡pero espero que considere agregar más de ese documento a su respuesta!
wvxvw
@Ovi, supongo que su pregunta es que programar en la época de Dijkstra más a menudo significaba escribir código de ensamblaje frente a la era moderna de los lenguajes de alto nivel. De manera similar, estoy leyendo la edición de 1974 de Mythical Man-Month, los conceptos aún están actualizados, pero las referencias técnicas son ensamblador a nivel de sistemas o PL / I, muy diferente de lo que la mayoría de la gente piensa que es la programación de hoy
JimLohse,
46

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.

Alexey Romanov
fuente
66
Mismo documento: "La evidencia anecdótica sugiere que hasta un tercio de todos los artículos publicados en revistas matemáticas contienen errores, no solo errores menores, sino teoremas y pruebas incorrectos". Bueno, eso fue en los 90, pero ¿es tan diferente hoy? Probablemente esos documentos existentes en esos días, todavía existen y todo se acumula ... Entonces, no estoy totalmente convencido de que las pruebas matemáticas proporcionadas en los documentos contengan menos errores.
MarkokraM
Anécdota fascinante, pero no veo que responda directamente o se involucre con la pregunta. ¿Desea editar su respuesta para responder más directamente a la pregunta que se le hizo? ¿Está argumentando que las pruebas matemáticas son tan defectuosas como escribir código de computadora? ¿Tiene más evidencia de eso que pueda proporcionar? Una anécdota o dos realmente no demuestran eso, ¿verdad?
DW
@DW Le envío un mensaje de correo electrónico a Leslie si él puede dar más pruebas de la reclamación.
MarkokraM
3
@DW Leslie dijo en su respuesta sincera que su colega realizó una investigación con 51 pruebas publicadas en Math Reviews en ese momento. En su opinión, es más que anecdótico, pero no apto para pruebas contundentes debido a varios hechos. El caso fue más complicado porque se produjeron algunos errores en las pruebas porque utilizaron pruebas erróneas en trabajos publicados anteriormente, etc. Sería un gran tema de investigación pero requiere mucho trabajo. Cómo verificar las pruebas de matemáticas mediante programación sigue siendo una gran pregunta. Las aplicaciones hechas para asistencia de prueba interactiva se encuentran en etapas muy tempranas. Al menos la interfaz de ellos.
MarkokraM
@DW La anécdota o dos demuestran cómo una prueba matemática puede parecer "correcta" pero en realidad no es sólida. Para cualquiera que haya escrito un algoritmo informático complejo y haya realizado una prueba matemática, e intente escribir un algoritmo informático como una prueba matemática y luego descubra cómo el "algoritmo" de alto nivel es traicionado por muchos, muchos errores en los detalles, el resultado No es sorprendente en absoluto.
Yakk
39

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.

Dan Bryant
fuente
14
+1 para tu último párrafo. Si bien las pruebas matemáticas en principio se construyen una encima de la otra, por lo general, los conceptos básicos son bien entendidos, el análogo de las bibliotecas de computadoras (aunque también tienen errores ...), y la prueba real no es demasiado larga. En contraste, el software de consumo es largo y complicado, y por lo tanto tiene muchas más oportunidades de fallar.
Yuval Filmus
66
En la práctica, el otro problema con el software del consumidor es que el comportamiento "correcto" a menudo está mal definido por adelantado y, por lo tanto, lo que solía ser correcto más tarde se vuelve incorrecto. Sería como tratar de escribir una prueba solo para descubrir que las personas han decidido cambiar los axiomas. Puedes arreglar eso en notación, ¿verdad?
Dan Bryant
2
@DanBryant Esa situación sucede en matemáticas. En particular, las definiciones de los términos cambian con el tiempo y, a menudo, son ambiguas incluso cuando se usan. "Pruebas y refutaciones" de Imre Lakatos describe esto con el término "polígono". Algo similar ha sucedido con "función" y, en menor medida, "integral". Incluso hoy en día, la "categoría" no es inequívoca y las pruebas y los teoremas pueden fallar dependiendo de a qué te refieres exactamente.
Derek Elkins
25

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:

X2+4 4X+3X+3=(X+1)(X+3)X+3=X+1

X2+4 4X+3X+3X=-3

Mehrdad
fuente
3
¡Gran respuesta! excepto que, como computadora, me opongo al uso de la palabra "innecesariamente". ;) [Supongamos que este fuera solo un paso en una prueba más grande con el objetivo de demostrar que -xes compuesto. ¡El hecho de que este paso es incorrecto cuando -x = 3es altamente relevante para la corrección de la prueba completa!]
Quuxplusone
@Quuxplusone: = P
Mehrdad
Las computadoras también pueden usar reglas simbólicas de reescritura matemática y no determinista, es solo que los lenguajes que usamos como C ++ son de muy bajo nivel y se basan en tecnología antigua (C tenía menos características que Algol 60, por ejemplo). Las únicas excepciones son los lenguajes de prueba / verificación como Idris / Agda, Lisp con solucionadores simbólicos y Mathematica. ja.wolframalpha.com/input/…
aoeu256
23

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

nortenorte!

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.

Ariel
fuente
18

¿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).
Jeutnarg
fuente
Vale la pena mencionar que el equivalente de programación de 'indempotencia' es la pureza funcional , que se reconoce y admite en algunos lenguajes como Haskell.
Pharap
12

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.

Kaveh
fuente
En realidad, no estoy seguro de quién está peor entre los programadores y los matemáticos al formular formalmente (es decir, de forma controlada por la máquina) la formulación de especificaciones de corrección y la prueba del código correcto para, por ejemplo, un programa 10KLOC o más grande. Por un lado, tiene toda la razón de que la mayoría de los programadores no tienen habilidades de demostración de teoremas bien desarrolladas. Por otro lado, las pruebas formales grandes son como programas grandes y requieren esencialmente habilidades de ingeniería de software para administrar. Estoy completamente seguro de que cualquier prueba informal de corrección para tal programa no tendría la esperanza de ser correcta.
Derek Elkins
Tal vez. En cualquier caso y solo para aclarar, no estoy tomando pruebas formales en mi respuesta, solo pruebas informales al nivel que vemos decir en los documentos de algoritmos.
Kaveh
11

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.

Readin
fuente
10

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.

Brice frito
fuente
7

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 :

ingrese la descripción de la imagen aquí

Félix Gagnon-Grenier
fuente
4

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.

navegador_
fuente
3
Parece tener una visión estrecha de lo que son las matemáticas y una visión demasiado amplia de lo que implica "probar" un programa de computadora. No necesita probar que todo el sistema es correcto para probar que un programa es correcto, solo necesita demostrar que es correcto asumiendo que los otros componentes cumplen con sus especificaciones. Si no lo hacen, no es culpa de su programa. Por otro lado, si su programa se rompe porque depende de detalles que no son parte de la especificación de esos componentes, por ejemplo, variaciones de implementaciones de IEEE754, entonces es su culpa.
Derek Elkins
Comentario justo Probablemente estoy haciendo un mal uso de alguna terminología ya que no es mi formación académica. Aunque creo que asumir que otros componentes son perfectos no es una buena idea, debido a mis comentarios anteriores.
navigator_
4

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.

wvxvw
fuente
¿Qué quieres decir con "largas pruebas matemáticas"? La prueba del teorema menor del gráfico es bastante larga, pero nadie lo discute realmente. El teorema de Feit-Thompson tiene una prueba bastante larga, pero nunca estuvo realmente en el limbo. ¿Cómo se compara la duración de las pruebas y los programas? ¿Número de palabras? ¿Realmente no hay diferencias notables entre las pruebas y los programas cuando se comparan pruebas y programas de complejidad (duración) similar?
Yuval Filmus
@YuvalFilmus, como en la cita: diez páginas de afirmaciones son largas para los humanos. ¿Cómo juzgo sobre la duración de un programa? Bueno, Dikstra ofreció una métrica: la longitud de su texto. Creo que puede ser demasiado simplista, pero sin embargo es una buena heurística. Hay otras métricas más interesantes, como, por ejemplo, la complejidad ciclomática
wvxvw
3

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.

usuario2138038
fuente
3
Espera, ¿qué te hace pensar que los matemáticos "entienden completamente" las pruebas y los lemas que usan? No estoy seguro de qué diferencia entre matemáticos y programadores está tratando de demostrar aquí.
Derek Elkins
3

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.

Oleg Lobachev
fuente
No estoy viendo totalmente si esto responde a la pregunta. El OP no dio ninguna indicación de que estaban hablando de lenguajes de programación con sistemas de tipos potentes, y creo que significan sistemas de tipos más genéricos. Entonces Curry-Howard es algo trivial en este caso.
6005
Sé que es un poco exagerado para C o cosas similares. Pero mi punto es: ¡las matemáticas están más cerca de lo que un principiante típico de CS podría pensar!
Oleg Lobachev
1
Parece que eres un "observador descuidado" del isomorfismo de Curry-Howards, al que me referí en mi respuesta. Incluso si tenemos un isomorfismo entre programas y pruebas, no se deduce que el acto de escribir programas y pruebas sea similar en absoluto. De hecho, incluso puede darse el caso de que todos los programas 'interesantes' o 'típicos' no correspondan a una prueba típica y viceversa.
Lagarto discreto
@Discretelizard No es demostrable que los programas "interesantes" no correspondan a una "prueba típica". Aquí hay un ejemplo en el que tomo la "prueba típica" de alguien y produzco un (bosquejo de) un programa innegablemente interesante (algo estrechamente relacionado con la eliminación gaussiana). Equipado con tipos adecuadamente precisos, creo que la mayoría de los programas "interesantes" serían lemas o teoremas útiles, pero muchas pruebas (constructivas) no tienen una importancia computacional real, solo están verificando las condiciones secundarias, aunque muchas sí.
Derek Elkins
3

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.

π

crobar
fuente
2
"Las pruebas matemáticas operan en sistemas informáticos imaginarios que tienen memoria infinita y potencia informática infinita". La mayoría de las pruebas matemáticas 'operan' en sistemas algebraicos formales, por ejemplo, los números reales (donde tenemos 'precisión infinita'). Esto también se puede hacer en programas: existen los llamados sistemas de álgebra computacional (CAS) que hacen precisamente esto. Además, campos completos de las matemáticas están relacionados con el hecho de que no podemos representar todos los números reales exactamente como números finitos de coma flotante. Creo que está haciendo una distinción entre matemáticas y programación donde no hay ninguna.
Lagarto discreto
1
@Discretelizard, sí, existen paquetes especiales con precisión arbitraria, pero incluso así, la memoria disponible limitará la precisión real alcanzable. También son paquetes especiales . Solo una pequeña proporción de la programación se realiza con dichos paquetes, y principalmente en un entorno académico.
crobar
π
@Discretelizard, creo que mi punto sigue en pie, la mayoría de los programadores no están utilizando dichos sistemas CAS. Son demasiado lentos para la programación del mundo real. La mayoría de la programación implica fundamentalmente operaciones con números de precisión limitados. Los lenguajes principales son C, C ++, Python, Java, etc. Ninguno usa la representación de estilo CAS por defecto (aunque los paquetes para hacer esto podrían crearse en ellos). Su contraejemplo es un pequeño subconjunto de idiomas / sistemas informáticos.
crobar
2
@crobar El problema con su respuesta es que la gran mayoría de los errores detectados no se deben a errores de coma flotante o desbordamientos de enteros (aunque estos contribuyen con un número decente, y esos aspectos definitivamente hacen que la corrección completa de un programa sea mucho más improbable). Sin embargo, podría hacer la afirmación más genérica de que los matemáticos carecen de muchas de las preocupaciones de los programadores, como el rendimiento, el tiempo de comercialización, la capacidad de mantenimiento y una capacidad limitada para cambiar los requisitos si resultan demasiado desafiantes.
Derek Elkins
3

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!

ingrese la descripción de la imagen aquí

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!

Dan Brumleve
fuente
3

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.

René Ahn
fuente
3

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.

Ivan Kuckir
fuente
3

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.

Theodore Norvell
fuente
2

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á.

Ben Crowell
fuente
3
Dos años de matemáticas de nivel universitario no significa dos años de pruebas se centró en la escritura (o gastar cualquier tiempo escribiendo pruebas). Dicho esto, mi impresión es que es común que los medianos clases de geometría / primeros de secundaria para incluir pruebas, por lo que aparentemente nos puede esperar incluso 13 años de edad para ser capaz de escribir pruebas sencillas, con menos de un año escolar de la educación en el tema. Los cálculos algebraicos paso a paso también son esencialmente pruebas. Creo que está poniendo el listón de "trivial" para programar demasiado bajo y para probar demasiado alto.
Derek Elkins
3
Podríamos escribir programas de la misma manera. Podría imaginar un requisito de que cada función / procedimiento que escriba tenga que proporcionar una especificación formal y una prueba (en Coq, por ejemplo) de que cumple con la especificación. Entonces hay formas de verificar que la prueba sea correcta de una manera que no requiera juicio o comprensión alguna.
DW
@DW: Está asumiendo que (1) el comportamiento deseado puede especificarse completamente en todos los casos, (2) existe la prueba necesaria (es decir, el problema no es indecidible) y (3) si la prueba existe, entonces Lo puedo encontrar. Creo que estos tres supuestos son falsos en al menos algunos casos (probablemente en casi todos los casos). Re 3, tenga en cuenta que aunque algunas pruebas pueden ser fáciles, muchas pruebas son muy difíciles de encontrar.
Ben Crowell
@DerekElkins: mi afirmación de que muy pocos estudiantes universitarios pueden escribir incluso pruebas triviales se basa en mi propia experiencia con mis estudiantes. Esto es en un colegio comunitario, así que YMMV. El hecho de que algunas clases de geometría de la escuela secundaria incluyan una gran dosis de redacción de pruebas no se traduce en el hecho de que todos los estudiantes universitarios pueden escribir pruebas. También se supone que saben hacer álgebra básica, pero en mi escuela aproximadamente la mitad de los estudiantes de primer año no pueden, lo que ayuda a explicar por qué tantos fracasan.
Ben Crowell
Esa sería una buena explicación para agregar a la respuesta, para explicar por qué no puede tomar el mismo enfoque para verificar que el programa sea correcto. En general, (2) y (3) rara vez son un problema, ya sea en la práctica o en principio (si no puede probar que el programa es correcto, escriba de una manera diferente hasta que pueda probar que es correcto). Sin embargo, su (1) es un punto importante, y creo que fortalecería la respuesta para explicar por qué eso dificulta hacer lo mismo para los programas que para las pruebas.
DW
2

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.

Super gato
fuente
1
"Solo una pequeña porción de las afirmaciones matemáticas que son verdaderas se puede probar prácticamente". - ¿Cómo estás midiendo "porción"? ¿Está esto bajo alguna distribución de probabilidad? ¿Tiene evidencia para apoyar esta declaración?
DW
"A menudo se pide a las computadoras que hagan cosas más allá del alcance de lo que puede lograr un software probablemente correcto". - ¿Tienes alguna evidencia de esto? ¿Tienes un ejemplo? ¿Está diciendo "más allá de lo que en principio se puede probar que es correcto" o "más allá de lo que razonablemente podemos imaginar probar en la práctica"?
DW
@DW: Si X e Y son declaraciones ortogonales que son verdaderas pero no demostrables, entonces, para cada declaración P demostrable, habrá al menos dos declaraciones ortogonales (P e X) e (P e Y) que son verdaderas pero no -demostrable. Cuando se trata de conjuntos infinitos, dicha lógica no necesariamente prueba nada, ya que uno podría usar una lógica similar para mostrar que hay el doble de enteros pares que de enteros impares, ya que por cada entero impar se pueden identificar dos enteros pares (4x) y (4x + 2) que no están asociados con ningún otro número entero impar, pero, por supuesto, los enteros pares e impares tienen la misma cardinalidad.
supercat
@DW: Por lo tanto, la frase "porción pequeña" solo puede tener sentido al describir la fracción de declaraciones verdaderas que pueden probarse de manera práctica, pero creo que es útil comprender que la incapacidad para probar todas las declaraciones verdaderas no es un "defecto". En cuanto a las computadoras, muchos campos usan rutinariamente algoritmos que tienen una probabilidad de falla extremadamente pequeña, pero no nula, y luego los ajustan para que la probabilidad sea aceptablemente baja (por ejemplo, por debajo del equipo golpeado por un meteorito). Sin embargo, en muchos casos, varios modos de falla no son independientes, por lo que puede ser esencialmente imposible ...
supercat
... para determinar las probabilidades de diferentes combinaciones de fallas. Si uno estima que la probabilidad de falla durante un período arbitrario de un minuto es de uno en 10 ^ -500, uno podría estar apagado por cientos de órdenes de magnitud y aún tener un sistema confiable, pero si uno está apagado por 494 órdenes de magnitud el sistema fallaría una vez cada dos años.
supercat
2
  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.

James Hollis
fuente
2

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.

Vladimir Sotirov
fuente
1

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.

Arnab Datta
fuente
2
¿Cuál es su definición de "falla" en un programa entonces?
user56834
0

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

Exeus
fuente
"los programas de computadora son mucho más grandes que las pruebas de matemáticas" Eso depende del programa y la prueba. Y gran parte de esto parece ser muy especulativo.
David Richerby
@DavidRicherby bueno, tenía en mente cosas como el teorema de Last Fermat y el Apollo de la NASA github.com/chrislgarry/Apollo-11 math.wisc.edu/~boston/869.pdf , y ni siquiera estamos hablando de sistemas operativos, etc.
Exeus
0

Niveles Básicos:

Veamos las cosas en el nivel más simple y básico.

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).

TOOGAM
fuente
1
Si bien presenta un buen argumento para la complejidad de la programación, ¡apenas considera las matemáticas! De hecho, parece subestimar la complejidad involucrada en las matemáticas formales: "¿Cuándo se descomponen las cosas en matemáticas, se llega a piezas individuales que los niños pueden entender", realmente ? Además, lo mismo podría decirse sobre una programación suficientemente 'de alto nivel' (por ejemplo, Scratch está diseñado para niños). También tenga en cuenta que aunque la especificación C completa no es implementable, un compilador que admite un subconjunto importante se ha demostrado formalmente correcto utilizando pruebas asistidas por computadora.
Lagarto discreto
Convenido. En una prueba de nivel de investigación, precisamente no verá algo en el nivel de2+3=5 5. En cambio, encontrará afirmaciones como "puede ser fácilmente probado por X", donde X tardó dos años en dominarlo; o "es una aplicación directa del teorema Y", donde Y tardó décadas y decenas de personas en probarse. Por supuesto, puede "compilar" cada trabajo de investigación sobre matemática / lógica formal elemental, encontrando miles de errores, estoy seguro, pero nadie se molesta en hacerlo . (Y no todo el mundo está de acuerdo en que eso es bueno y bien Así que unas pocas personas. No tratan de formalizar las matemáticas.)
Rafael
Meta nota: si eres un experto en una cosa y un principiante experto (o inferior) en otra, estás en la peor posición posible para comparar las dos.
Raphael
Lagarto discreto: este es el Computer Science SE. Además, después de haber leído otras respuestas antes de publicar, sentí que tocaban las matemáticas mucho más que las computadoras. Sentí que mi respuesta era mejor al no alargarme solo para agregar palabras que serían en gran medida redundantes con lo que estaba escrito en otra parte. /// En cuanto a Scratch, el nivel alto es más complejo, no más simple (cuando se observa la perspectiva de comprender completamente todas las partes móviles). Desde esta perspectiva, desde la que escribía, Assembly es más simple que Scratch en la parte superior de otras capas (con puertas NAND electrónicas aún más simples)
TOOGAM
0

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.

Justin Meiners
fuente
2
Diría que las pruebas matemáticas son totalmente capaces de describir el conocimiento de "qué": tome, por ejemplo, cualquier prueba que construya un ejemplo para demostrar la existencia o un método para calcular un valor. Aún así, estoy de acuerdo en que el estado es algo ausente en las pruebas, en el sentido de que no hay otro estado que el explícitamente descrito por el autor (o lector). Es precisamente este estado el que permite que un programa haga algo que el lector / autor desconoce, mientras que esto es imposible en una prueba. (claro, las pruebas pueden tener características o resultados no deseados, pero todavía se necesita algún pensamiento activo para obtenerlas)
Lagarto discreto
@Discretelizard Este es un comentario útil. Creo que la línea entre el "qué" y el "cómo" es ciertamente confusa. Probar un algoritmo hace lo que crees que hace, realmente no describe "cómo hacerlo" en mi mente, solo garantiza que ciertas propiedades se mantengan. Desde un punto de vista filosófico, creo que "cómo" el conocimiento requiere una correspondencia con el mundo. Los programas siempre hacen lo que les dices. Cuando tienes un error, lo que le dijiste que hiciera no correspondía con el mundo (lo que estás modelando). La matemática, independiente de una aplicación (como los problemas de física) parece depender de la coherencia.
Justin Meiners