Por que escrever provas matemáticas é mais à prova de falhas do que escrever código de computador?

190

Percebi que acho muito mais fácil escrever provas matemáticas sem cometer erros do que escrever um programa de computador sem erros.

Parece que isso é algo mais difundido do que apenas minha experiência. A maioria das pessoas comete erros de software o tempo todo em sua programação e possui o compilador para dizer qual é o erro o tempo todo. Eu nunca ouvi falar de alguém que escreveu um grande programa de computador sem erros de uma só vez, e tinha total confiança de que seria sem erros. (De fato, quase nenhum programa é sem erros, mesmo muitos com alta depuração).

No entanto, as pessoas podem escrever artigos ou livros inteiros de provas matemáticas, sem que nenhum compilador lhes dê feedback de que cometeram um erro e, às vezes, sem receber feedback de outras pessoas.

Deixe-me ser claro. isso não quer dizer que as pessoas não cometam erros nas provas matemáticas, mas mesmo para matemáticos com pouca experiência, os erros geralmente não são tão problemáticos e podem ser resolvidos sem a ajuda de algum "oráculo externo", como um compilador apontando para o seu erro.

De fato, se esse não fosse o caso, a matemática dificilmente seria possível, parece-me.

Então, isso me levou a fazer a pergunta: o que há de tão diferente em escrever provas matemáticas sem falhas e em escrever códigos de computador sem falhas que o tornam para que o primeiro seja muito mais tratável que o segundo?

Pode-se dizer que é simplesmente o fato de as pessoas terem o "oráculo externo" de um compilador apontando-os para seus erros que torna os programadores preguiçosos, impedindo-os de fazer o que é necessário para escrever código rigorosamente. Essa visão significaria que, se eles não tivessem um compilador, seriam capazes de ser tão impecáveis ​​quanto os matemáticos.

Você pode achar isso persuasivo, mas com base na minha experiência em programação e anotação de provas matemáticas, parece-me intuitivamente que isso realmente não é explicação. Parece haver algo mais fundamentalmente diferente nos dois empreendimentos.

Meu pensamento inicial é que, o que pode ser a diferença, é que, para um matemático, uma prova correta exige apenas que cada passo lógico esteja correto. Se todas as etapas estiverem corretas, toda a prova estará correta. Por outro lado, para que um programa seja sem bugs, não apenas todas as linhas de código precisam estar corretas, mas sua relação com todas as outras linhas de código no programa também deve funcionar.

Em outras palavras, se a etapa em uma prova é correta, então a cometer um erro na etapa não vai atrapalhar passo nunca. Mas se uma linha do código for corretamente escrita, cometer um erro na linha influenciará o funcionamento da linha , de modo que sempre que escrevermos a linha , teremos que levar em consideração sua relação com todas as outras linhas. Podemos usar o encapsulamento e todas essas coisas para limitar isso, mas ele não pode ser removido completamente.Y X X Y X XXYXXYXX

Isso significa que o procedimento para verificar erros em uma prova matemática é essencialmente linear no número de etapas de prova, mas o procedimento para verificar erros no código de computador é essencialmente exponencial no número de linhas de código.

O que você acha?

Nota: Esta pergunta tem um grande número de respostas que exploram uma grande variedade de fatos e pontos de vista. Antes de responder, leia todos eles e responda apenas se tiver algo novo a adicionar. Respostas redundantes ou que não apóiam opiniões com fatos podem ser excluídas.

user56834
fonte
3
Você conhece provas de correção de programas, tanto em papel quanto mecanizadas em provadores de teoremas? Ambos existem e contradizem sua atualização. O que é verdade é que a programação normalmente ensinada tem pouco a ver com a programação com provas de correção.
Bluesorblade
76
Lembra-me de uma citação de Knuth, acho que "Cuidado com o código acima! Só provei que estava correto, nunca testei"
Hagen von Eitzen
Comentários não são para discussão prolongada; esta conversa foi movida para o bate-papo .
Gilles
7
Encontre uma prova matemática escrita à mão com 100 milhões de linhas e sem "bugs", e darei tudo o que tenho.
Davor
Programas funcionais podem ser muito mais fáceis de escrever do que provas, no entanto, assim que o estado chegar ... a dificuldade explode ...
aoeu256

Respostas:

226

Deixe-me oferecer uma razão e um equívoco como resposta à sua pergunta.

A principal razão pela qual é mais fácil escrever (aparentemente) provas matemáticas corretas é que elas são escritas em um nível muito alto. Suponha que você possa escrever um 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)

Seria muito mais difícil dar errado ao programar dessa maneira, pois a especificação do programa é muito mais sucinta do que sua implementação . De fato, todo programador que tenta converter pseudocódigo em código, especialmente em código eficiente, encontra esse grande abismo entre a idéia de um algoritmo e seus detalhes de implementação . As provas matemáticas concentram-se mais nas idéias e menos nos detalhes.

A verdadeira contrapartida do código para provas matemáticas são as provas auxiliadas por computador . São muito mais difíceis de desenvolver do que as provas textuais usuais, e muitas vezes descobrimos vários cantos ocultos que são "óbvios" para o leitor (que geralmente nem os notam), mas não tão óbvios para o computador. Além disso, como o computador só pode preencher lacunas relativamente pequenas no momento, as provas devem ser elaboradas a um nível tal que um humano que as leia sinta falta da floresta pelas árvores.

Um equívoco importante é que as provas matemáticas geralmente estão corretas. De fato, isso provavelmente é bastante otimista. É muito difícil escrever provas complicadas sem erros, e os papéis geralmente contêm erros. Talvez os casos recentes mais celebrados sejam a primeira tentativa de Wiles (um caso especial) do teorema da modularidade (que implica o último teorema de Fermat) e várias lacunas na classificação de grupos finitos simples, incluindo mais de 1000 páginas em grupos de quasitina que eram escrito 20 anos após a classificação ter sido supostamente concluída.

Um erro em um artigo de Voevodsky o fez duvidar tanto de provas escritas que ele começou a desenvolver a teoria dos tipos de homotopia , uma estrutura lógica útil para desenvolver formalmente a teoria da homotopia e, a partir de então, usou um computador para verificar todo o seu trabalho subsequente (pelo menos de acordo com o seu próprio admissão). Embora esta seja uma posição extrema (e atualmente impraticável), ainda é o caso que, ao usar um resultado, é preciso revisar a prova e verificar se ela está correta. Na minha área, existem alguns artigos que se sabe estarem errados, mas nunca foram retratados, cujo status é transmitido de boca em orelha entre os especialistas.

Yuval Filmus
fonte
Comentários não são para discussão prolongada; esta conversa foi movida para o bate-papo .
DW
11
É possível que, no futuro, os assistentes de prova sejam usados ​​para verificar seu código e a prova? Talvez seja a hora de aprender um Agda para você ? (Desculpe ...)
Alex Vong
3
@AlexVong Um problema disso é que escrever uma especificação formal para código não trivial (para que você possa verificar se o código realmente cumpre a especificação) é quase impossível. Por exemplo, você pode imaginar o quão complicada seria uma especificação formal para um navegador (incluindo toda a interação do usuário, todos os formatos e protocolos de arquivos suportados etc.)?
svick
2
@svick Você está certo, para a interação do usuário, às vezes nem é claro qual deve ser o comportamento certo. Portanto, devemos nos concentrar em algo com uma especificação formal adequada (por exemplo, prova, compilador).
Alex Vong
11
De fato. Isso também pode ser uma explicação do motivo pelo qual muitas pessoas consideram a codificação em idiomas de nível inferior muito mais entediante e menos divertida do que a codificação em linguagens abstratas de alto nível. Embora isso também possa diferir por pessoa, é claro (alguns podem até gostar de construir circuitos eletrônicos / de hardware de nível muito mais baixo do que escrever softwares executados neles? Além disso, o código de nível inferior ainda pode ser insubstituível em muitos casos e escrevê-lo bem pode ser uma habilidade / façanha escassa, digna de elogios por si só).
XJI
77

(Provavelmente, estou arriscando alguns votos negativos aqui, pois não tenho tempo / interesse em fazer disso uma resposta adequada, mas acho o texto citado (e o restante do artigo citado) abaixo bastante esclarecedor, considerando também que eles estão escritos por um matemático conhecido. Talvez eu possa melhorar a resposta mais tarde.)

A idéia, que suponho que não seja particularmente distinta da resposta existente, é que uma "prova" ou argumento se comunique com uma comunidade matemática, onde o objetivo é convencê-los de que os detalhes (tediosos) podem ser preenchidos, em princípio, para obter uma prova formal totalmente especificada - sem muitas vezes fazê-lo. Uma instância crítica disso é que você pode usar os teoremas existentes simplesmente declarando-os, mas a reutilização de código é muito mais desafiadora em geral. Considere também pequenos "bugs", que podem tornar completamente inútil um pedaço de código (por exemplo, SEGFAULTs), mas podem deixar um argumento matemático praticamente intacto (ou seja, se o erro puder ser contido sem o argumento desmoronar).

O padrão de correção e integridade necessário para que um programa de computador funcione é um par de ordens de magnitude superior ao padrão de provas válidas da comunidade matemática. No entanto, grandes programas de computador, mesmo quando foram escritos com muito cuidado e testados com muito cuidado, sempre parecem ter bugs. [...] A matemática enquanto praticamos é muito mais formalmente completa e precisa do que outras ciências, mas é muito menos formalmente completa e precisa para seu conteúdo do que os programas de computador. A diferença tem a ver não apenas com a quantidade de esforço: o tipo de esforço é qualitativamente diferente. Em grandes programas de computador, uma tremenda proporção de esforço deve ser gasta em inúmeros problemas de compatibilidade: garantir que todas as definições sejam consistentes, desenvolvendo "boas" estruturas de dados que possuem uma generalidade útil, mas não incômoda, decidindo sobre a generalidade "correta" para funções, etc. A proporção de energia gasta na parte operacional de um grande programa, distinta da parte contábil, é surpreendentemente pequena. Devido a problemas de compatibilidade que quase inevitavelmente aumentam de controle porque as definições "corretas" mudam à medida que a generalidade e a funcionalidade são adicionadas, os programas de computador geralmente precisam ser reescritos com frequência, geralmente do zero.

SOBRE A PROVA E O PROGRESSO EM MATEMÁTICA (pp. 9-10), de WILLIAM P. THURSTON https://arxiv.org/pdf/math/9404236.pdf

Omar
fonte
3
O ponto sobre "reutilização de código" é bastante apropriado. Traduzir uma longa prova do russo para o inglês exige muita digitação ; mas traduzir um grande programa de computador de, digamos, C ++ para Java, exige muita reflexão . Além disso, ressuscitar uma prova de 3000 anos em grego antigo é igualmente fácil; ressuscitar um programa de 30 anos no PL / 1 é tão difícil quanto difícil.
Quuxplusone
2
O exemplo do grego antigo também me fez perceber: programadores de computador usam uma grande quantidade de gírias e coloquialismos locais, como (void*)1e open('/dev/null'), que podem até não ser portáveis ​​entre diferentes subculturas, muito menos traduzíveis para o idioma de destino. (O leitor só precisa entender sua semântica aproximada em virtude de uma longa experiência.) Acho que as provas matemáticas contêm menos desse tipo de "gíria". Se uma prova usa uma palavra, seu significado universal real é suposto ser dedutível pelo leitor de alguma forma. Programas de computador nem têm significados universais!
Quuxplusone
11
+1, porque como construtivista , a presunção desenfreada de um distinto de um valor arbitrariamente grande me deixa louca. Isso sobe de uma falácia no nível de valor para uma falácia lógica quando os matemáticos começam a falar sobre séries infinitas e, em seguida, apresentam argumentos baseados nessas séries, efetuando um erro em pé de igualdade com uma falácia oculta . 000
Nat
@ Nat você pode elaborar? Eu não entendo.
Gregory Magarshak 01/01
@GregoryMagarshak Esta resposta demonstrou um caso em que supor que o infinito válido em construção em série leva a uma falácia, que eu descrevia como sendo essa falácia oculta00 (a versão " disfarçada " mais abaixo na Wikipedia seção). Um matemático clássico pode dizer que o erro foi assumir que uma série infinita converge, embora um construtivista descreva a falácia como uma presunção não qualificada do infinito.
Nat
55

Permita-me começar citando EW Dijkstra:

"A programação é um dos ramos mais difíceis da matemática aplicada; os matemáticos mais pobres devem continuar sendo matemáticos puros". (de EWD498)

Embora o que Dijkstra quis dizer com 'programação' seja um pouco diferente do uso atual, ainda há algum mérito nessa citação. As outras respostas já mencionaram que é permitido que o nível de abstração na matemática seja muito maior do que na programação, o que significa que podemos ignorar algumas partes complicadas, se desejarmos fazê-lo.

No entanto, acredito que isso é apenas uma consequência de uma diferença mais fundamental entre uma prova e um programa de computador, que é o seu objetivo .

O principal objetivo de uma prova matemática é, entre outros, convencer-se de que uma afirmação matemática é correta e, talvez ainda mais importante, alcançar entendimento . Portanto, você pode optar por trabalhar apenas no mundo matemático, onde tudo é criado para que a compreensão possa ser alcançada pelo design (embora alguns estudantes implorem para diferir ...) É exatamente isso que Dijkstra quis dizer com "matemáticos puros", aqueles que (quase) se preocupam apenas com fatos matemáticos e com a compreensão de suas propriedades.

Portanto, não se surpreenda que produzir provas corretas seja relativamente à prova de falhas: é o objetivo de todo o "exercício". (Ainda assim, isso não significa que erros não existem ou mal existem; errar é apenas humano, dizem eles)

Agora, se considerarmos a programação, qual é o nosso propósito? Na verdade, não buscamos entender, queremos algo que funcione . Mas quando algo "funciona"? Algo funciona quando criamos com sucesso algo que permite que uma máquina estranha conclua a tarefa que queremos que seja executada e, de preferência, bem rápido também.

Esta é, acredito, a diferença fundamental, pois significa que nosso objetivo não pode ser simplesmente declarado como um teorema que nosso programa "prova"; desejamos algo no mundo real (seja o que for), não algum artefato matemático. Isso significa que não podemos teoricamente alcançar nosso objetivo (embora a Dijkstra faça com que você o tente independentemente), pois devemos apaziguar a máquina, esperar que realmente saibamos qual tarefa queremos que ela realize e também que estejamos cientes de coisas que não foram consideradas, ainda que aconteçam de alguma forma.

Portanto, no final, não há outra maneira senão tentar e provavelmente falhar, consertar, falhar e tentar novamente até estarmos um pouco satisfeitos com o resultado.


Observe que sua hipótese de escrever provas sem falhas é mais simples do que programas sem falhas (que são de fato declarações diferentes, como @Ariel aponta) podem estar de fato errados, pois as provas geralmente são construídas por tentativa e erro em algum nível. Ainda assim, espero que isso lance alguma luz sobre a questão implícita: "Qual é realmente a diferença entre provar algum teorema e escrever um programa?" (À qual um observador descuidado da correspondência de Curry-Howard poderia dizer: "Nada!")


Como @wvxvw mencionado nos comentários, os seguintes parágrafos de 'notas sobre programação estruturada' (EWD249, página 21) são muito relevantes:

(...) Um programa nunca é um objetivo em si; o objetivo de um programa é evocar cálculos e o objetivo dos cálculos é estabelecer o efeito desejado. Embora o programa seja o produto final produzido pelo programador, os possíveis cálculos evocados por ele - cuja "criação" é deixada para a máquina! - são o verdadeiro assunto de seu ofício. Por exemplo, sempre que um programador declara que seu programa está correto, ele realmente faz uma afirmação sobre os cálculos que pode evocar.

(...) Em certo sentido, a criação de um programa é, portanto, mais difícil do que a criação de uma teoria matemática: tanto o programa quanto a teoria são objetos estruturados e atemporais. Mas, embora a teoria matemática faça sentido como está, o programa só faz sentido através de sua execução.

Lagarto discreto
fonte
2
Sou apenas um leigo; a que Dijkstra realmente se refere por "programação"?
Ovi
2
@Ovi Não tenho muita certeza, mas a principal diferença é que ele fala sobre resolver problemas algorítmicos (não triviais) mais do que tarefas de programação 'gerais', ou seja, ele certamente não está falando sobre algum programa CRUD que precisa conectar alguns arquiteturas ou outros componentes, etc. Mais na opinião de Dijkstra de programação podem ser vistos no existente esta resposta
Discreta lagarto
3
Voto positivo por citar Dijkstra, mas você escolheu o lugar errado! Ele escreveu muito sobre esse problema nos primeiros parágrafos da Programação Estruturada. Eu não gostaria de alterar sua resposta enviando uma citação diferente, mas espero que você inclua mais desse artigo na sua resposta!
wvxvw
@Ovi, meu palpite sobre sua pergunta é que a programação no tempo de Dijkstra significava mais frequentemente escrever código de montagem do que a era moderna das linguagens de alto nível. Da mesma forma, estou lendo a edição de 1974 do Mythical Man-Month, os conceitos ainda são atuais, mas as referências técnicas são assembler no nível de sistemas ou PL / I, muito diferente do que a maioria das pessoas pensa como programação hoje
JimLohse
46

Lamport fornece algumas bases para discordâncias sobre a prevalência de erros nas provas em Como escrever uma prova (páginas 8-9) :

Cerca de vinte anos atrás, decidi escrever uma prova do teorema de Schroeder-Bernstein para uma aula de matemática introdutória. A prova mais simples que encontrei foi no texto clássico de topologia geral de Kelley. Como Kelley estava escrevendo para um público mais sofisticado, tive que acrescentar muitas explicações à prova de meia página dele. Eu tinha escrito cinco páginas quando percebi que a prova de Kelley estava errada. Recentemente, eu queria ilustrar uma palestra sobre meu estilo de prova com uma prova incorreta convincente, então me virei para Kelley. Não consegui encontrar nada de errado com a prova dele; parecia obviamente correto! Ler e reler a prova me convenceram de que minha memória havia falhado, ou então eu era muito estúpido há vinte anos. Ainda assim, a prova de Kelley era curta e serviria como um bom exemplo, então comecei a reescrevê-la como uma prova estruturada.

... O estilo foi aplicado pela primeira vez a provas de teoremas comuns em um artigo que escrevi com Martin Abadi. Ele já havia escrito provas convencionais - provas que eram boas o suficiente para nos convencer e, presumivelmente, aos árbitros. Reescrevendo as provas em um estilo estruturado, descobrimos que quase todos tinham erros sérios, embora os teoremas estivessem corretos. Qualquer esperança de que provas incorretas não levem a teoremas incorretos foi destruída em nossa próxima colaboração. Repetidas vezes, fizemos uma conjectura e escrevemos um esboço de prova no quadro-negro - um esboço que poderia facilmente ser transformado em uma prova convencional convincente - apenas para descobrir, tentando escrever uma prova estruturada, que a conjectura era falsa. Desde então, nunca acreditei em um resultado sem uma prova cuidadosa e estruturada.

Alexey Romanov
fonte
6
Mesmo artigo: "Evidências anedóticas sugerem que até um terço de todos os trabalhos publicados em periódicos matemáticos contêm erros - não apenas erros menores, mas teoremas e provas incorretos". Bem, isso foi nos anos 90, mas hoje é diferente? Provavelmente, aqueles papéis existentes naqueles dias ainda existem e tudo se acumula ... Então, não estou totalmente convencido de que as provas matemáticas fornecidas nos papéis contenham menos erros.
MarkokraM
Anedota fascinante, mas não estou vendo que ela responda diretamente ou se envolva com a pergunta. Deseja editar sua resposta para responder mais diretamente à pergunta que foi feita? Você está argumentando que as provas matemáticas são tão defeituosas quanto escrever código de computador? Você tem mais evidências para isso que pode fornecer? Uma anedota ou duas realmente não demonstram isso, não é?
DW
@DW Eu envio uma mensagem de e-mail para Leslie se ele puder dar mais evidências para a reivindicação.
MarkokraM
3
@DW Leslie disse em sua resposta sincera que seu colega fez uma investigação com 51 provas publicadas na Math Reviews naquele momento. Na sua opinião, é mais do que anedótico, mas não é adequado para fortes evidências devido a vários fatos. O caso foi mais complicado porque ocorreram alguns erros nas provas porque usavam provas errôneas em artigos publicados anteriormente, etc. Seria um ótimo tópico de pesquisa, mas requer muito trabalho. Como verificar provas matemáticas programaticamente ainda é uma grande questão. Os aplicativos criados para assistência de prova interativa estão em estágios muito iniciais. Pelo menos a interface deles.
MarkokraM
@DW A anedota ou duas demonstra como uma prova matemática pode parecer "correta", mas na verdade não é correta. Para quem escreveu um algoritmo de computador complexo e fez uma prova matemática e tentou escrever um algoritmo de computador como uma prova matemática e depois descobriu como o "algoritmo" de alto nível é traído por muitos, muitos bugs nos detalhes, o resultado não é de todo surpreendente.
Yakk
39

Uma grande diferença é que os programas geralmente são escritos para operar com entradas, enquanto as provas matemáticas geralmente começam com um conjunto de axiomas e teoremas conhecidos anteriormente. Às vezes, é necessário cobrir vários casos de canto para obter uma prova suficientemente geral, mas os casos e sua resolução são explicitamente enumerados e o escopo do resultado é implicitamente restrito aos casos cobertos.

Compare isso com um programa de computador, que deve fornecer uma saída 'correta' para uma variedade de entradas possíveis. Raramente é possível enumerar todas as entradas e tentar todas elas. Pior ainda, suponha que o programa interaja com um ser humano e permita que sua contribuição modifique o funcionamento? Os seres humanos são notoriamente imprevisíveis e o número de entradas possíveis para um programa razoavelmente grande com interação humana cresce a um ritmo prodigioso. Você precisa tentar prever todas as diferentes maneiras em que um programa pode ser usado e tentar fazer com que todos esses casos de uso funcionem ou, pelo menos, falhem de uma maneira razoável, quando a falha é a única opção. E isso pressupõe que você saiba como deve funcionar em todos os casos obscuros de canto.

Finalmente, um programa grande não pode realmente ser comparado a uma única prova, mesmo que seja complexa. Um programa grande provavelmente é mais parecido com a coleta e a revisão de uma pequena biblioteca de literatura, algumas das quais podem ter erros que você precisa solucionar. Para programas mais na escala de uma única prova, que pode ser uma pequena implementação de algoritmo, digamos, engenheiros de software experientes podem concluí-los sem cometer erros, especialmente ao usar ferramentas modernas que evitam / resolvem erros triviais comuns (como erros de ortografia ), que são equivalentes aos problemas iniciais que você resolveria na revisão.

Dan Bryant
fonte
14
+1 no seu último parágrafo. Embora as provas matemáticas sejam, em princípio, construídas umas sobre as outras, geralmente o básico é bem compreendido, o analógico das bibliotecas de computadores (embora elas também tenham bugs ...), e a prova real não é muito longa. Por outro lado, o software do consumidor é longo e complicado e, portanto, tem muito mais oportunidades de falhar.
Yuval Filmus
6
Na prática, o outro problema do software de consumo é que o comportamento "correto" geralmente é mal definido de antemão e, portanto, o que costumava ser correto mais tarde se torna errado. Seria como tentar escrever uma prova apenas para descobrir que as pessoas decidiram mudar os axiomas. Você pode consertar isso na notação, certo?
Dan Bryant
2
@ DanBryant Essa situação acontece em matemática. Em particular, as definições dos termos mudam ao longo do tempo e, muitas vezes, são ambíguas mesmo quando são usadas. "Provas e refutações" de Imre Lakatos descreve isso com o termo "polígono". Uma coisa semelhante aconteceu com "função" e, em menor grau, "integral". Ainda hoje, "categoria" não é inequívoca e as provas e os teoremas podem falhar, dependendo do que exatamente você quer dizer.
Derek Elkins
25

Eles dizem que o problema com os computadores é que eles fazem exatamente o que você lhes diz.

Eu acho que isso pode ser uma das muitas razões.

Observe que, com um programa de computador, o gravador (você) é inteligente, mas o leitor (CPU) é burro.
Mas com uma prova matemática, o escritor (você) é esperto e o leitor (revisor) também é esperto.

Isso significa que você nunca pode se dar ao luxo de entrar em uma situação de "bem, você sabe o que eu quero dizer " com um computador. Ele faz exatamente o que você diz, sem conhecer suas intenções.

Por exemplo, digamos que este seja um passo em alguma prova:

x2+4x+3x+3=(x+1)(x+3)x+3=x+1

x2+4x+3x+3x=3

Mehrdad
fonte
3
Ótima resposta! exceto que, como computador, eu me oponho ao uso da palavra "desnecessariamente". ;) [Suponha que este foi apenas um passo em uma prova maior com o objetivo de provar que -xé composto. O fato de esta etapa estar errada quando -x = 3é altamente relevante para a correção da prova concluída!]
Quuxplusone
@Quuxplusone: = P
Mehrdad
Os computadores também podem usar regras simbólicas de matemática e regras não-determinísticas de reescrita, é que as linguagens que usamos como C ++ são de nível muito baixo e baseadas em tecnologia antiga (C tinha menos recursos do que o Algol 60, por exemplo). As únicas exceções são as linguagens de verificação / verificação como Idris / Agda, Lisp com solucionadores simbólicos e Mathematica. ja.wolframalpha.com/input/…
aoeu256 28/08
23

Uma questão que acho que não foi abordada na resposta de Yuval é que parece que você está comparando animais diferentes.

nn!

Verificar propriedades semânticas de programas é indecidível (teorema de Rice) e, analogamente, verificar se uma afirmação na lógica de predicados de primeira ordem é verdadeira também é indecidível. O ponto é que não há diferença real na dureza da maneira como você está encarando os problemas. Por outro lado, podemos raciocinar sobre propriedades sintáticas de programas (compiladores), e isso é análogo ao fato de podermos verificar provas. Os bugs (o código não faz o que eu quero) são semânticos, portanto, você deve compará-los com o equivalente correto.

Fortalecerei Yuval e direi que campos inteiros cresceram com a motivação de escrever provas matemáticas que podem ser escritas e verificadas em algum sistema formal; portanto, mesmo o processo de verificação não é nada trivial.

Ariel
fonte
18

O que há de tão diferente em escrever provas matemáticas sem falhas e em escrever códigos de computador sem falhas que a tornam tão mais tratável que a primeira?

Acredito que os principais motivos são a idempotência (fornece os mesmos resultados para as mesmas entradas) e imutabilidade (não muda).

E se uma prova matemática pudesse dar resultados diferentes se fosse lida na terça-feira ou quando o ano avançasse para 2000 a partir de 1999? E se parte de uma prova matemática fosse voltar algumas páginas, reescrever algumas linhas e recomeçar a partir desse ponto?

Tenho certeza de que essa prova seria quase tão propensa a erros quanto um segmento normal de código de computador.

Também vejo outros fatores secundários:

  1. Os matemáticos geralmente são muito mais instruídos antes de tentar escrever uma prova significativa / publicável. 1/4 dos desenvolvedores profissionais autônomos começaram a codificar há menos de 6 anos (consulte a pesquisa SO 2017 ), mas presumo que a maioria dos matemáticos tenha mais de uma década de ensino formal de matemática.
  2. As provas matemáticas raramente são realizadas no mesmo nível de escrutínio que o código de computador. Um único erro de digitação pode / interromperá um programa, mas dezenas de erros de digitação podem não ser suficientes para destruir o valor de uma prova (apenas sua legibilidade).
  3. O diabo está nos detalhes e o código do computador não pode pular detalhes. As provas são gratuitas para pular etapas que são consideradas simples / rotineiras. Existem alguns açúcares sintáticos disponíveis em idiomas modernos, mas estes são codificados e bastante limitados em comparação.
  4. A matemática é mais antiga e tem uma base / núcleo mais sólido. Certamente, há uma infinidade de subcampos novos e brilhantes em matemática, mas a maioria dos princípios básicos está em uso há décadas. Isso leva à estabilidade. Por outro lado, os programadores ainda discordam da metodologia básica de codificação (basta perguntar sobre o desenvolvimento Agile e sua taxa de adoção).
Jeutnarg
fonte
Vale a pena mencionar que o equivalente da 'indempotência' da programação é a pureza funcional , que é reconhecida e suportada em algumas linguagens como Haskell.
Pharap
12

Eu concordo com o que Yuval escreveu. Mas também tem uma resposta muito mais simples: na prática, os engenheiros de software nem mesmo tentam verificar a exatidão de seus programas, simplesmente não o fazem, nem mesmo escrevem as condições que definem quando o programa está correto.

Existem várias razões para isso. Uma é que a maioria dos engenheiros de software não tem a capacidade de formular problemas matematicamente, nem sabe como escrever provas de correção.

Outra é que definir condições de correção para um sistema de software complexo (especialmente um sistema distribuído) é uma tarefa muito difícil e demorada. Espera-se que eles tenham algo que parece funcionar em questão de semanas.

Outra razão é que a correção de um programa depende de muitos outros sistemas escritos por outros que, novamente, não possuem semântica clara. Existe uma lei da Hyrum que diz essencialmente que, se a sua biblioteca / serviço tiver um comportamento observável (não faz parte do contrato), alguém eventualmente dependerá. Isso significa essencialmente que a idéia de desenvolver software de forma modular com contratos claros como lemas em matemática não funciona na prática. Piora nos idiomas em que a reflexão é usada. Mesmo se um programa estiver correto hoje, poderá ser interrompido amanhã quando alguém fizer alguma refatoração trivial em uma de suas dependências.

Na prática, o que normalmente acontece é que eles têm testes. Os testes agem como o esperado do programa. Sempre que um novo bug é encontrado, eles adicionam testes para detectá-lo. Funciona até certo ponto, mas não é uma prova de correção.

Quando as pessoas não têm as habilidades necessárias para definir a correção, nem escrever programas corretos, nem se espera que o façam, e isso é bastante difícil, não é surpresa que os softwares não estejam corretos.

Mas observe também que, no final, em melhores lugares, a engenharia de software é feita pela revisão de código. Esse é o autor de um programa que precisa convencer pelo menos uma outra pessoa de que o programa funciona corretamente. É nesse ponto que são apresentados alguns argumentos informais de alto nível. Mas, novamente, normalmente nada acontece perto de uma definição rigorosa clara de correção ou prova de correção.

Em matemática, as pessoas estão focadas na correção. No desenvolvimento de software, há muitas coisas com as quais um programador precisa se preocupar e há trocas entre eles. Ter um software livre de bugs ou até mesmo uma boa definição de correção (com os requisitos mudando ao longo do tempo) é o ideal, mas deve ser negociado com outros fatores e um dos mais importantes entre eles é o tempo gasto no desenvolvimento por meio da aplicação existente. desenvolvedores. Portanto, na prática, em melhores lugares, a meta e os processos estão mitigando o risco de erros, tanto quanto possível, em vez de tornar o software livre de erros.

Kaveh
fonte
Na verdade, não tenho certeza de quem está em pior situação entre programadores e matemáticos ao formular formalmente (ou seja, de maneira verificada pela máquina) formular especificações de correção e provar o código correto para, por exemplo, um programa de 10KLOC ou maior. Por um lado, você está completamente certo de que a maioria dos programadores não possui habilidades de prova de teoremas bem desenvolvidas. Por outro lado, grandes provas formais são como grandes programas e requerem essencialmente habilidades de engenharia de software para serem gerenciadas. Estou completamente confiante de que qualquer prova informal de correção para esse programa não teria esperança de estar certa.
Derek Elkins
Talvez. De qualquer forma, e apenas para esclarecer, não estou levando em conta provas formais em minha resposta, apenas provas informais no nível que vemos dizer nos documentos de algoritmos.
Kaveh
11

Já existem muitas respostas boas, mas ainda há mais razões pelas quais matemática e programação não são as mesmas.

1 As provas matemáticas tendem a ser muito mais simples que os programas de computador. Considere os primeiros passos de uma prova hipotética:

Seja um inteiro

Seja b um inteiro

Seja c = a + b

Até agora, a prova está boa. Vamos transformar isso nos primeiros passos de um programa semelhante:

Seja a = input ();

Seja b = input ();

Seja c = a + b;

Já temos uma infinidade de problemas. Supondo que o usuário realmente inseriu um número inteiro, precisamos verificar os limites. É um maior do que -32768 (ou qualquer que seja o min int em seu sistema é)? É um menos de 32767? Agora temos que verificar a mesma coisa para b . E porque nós adicionamos um e b o programa não está correto, a menos que a + bé maior que -32768 e menor que 32767. Essas são 5 condições separadas que um programador precisa se preocupar com o que um matemático pode ignorar. O programador não apenas precisa se preocupar com eles, mas também precisa descobrir o que fazer quando uma dessas condições não for atendida e escrever um código para fazer o que ele decidir que é a maneira de lidar com essas condições. A matemática é simples. A programação é difícil.

2 O questionador não diz se está se referindo a erros em tempo de compilação ou erros em tempo de execução, mas os programadores geralmente não se importam com erros em tempo de compilação. O compilador as encontra e é fácil de corrigir. Eles são como erros de digitação. Com que frequência as pessoas digitam vários parágrafos sem erros na primeira vez?

3 Treinamento.Desde tenra idade, somos ensinados a fazer matemática, e enfrentamos as consequências de pequenos erros repetidamente. Um matemático treinado teve que começar a resolver problemas de álgebra em várias etapas, geralmente no ensino médio e teve que fazer dezenas (ou mais) desses problemas toda semana, durante um ano. Um único sinal negativo descartado fez com que todo um problema estivesse errado. Após a álgebra, os problemas ficaram mais longos e mais difíceis. Os programadores, por outro lado, geralmente têm muito menos treinamento formal. Muitos são autodidatas (pelo menos inicialmente) e não receberam treinamento formal até a universidade. Mesmo no nível universitário, os programadores precisam fazer algumas aulas de matemática, enquanto os matemáticos provavelmente fazem uma ou duas aulas de programação.

Readin
fonte
10

Gosto da resposta de Yuval, mas queria discernir um pouco. Um motivo pelo qual você pode achar mais fácil escrever provas de matemática pode se resumir a quão ontológica matemática é platônica. Para entender o que quero dizer, considere o seguinte:

  • Funções em matemática são puras (todo o resultado da chamada de uma função é completamente encapsulado no valor de retorno, que é determinístico e calculado completamente a partir do valor de entrada).
  • A matemática não tem mutação ou reatribuição (quando você precisa modelar tais coisas, funções e sequências são usadas).
  • A matemática é referencialmente transparente (por exemplo, sem ponteiros, sem noção de chamada por nome vs chamada por valor) e objetos matemáticos possuem semântica de igualdade extensional (se "duas" coisas são iguais em todos os aspectos observáveis, então elas são de fato a mesma coisa).

Embora seja discutível se as restrições acima facilitam ou não a criação de um programa, acho que há amplo acordo de que as restrições acima facilitam o raciocínio sobre um programa. A principal coisa que você faz ao escrever uma prova de matemática é a razão da prova que está escrevendo atualmente (como, diferentemente da programação, você nunca precisa duplicar o esforço em matemática, pois as abstrações são gratuitas), por isso geralmente vale a pena insistir no acima das restrições.

Brice frito
fonte
7

As provas matemáticas fundamentais não equivalem a uma aplicação no mundo real, projetada para atender às necessidades de seres humanos vivos.

Os seres humanos mudarão seus desejos, necessidades e exigências no que é possivelmente uma base diária no campo dos programas de computador.

O que há de tão diferente em escrever provas matemáticas sem falhas e em escrever códigos de computador sem falhas que a tornam tão mais tratável que a primeira?

Com um requisito tão claro quanto um problema matemático, um programa sem falhas poderia ser escrito. Provar que o algoritmo de Dijkstra pode encontrar o caminho mais curto entre dois pontos em um gráfico não é o mesmo que implementar um programa que aceita entradas arbitrárias e encontrar os pontos mais curtos entre quaisquer dois pontos nele.

Existem preocupações de memória, desempenho e hardware a serem gerenciadas. Eu gostaria que não pudéssemos pensar sobre isso ao escrever algoritmos, que poderíamos usar construções puras e funcionais para gerenciar isso, mas os programas de computador vivem no mundo "real" do hardware, enquanto a prova matemática reside na ... "teoria".


Ou, para ser mais sucinto :

insira a descrição da imagem aqui

Félix Gagnon-Grenier
fonte
4

Olhando de outro ângulo, em um ambiente não acadêmico, muitas vezes se resume a dinheiro.

Como as outras postagens afirmam bem, Math é uma única especificação abstrata, portanto, uma prova precisa trabalhar consistentemente dentro dessa especificação para ser comprovada. Um programa de computador pode operar em muitas implementações da especificação abstrata da matemática - ou seja, a maneira como um idioma ou fabricante de hardware implementa a matemática de ponto flutuante pode ser um pouco diferente de outro, o que pode causar pequenas flutuações nos resultados.

Como tal, 'provar' um programa de computador antes de escrevê-lo envolveria provar a lógica no nível do hardware, nível do sistema operacional, nível do driver, linguagem de programação, compilador, talvez intérprete e assim por diante, para todas as combinações possíveis de hardware que o programa concebivelmente, pode ser executado e quaisquer dados concebíveis que possa ingerir. Você provavelmente encontrará esse nível de preparação e entendimento em missões espaciais, sistemas de armas ou sistemas de controle de energia nuclear, onde fracasso significa dezenas de bilhões de dólares perdidos e potencialmente muitas vidas perdidas, mas não muito mais.

Para o seu programador e / ou empresa "todos os dias", é muito, muito mais econômico aceitar um certo nível de precisão no código mais correto e vender um produto utilizável, e os desenvolvedores podem corrigir os erros retroativamente à medida que são descobertos durante o processo. uso.

navegador_
fonte
3
Você parece ter uma visão estreita do que é matemática e uma visão muito abrangente do que "prova" de um programa de computador implica. Você não precisa provar que todo o sistema está correto para provar que um programa está correto, basta provar que está correto, assumindo que os outros componentes atendam às especificações. Caso contrário, não é culpa do seu programa. Por outro lado, se o seu programa for interrompido porque depende de detalhes que não fazem parte da especificação desses componentes, por exemplo, variações de implementações da IEEE754, a culpa é sua.
Derek Elkins
Comentário justo. Provavelmente estou usando mal uma terminologia, pois não é minha formação acadêmica. Embora eu ache que assumir que outros componentes não tenham falhas não é uma coisa sábia, devido aos meus comentários anteriores.
Navigator_
4

Eu acho que seu raciocínio é válido, mas sua opinião não é. As provas matemáticas simplesmente não são mais tolerantes a falhas do que os programas, se ambas são escritas por humanos. Dijkstra já foi citado aqui, mas vou oferecer uma cotação adicional.

No entanto, devemos organizar os cálculos de forma que nossos poderes limitados sejam suficientes para garantir que o cálculo estabeleça o efeito desejado. Esta organização inclui a composição do programa e lá nos deparamos com o próximo problema de tamanho, viz. a extensão do texto do programa, e devemos dar a esse problema também reconhecimento explícito. Devemos permanecer cientes do fato de que a extensão em que podemos ler ou escrever um texto depende muito de seu tamanho. [...]

É com o mesmo humor que gostaria de chamar a atenção do leitor para o fato de que a "clareza" tem aspectos quantitativos pronunciados, fato que muitos matemáticos, curiosamente, parecem desconhecer. Um teorema que declara a validade de uma conclusão quando dez páginas cheias de condições são dificilmente uma ferramenta conveniente, pois todas as condições precisam ser verificadas sempre que o teorema for apelado. Na geometria euclidiana, o teorema de Pitágoras vale para quaisquer três pontos A, B e C, de modo que, através de A e C, uma linha reta pode ser desenhada ortogonal a uma linha reta através de B e C. Quantos matemáticos apreciam que o teorema permaneça aplicável quando alguns ou todos os pontos A, B e C coincidem? no entanto, isso parece em grande parte responsável pela conveniência com a qual o Teorema de Pitágoras pode ser usado.

Resumindo: como um ser humano de raciocínio lento, tenho uma cabeça muito pequena e é melhor aprender a conviver com ela e a respeitar minhas limitações e dar-lhes crédito total, em vez de tentar ignorá-las, pois o último esforço vã será punido pelo fracasso.

Isso é ligeiramente editado nos últimos três parágrafos do primeiro capítulo da Programação Estruturada de Dijkstra.

Talvez reformulando isso, aplique melhor à sua pergunta: a correção é em grande parte uma função do tamanho da sua prova. A correção de provas matemáticas longas é muito difícil de estabelecer (muitas "provas" publicadas vivem no limbo da incerteza, pois ninguém as verificou de fato). Mas, se você comparar a correção de programas triviais com provas triviais, provavelmente não haverá diferença perceptível. No entanto, os assistentes de prova automatizados (em um sentido mais amplo, seu compilador Java também é um assistente de prova), permitem que os programas vencam automatizando muitas bases.

wvxvw
fonte
O que você quer dizer com "longas provas matemáticas"? A prova do teorema menor do gráfico é bastante longa, mas não é realmente contestada por ninguém. O teorema de Feit-Thompson tem uma prova bastante longa, mas nunca esteve realmente no limbo. Como você compara os comprimentos das provas e programas? Número de palavras? Não há realmente diferenças visíveis entre provas e programas quando você compara provas e programas de complexidade semelhante (duração)?
Yuval Filmus
@YuvalFilmus como na citação: dez páginas de afirmações são longas para os seres humanos. Como julgo a duração de um programa? Bem, Dikstra ofereceu uma métrica: o comprimento do seu texto. Eu acho que pode ser muito simplista, mas é uma boa heurística, no entanto. Há outros, métricas mais interessantes, como, por exemplo, a complexidade ciclomática
wvxvw
3

Como outras respostas abordaram suas respostas (desejo elaborar), mas grande parte do problema é o uso da biblioteca. Mesmo com a documentação perfeita (tão comum quanto o código sem erros), é impossível transferir o conhecimento completo de uma biblioteca para todos os programadores que usam a biblioteca. Se o programador não entender perfeitamente sua biblioteca, ele poderá cometer erros ao usá-la. Às vezes, isso pode resultar em erros críticos descobertos quando o código não funciona. Mas para pequenos erros, eles podem passar despercebidos.

Uma situação semelhante seria se um matemático usasse provas e lemas existentes sem entendê-las completamente; suas próprias provas provavelmente seriam falhas. Embora isso possa sugerir que uma solução é aprender perfeitamente cada biblioteca que se usa; isso consome praticamente muito tempo e pode exigir conhecimento de domínio que o programador não possui (conheço muito pouco sobre seqüenciamento de DNA / síntese de proteínas; ainda assim, posso trabalhar com esses conceitos usando bibliotecas).

Em termos mais sucintos, a engenharia de software (engenharia em geral) baseia-se em encapsular diferentes níveis de abstração para permitir que as pessoas se concentrem em áreas menores do problema em que se especializam. Isso permite que as pessoas desenvolvam conhecimentos em sua área, mas também exige excelente comunicação entre cada camada. Quando essa comunicação não é perfeita, causa problemas.

user2138038
fonte
3
Espere, o que faz você pensar que os matemáticos "compreendem completamente" as provas e os lemas que eles usam? Não tenho certeza de que diferença entre matemáticos e programadores você está tentando demonstrar aqui.
Derek Elkins
3

Vou tentar ser original depois de todas essas ótimas respostas.

Programas são provas

O isomorfismo de Curry-Howard nos diz que os tipos no seu programa são os teoremas e o código real é a prova deles.

É certo que essa é uma visão muito abstrata e de alto nível. O problema que você provavelmente quer dizer é que escrever um código típico é mais difícil porque fica muito baixo. Na maioria dos casos, você "precisa informar à máquina o que fazer". Ou, analisando isso de outra maneira: os matemáticos são realmente bons em abstração.

Como nota lateral: "A música dos riachos" é uma das pontes mais bonitas entre os dois. Ele basicamente cria coisas para ser capaz de dizer "eu quero este em que maneira" ea máquina magicamente faz isso exatamente como desejado.

Oleg Lobachev
fonte
Não estou vendo totalmente se isso aborda a questão. O OP não deu nenhuma indicação de que eles estavam falando sobre linguagens de programação com sistemas de tipos poderosos, e acho que eles significam sistemas de tipos mais genéricos. Portanto, Curry-Howard é meio trivial neste caso.
6005
Eu sei que é um pouco rebuscado para C ou coisas semelhantes. Mas o que quero dizer é: a matemática está mais próxima do que um iniciante típico de CS imagina!
precisa
11
Parece que você é um "observador descuidado" do isomorfismo de Curry-Howards, ao qual me referi na minha resposta. Mesmo se tivermos um isomorfismo entre programas e provas, não se segue que o ato de escrever programas e escrever provas seja semelhante. De fato, pode até acontecer que todos os programas 'interessantes' ou 'típicos' não correspondam a uma prova típica e vice-versa.
Lagarto discreto
@Discretelizard Não é demonstrável que os programas "interessantes" não correspondam a uma "prova típica". Aqui está um exemplo em que pego a "prova típica" de alguém e produzo (esboço de) um programa inegavelmente interessante (algo intimamente relacionado à eliminação gaussiana). Equipado com tipos adequadamente precisos, acho que a maioria dos programas "interessantes" seriam lemas ou teoremas úteis, mas muitas provas (construtivas) não têm significado computacional real - elas estão apenas verificando condições colaterais - embora muitas o façam.
Derek Elkins
3

Nenhuma das muitas outras respostas aponta o seguinte. As provas matemáticas operam em sistemas de computação imaginária que têm memória infinita e poder computacional infinito. Portanto, eles podem manter números arbitrariamente grandes com precisão infinita e não perder precisão em nenhum cálculo.

π

crobar
fonte
2
"As provas matemáticas operam em sistemas de computação imaginária que têm memória infinita e poder computacional infinito". A maioria das provas matemáticas 'opera' em sistemas algébricos formais, por exemplo, os números reais (onde temos 'precisão infinita'). Isso também pode ser feito em programas: existem os chamados sistemas de álgebra computacional (CAS) que fazem exatamente isso! Além disso, campos inteiros da matemática estão preocupados com o fato de que não podemos representar todos os números reais exatamente como números finitos de ponto flutuante. Eu acho que você está fazendo uma distinção entre matemática e programação onde não há.
Lagarto discreto
11
@Discretelizard, sim, existem pacotes especiais com precisão arbitrária, mas mesmo assim, a memória disponível limitará a precisão real alcançável. Também são pacotes especiais . Apenas uma pequena proporção da programação é feita com esses pacotes, e principalmente em um ambiente acadêmico.
Croc #
π
@ Discretelizard, acho que meu argumento ainda permanece, a maioria dos programadores não está usando esses sistemas CAS. Eles são muito lentos para a programação do mundo real. A maioria da programação envolve fundamentalmente operações em números de precisão limitados. Os principais idiomas são C, C ++, Python, Java etc. Nenhum usa a representação no estilo CAS por padrão (embora os pacotes para isso possam ser criados neles). Seu contra-exemplo é um pequeno subconjunto de nicho de linguagens / sistemas de computador.
Croc
2
@crobar O problema com a sua resposta é que a grande maioria dos erros detectados não se deve a erros de ponto flutuante ou a estouros de números inteiros (embora esses contribuam com um número decente e esses aspectos definitivamente tornem a correção total de um programa muito mais improvável). Você poderia, no entanto, alegar de maneira mais genérica que os matemáticos carecem de muitas das preocupações dos programadores, como desempenho, tempo de colocação no mercado, manutenção e capacidade limitada de alterar os requisitos, se eles forem muito desafiadores.
Drek Elkins
3

Não é. As provas matemáticas são exatamente tão problemáticas por natureza, mas seus leitores são mais permissivos que um compilador. Da mesma forma, os leitores de um programa de computador são facilmente enganados e acreditam que ele está correto, pelo menos até tentarem executá-lo.

Por exemplo, se tentarmos traduzir uma prova matemática em um idioma formal como o ZFC, ele também conterá bugs. Isso ocorre porque essas provas podem ficar muito longas, então somos forçados a escrever um programa para gerar a prova. Poucas pessoas se arriscam, por sua conta e risco, embora haja pesquisas ativas na formalização de provas fundamentais.

E, de fato, a matemática pode ter BSOD! Não seria a primeira vez!

insira a descrição da imagem aqui

Essa idéia ortodoxa de que todas as provas matemáticas que foram suficientemente verificadas são essencialmente corretas ou podem ser corrigidas é a mesma que motivou seu projeto de software no trabalho: enquanto permanecermos no roteiro, obteremos todos os erros e as recursos completos - é um processo interativo que leva a um produto final definido.

Aqui está o outro lado. Olha, nós já temos o financiamento, validamos o conceito do negócio, todos os documentos estão aqui para você ler. Só precisamos que você execute e é uma coisa certa!

Também não sentimos muito por Hilbert , ele sabia no que estava se metendo. São apenas negócios.

Se você quer ter certeza, tome tudo caso a caso e tire suas próprias conclusões!

Dan Brumleve
fonte
3

Vejo duas razões importantes pelas quais os programas são mais propensos a erros do que as provas de matemática:

1: Os programas contêm variáveis ​​ou objetos dinâmicos que mudam ao longo do tempo, enquanto objetos matemáticos nas provas são normalmente estáticos. Assim, a notação em matemática pode ser usada como suporte direto ao raciocínio (e se a = b, esse ainda é o caso) em que isso não funciona em programas. Além disso, esse problema fica muito pior quando os programas são paralelos ou têm vários threads.

2: A matemática geralmente assume objetos definidos de maneira relativamente ordenada (gráficos, manifolds, anéis, grupos, etc.), enquanto a programação lida com objetos muito confusos e bastante irregulares: aritmética de precisão finita, pilhas finitas, conversões de caracteres inteiros, ponteiros, lixo que precisa de coleta , etc ... A coleta de condições relevantes para a correção é, portanto, muito difícil de lembrar.

René Ahn
fonte
3

Você deve distinguir duas "categorias" diferentes:

  • pseudo-provas (ou pseudo-código) - é o que você vê nos livros. Está escrito em linguagem natural (por exemplo, em inglês). É isso que você deve usar para aprender matemática (ou algoritmos).
  • provas formais (ou código formal) - você a escreve quando precisa que sua prova (ou código) seja mecanicamente verificável (ou executável). Essa representação não requer nenhuma "inteligência humana". Ele pode ser verificado (ou executado) mecanicamente, seguindo algumas etapas predefinidas (normalmente feitas pelos computadores hoje em dia).

Nós usamos pseudo-código há milhares de anos (por exemplo, algoritmo Euclides). Escrever código formal (em linguagens formais como C ou Java) tornou-se extremamente popular e útil após a invenção dos computadores. Infelizmente, porém, as provas formais (em idiomas formais como Principia Mathematica ou Metamath) não são muito populares. E como todo mundo escreve pseudo-provas hoje, as pessoas costumam discutir sobre novas provas. Os erros podem ser encontrados anos, décadas ou mesmo séculos após a "prova" real.

Ivan Kuckir
fonte
3

Não consigo encontrar a referência, mas acho que Tony Hoare disse uma vez algo do seguinte modo: A diferença entre verificar um programa e verificar uma prova é que uma prova pode ser verificada duas linhas por vez.

Em uma palavra: localidade.

As provas são escritas para que possam ser facilmente verificadas. Os programas são escritos para que possam ser executados. Por esse motivo, os programadores geralmente deixam de fora informações que seriam úteis para alguém que verifica o programa.

Considere este programa, onde x é somente leitura

    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)

É fácil de executar, mas difícil de verificar.

Mas se eu adicionar novamente as asserções ausentes, você poderá verificar o programa localmente, apenas verificando se cada sequência de atribuições está correta, com respeito às suas pré e pós-condições e que, para cada loop, a pós-condição do loop é implícita pelo invariável e a negação da proteção de loop.

    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)

Voltando à pergunta original: Por que escrever provas matemáticas é mais à prova de falhas do que escrever código de computador? Como as provas são projetadas para serem verificadas com facilidade por seus leitores, elas são verificadas com facilidade por seus autores e, portanto, os autores de alertas tendem a não cometer (ou pelo menos manter) erros lógicos em suas provas. Quando programamos, geralmente deixamos de escrever o motivo pelo qual nosso código está correto; o resultado é que é difícil para os leitores e o autor de um programa verificar o código; o resultado é que os autores cometem (e depois mantêm) erros.

Mas há esperança. Se, quando escrevemos um programa, também escrevemos a razão pela qual achamos que o programa está correto, podemos verificar o código enquanto o escrevemos e, assim, escrever menos código de buggy. Isso também tem o benefício de que outras pessoas possam ler nosso código e verificar por si mesmos.

Theodore Norvell
fonte
2

Poderíamos perguntar se é mais difícil na prática , ou em princípio , escrever provas ou escrever código.

Na prática, provar é muito mais difícil do que codificar. Muito poucas pessoas que fizeram dois anos de matemática em nível universitário podem escrever provas, mesmo que triviais. Entre as pessoas que cursaram dois anos no ensino médio, provavelmente pelo menos 30% podem resolver o FizzBuzz .

Mas, em princípio , existem razões fundamentais pelas quais é o contrário. As provas podem, pelo menos em princípio, ser verificadas quanto à correção através de um processo que não requer julgamento ou entendimento. Os programas não podem - nem podemos dizer, através de qualquer processo prescrito, se um programa será interrompido.

Ben Crowell
fonte
3
Dois anos de matemática em nível de faculdade não significam dois anos focados em escrever provas (ou gastar algum tempo escrevendo provas). Dito isso, minha impressão é que é comum que as aulas de geometria do ensino médio / início do ensino médio incluam provas; portanto, aparentemente, podemos esperar que mesmo com 13 anos de idade seja capaz de escrever provas simples com menos de um ano escolar no ensino médio. tema. Os cálculos algébricos passo a passo também são essencialmente provas. Eu acho que você está colocando a fasquia de "trivial" para programar muito baixo e provar muito alto.
Derek Elkins
3
Poderíamos escrever programas da mesma maneira. Você pode imaginar um requisito de que toda função / procedimento que você escreve deve fornecer uma especificação formal e uma prova (em Coq, digamos) de que ela atende à especificação. Existem, então, maneiras de verificar se a prova está correta de uma maneira que não requer julgamento ou entendimento.
DW
@ DW: Você está assumindo que (1) o comportamento desejado pode ser totalmente especificado em todos os casos, (2) existe a prova necessária (ou seja, o problema não é indecidível) e (3) se a prova existe, então pode encontrá-lo. Eu acho que todas essas três suposições são falsas em pelo menos alguns casos (provavelmente quase todos). Re 3, observe que, embora algumas provas possam ser fáceis, muitas são muito difíceis de encontrar.
Ben Crowell
@DerekElkins: Minha afirmação de que pouquíssimos estudantes universitários podem escrever provas triviais se baseia em minha própria experiência com meus alunos. Isso é em uma faculdade comunitária, então YMMV. O fato de algumas aulas de geometria do ensino médio incluírem uma dose pesada de prova de prova não se traduz no fato de que todos os estudantes universitários podem escrever provas. Eles também devem saber como fazer álgebra básica, mas na minha escola cerca de metade dos alunos de calouros não pode - o que ajuda a explicar por que tantos falham.
precisa
Essa seria uma boa explicação para adicionar à resposta, para explicar por que você não pode adotar a mesma abordagem para verificar se o programa está correto. Geralmente (2) e (3) raramente são um problema, seja na prática ou em princípio (se você não pode provar o programa correto, escrever de uma maneira diferente até que você pode provar isso correto). No entanto, o seu (1) é um ponto importante, e acho que isso fortaleceria a resposta para explicar por que isso dificulta a mesma coisa para os programas que fazemos para as provas.
DW
2

Apenas uma pequena porção de afirmações matemáticas verdadeiras pode ser praticamente comprovada. Mais significativamente, seria impossível construir um conjunto não-trivial (*) de axiomas matemáticos que permitiriam a comprovação de todas as afirmações verdadeiras. Se alguém precisasse escrever programas para fazer uma pequena fração do que poderia ser feito com computadores, seria possível escrever um software comprovadamente correto, mas os computadores são frequentemente chamados a fazer coisas além do alcance do que é comprovadamente correto software pode realizar.

(*) É possível definir um conjunto de axiomas que permitiriam que todas as afirmações verdadeiras fossem enumeradas e, portanto, comprovadas, mas essas geralmente não são muito interessantes. Embora seja possível categorizar formalmente conjuntos de axiomas naqueles que são ou não, relativamente falando, não triviais, o ponto principal é que a existência provável de declarações verdadeiras, mas que não podem ser comprovadas, não é uma falha em um conjunto. de axiomas. A adição de axiomas para tornar prováveis ​​quaisquer declarações verdadeiras, mas não prováveis, faria com que outras declarações se tornassem verdadeiras, mas sem elas serem prováveis.

supercat
fonte
11
"Apenas uma pequena porção de afirmações matemáticas que são verdadeiras pode ser praticamente comprovada." - Como você está medindo a "porção"? Isso está sob alguma distribuição de probabilidade? Você tem evidências para apoiar esta afirmação?
DW
"os computadores costumam fazer coisas além do que o software comprovadamente correto pode realizar". - Você tem alguma evidência disso? Você tem um exemplo? Você está reivindicando "além do que, em princípio, pode ser provado correto" ou "além do que podemos razoavelmente imaginar provar na prática"?
DW
@DW: Se X e Y são declarações ortogonais verdadeiras, mas não prováveis, então, para cada declaração provável P, haverá pelo menos duas declarações ortogonais (P e X) e (P e Y) verdadeiras, mas não prováveis. -demonstrável. Ao lidar com conjuntos infinitos, essa lógica não prova necessariamente nada, pois é possível usar uma lógica semelhante para mostrar que existem duas vezes mais números pares do que números ímpares, pois para cada número inteiro ímpar é possível identificar dois números pares (4x) e (4x + 2) que não estão associados a nenhum outro número ímpar, mas é claro que números pares e ímpares têm cardinalidade igual.
Super12 dez17
@DW: A frase "pequena porção" pode, portanto, realmente fazer sentido ao descrever a fração de afirmações verdadeiras que podem ser praticamente comprovadas, mas acho útil entender que a incapacidade de provar todas as afirmações verdadeiras não é uma "falha". Quanto aos computadores, muitos campos usam rotineiramente algoritmos com uma probabilidade de falha extremamente pequena, mas diferente de zero, e os ajustam para que a probabilidade seja aceitavelmente baixa (por exemplo, abaixo da do equipamento atingido por um meteoro). Em muitos casos, vários modos de falha não são independentes, no entanto, por isso pode ser essencialmente impossível ... #
308
... para determinar as probabilidades de diferentes combinações de falhas. Se alguém estimar a probabilidade de falha durante um período arbitrário de um minuto como sendo um em 10 ^ -500, pode-se perder centenas de ordens de magnitude e ainda ter um sistema confiável, mas se estiver 494 ordens de magnitude o sistema falharia uma vez a cada dois anos.
Supercat 12/12
2
  1. Programas de computador são testados no mundo real. Um erro técnico complicado em uma longa prova matemática, que apenas um número limitado de pessoas pode entender, tem uma boa chance de permanecer sem ser detectado. É provável que o mesmo tipo de erro em um produto de software produza um comportamento estranho que os usuários comuns percebem. Portanto, a premissa pode não estar correta.

  2. Programas de computador executam funções úteis do mundo real. Eles não precisam estar 100% corretos para fazer isso, e altos padrões de correção são bem caros. As provas só são úteis se elas realmente provarem algo; portanto, pular a parte '100% correta' não é uma opção para matemáticos.

  3. As provas matemáticas são claramente definidas. Se uma prova é falha, o autor cometeu um erro. Muitos bugs nos programas de computador ocorrem porque os requisitos não foram comunicados adequadamente ou há um problema de compatibilidade com algo que o programador nunca ouviu falar.

  4. Muitos programas de computador não podem ser provados corretos. Eles podem resolver problemas definidos informalmente, como reconhecer rostos. Ou podem ser como um software de previsão do mercado de ações e ter um objetivo formalmente definido, mas envolvem muitas variáveis ​​do mundo real.

James Hollis
fonte
2

Uma grande parte da matemática como atividade humana tem sido o desenvolvimento de linguagens específicas de domínio, nas quais a verificação de provas é fácil para um ser humano.

A qualidade de uma prova é inversamente proporcional ao seu comprimento e complexidade. O comprimento e a complexidade são frequentemente reduzidos pelo desenvolvimento de uma boa notação para descrever a situação em questão sobre a qual estamos fazendo uma declaração, juntamente com os conceitos auxiliares que interagem com a prova específica em consideração.

Este não é um processo fácil, e a maioria das provas testemunhadas por pessoas removidas da vanguarda da pesquisa ocorrem em campos matemáticos (como álgebra e análise) que tiveram centenas, senão milhares, de anos durante os quais a notação desse campo foi foi refinado até o ponto em que o ato de escrever as provas parece uma brisa.

No entanto, na vanguarda da pesquisa, principalmente se você trabalha com problemas que não estão em campos com notação bem estabelecida ou bem desenvolvida, eu apostaria a dificuldade de até escrever uma prova correta se aproxima da dificuldade de escrever um programa correto. Isso seria porque você também precisaria escrever o analógico de um projeto de linguagem de programação, treinar sua rede neural para compilá-la corretamente, tentar escrever a prova disso, ficar sem memória, tentar otimizar a linguagem, itere seu cérebro aprendendo o idioma, escreva a prova novamente etc.

Para reiterar, acho que escrever provas corretas pode abordar a dificuldade de escrever programas corretos em certas áreas da matemática, mas essas áreas são necessariamente jovens e pouco desenvolvidas porque a própria noção de progresso na matemática está intimamente ligada à facilidade da prova verificação.

Outra maneira de expressar o argumento que quero enfatizar é que as linguagens de programação e a matemática são projetadas no final do dia para que programas e provas de computador, respectivamente, sejam possíveis de compilar. É apenas que a compilação de um programa de computador é feita em um computador e garante a correção sintática, que geralmente tem pouco a ver com a correção do próprio programa, enquanto "compilar" uma prova é feita por um ser humano e garante a correção sintática, que é a mesma coisa que correção da prova.

Vladimir Sotirov
fonte
1

Você está honestamente comparando maçãs e laranjas aqui. À prova de falhas e sem erros não são a mesma coisa.

Se um programa compara os números 2e 3e diz que 2 is greater than 3, então ele poderia ser por causa de uma implementação de buggy:

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

O programa ainda está livre de falhas. Ao comparar dois números ae b, sempre será capaz de dizer se bé maior que o a. Não é apenas o que você (o programador) deveria pedir ao computador.

Arnab Datta
fonte
2
Qual é a sua definição de "falha" em um programa então?
user56834
0

a) Como os programas de computador são muito maiores que as provas de matemática

a.1) Acredito que há mais pessoas usadas durante a escrita de programas complexos do que na prova de matemática. Isso significa que a margem de erro é maior.

b) Como os CEOs / acionistas se preocupam mais com dinheiro do que com a correção de pequenos bugs , enquanto você (como desenvolvedor) precisa executar suas tarefas para atender a alguns requisitos / prazos / demonstrações

c) Como você pode ser programador sem conhecimento "profundo" em ciência da computação, enquanto isso seria difícil de fazer em matemática (acredito)

Além disso:

NASA:

Este software está livre de erros. É perfeito, tão perfeito quanto os seres humanos alcançaram. Considere estas estatísticas: as três últimas versões do programa - cada uma com 420.000 linhas - tiveram apenas um erro cada. As últimas 11 versões deste software apresentaram um total de 17 erros.

Faça a atualização do software para permitir que o ônibus navegue com os satélites de posicionamento global, uma alteração que envolve apenas 1,5% do programa, ou 6.366 linhas de código. As especificações para essa alteração executam 2.500 páginas, um volume mais grosso que uma lista telefônica. As especificações para o programa atual preenchem 30 volumes e executam 40.000 páginas.

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

Exeus
fonte
"programas de computador são muito maiores que provas de matemática" Isso depende do programa e da prova. E muito disso parece ser muito especulativo.
David Richerby
@DavidRicherby bem, eu tinha em mente coisas como o teorema de Last fermat e o Apollo da NASA github.com/chrislgarry/Apollo-11 math.wisc.edu/~boston/869.pdf - e nem estamos falando de sistemas operacionais e assim por diante.
Exeus
0

Níveis básicos:

Vejamos as coisas no nível mais simples e mais básico.

Para matemática, temos:
2 + 3 = 5

Eu aprendi sobre isso quando eu era muito, muito jovem. Eu posso olhar para os elementos mais básicos: dois objetos e três objetos. Ótimo.

Para programação de computadores, a maioria das pessoas costuma usar uma linguagem de alto nível. Alguns idiomas de alto nível podem até "compilar" em um dos idiomas de baixo nível, como C. C, que pode ser traduzido para o idioma Assembly. A linguagem assembly é então convertida em código de máquina. Muitas pessoas pensam que a complexidade termina aí, mas isso não acontece: as CPUs modernas tomam o código da máquina como instruções, mas depois executam o "microcódigo" para realmente executar essas instruções.

Isso significa que, no nível mais básico (lidando com as estruturas mais simples), agora estamos lidando com o microcódigo, embutido no hardware e que a maioria dos programadores nem usa diretamente, nem atualiza. De fato, não apenas a maioria dos programadores não toca no microcódigo (0 níveis acima do microcódigo), como também não toca no código da máquina (1 nível acima do microcódigo), nem no Assembly (2 níveis acima do microcódigo) ( exceto, talvez, por um pouco de treinamento formal durante a faculdade). A maioria dos programadores gastará tempo apenas 3 ou mais níveis acima.

Além disso, se olharmos para a Assembléia (que é o nível mais baixo que as pessoas normalmente obtêm), cada etapa individual é tipicamente compreensível por pessoas que foram treinadas e têm os recursos para interpretar essa etapa. Nesse sentido, o Assembly é muito mais simples que uma linguagem de nível superior. No entanto, o Assembly é tão simples que executar tarefas complexas, ou mesmo medíocres, é muito entediante. Os idiomas de nível superior nos libertam disso.

Em uma lei sobre "engenharia reversa", um juiz declarou que, mesmo que o código possa ser teoricamente manipulado um byte de cada vez, os programas modernos envolvem milhões de bytes; portanto, alguns tipos de registros (como cópias de código) devem ser feitos apenas para tais um esforço para ser viável. (Portanto, o desenvolvimento interno não foi considerado uma violação da regra generalizada de "não fazer cópias" da lei de direitos autorais.) (Provavelmente estou pensando em fabricar cartuchos não autorizados da Sega Genesis, mas talvez esteja pensando em algo dito durante o caso Game Genie. )

Modernização:

Você executa código destinado a 286s? Ou você executa o código de 64 bits?

A matemática usa fundamentos que remontam a milênios. Com computadores, as pessoas normalmente consideram o investimento em algo de duas décadas um desperdício inútil de recursos. Isso significa que a matemática pode ser muito mais completamente testada.

Padrões de ferramentas usadas:

Foi-me ensinado (por um amigo que tinha um treinamento mais formal em programação de computadores do que eu) que não existe um compilador C sem erros que atenda às especificações C. Isso ocorre porque a linguagem C basicamente assume a possibilidade de usar memória infinita para o propósito de uma pilha. Obviamente, um requisito tão impossível teve que ser desviado de quando as pessoas tentavam criar compiladores utilizáveis ​​que funcionavam com máquinas reais, que são um pouco mais finitas por natureza.

Na prática, descobri que, com o JScript no Windows Script Host, consegui realizar muitas coisas boas usando objetos. (Gosto do ambiente porque o conjunto de ferramentas necessário para experimentar o novo código está incorporado nas versões modernas do Microsoft Windows.) Ao usar esse ambiente, descobri que às vezes não há documentação facilmente localizável sobre como o objeto funciona. No entanto, usar o objeto é tão benéfico, que eu faço assim mesmo. Então, o que eu faria é escrever um código, que pode ser buggy como um ninho de vespas, e fazê-lo em um ambiente agradável em área restrita onde eu possa ver os efeitos e aprender sobre os comportamentos do objeto enquanto interage com ele.

Em outros casos, às vezes somente depois de descobrir como o objeto se comporta, descobri que o objeto (fornecido com o sistema operacional) é defeituoso e que é um problema conhecido que a Microsoft decidiu intencionalmente não será corrigido .

Em tais cenários, eu confio no OpenBSD, criado por programadores talentosos que criam novos lançamentos dentro do cronograma, regularmente (duas vezes por ano), com um famoso registro de segurança de "apenas dois buracos remotos" em mais de 10 anos? (Até eles têm patches de errata para problemas menos graves.) Não, de maneira alguma. Não confio em um produto com qualidade tão alta, porque estou trabalhando para uma empresa que oferece suporte a empresas que fornecem às pessoas máquinas que usam o Microsoft Windows, e é nisso que meu código precisa trabalhar.

A praticidade / usabilidade exige que eu trabalhe nas plataformas que as pessoas acham úteis, e essa é uma plataforma que é notoriamente ruim para a segurança (mesmo que enormes melhorias tenham sido feitas desde os primeiros dias do milênio em que os produtos da mesma empresa eram muito piores) .

Sumário

Existem inúmeras razões pelas quais a programação de computadores é mais suscetível a erros, e isso é aceito pela comunidade de usuários de computadores. De fato, a maioria dos códigos é escrita em ambientes que não toleram esforços sem erros. (Algumas exceções, como o desenvolvimento de protocolos de segurança, podem receber um pouco mais de esforço nesse sentido.) Além do pensamento comum de que as empresas não desejam investir mais dinheiro e perdem prazos artificiais para agradar os clientes, há o impacto de a marcha da tecnologia que simplesmente afirma que, se você gastar muito tempo, estará trabalhando em uma plataforma obsoleta, porque as coisas mudam significativamente em uma década.

Imediatamente, lembro-me de me surpreender com o quão curtas eram algumas funções muito úteis e populares, quando vi algum código fonte para strlen e strcpy. Por exemplo, strlen pode ter sido algo como "int strlen (char * x) {char y = x; while ( (y ++)); return (yx) -1;}"

No entanto, programas de computador típicos são muito mais longos que isso. Além disso, muita programação moderna usará outro código que pode ser testado menos detalhadamente, ou mesmo conhecido por ser buggy. Os sistemas atuais são muito mais elaborados do que aquilo que pode ser facilmente pensado, exceto afastando manualmente muitas das minúcias como "detalhes manipulados por níveis mais baixos".

Essa complexidade obrigatória e a certeza de trabalhar com sistemas complexos e até errados tornam a programação de computadores muito mais verificável do que muita matemática, onde as coisas tendem a se resumir a níveis muito mais simples.

Quando você divide as coisas em matemática, você começa a aprender peças individuais que as crianças podem entender. A maioria das pessoas confia na matemática; pelo menos aritmética básica (ou, pelo menos, contando).

Quando você realmente divide a programação de computadores para ver o que está acontecendo, acaba implementando padrões e códigos quebrados que são executados eletronicamente, e essa implementação física é apenas um passo abaixo do microcódigo que a maioria dos cientistas da computação ouse tocar (se eles estão cientes disso).

Conversei com alguns programadores que estão na faculdade ou recém-formados que objetam totalmente a noção de que código sem erros pode ser escrito. Eles descartaram a possibilidade e, embora reconheçam que alguns exemplos impressionantes (que pude mostrar) são alguns argumentos convincentes, eles consideram essas amostras raros casos não representativos e ainda descartam a possibilidade de poder contar. em ter padrões tão altos. (Uma atitude muito, muito diferente da fundamentação muito mais confiável que vemos na matemática.)

TOOGAM
fonte
11
Enquanto você faz um bom argumento para a complexidade da programação, você mal considera a matemática! De fato, você parece subestimar a complexidade envolvida na matemática formal: "Quando você divide as coisas em matemática, você obtém partes individuais que as crianças podem entender", sério ? Além disso, o mesmo poderia ser dito sobre a programação suficientemente 'de alto nível' (por exemplo, o Scratch é projetado para crianças). Observe também que, embora a especificação C completa não seja implementável, um compilador que suporte um subconjunto importante foi mostrado formalmente correto usando as provas assistidas por computador.
Lagarto discreto
2+3=5
Meta nota: se você é especialista em uma coisa e iniciante (ou inferior) em outra, está na pior posição possível para comparar as duas.
Raphael
Lagarto discreto - este é o Computer Science SE. Além disso, depois de ler outras respostas antes de postar, senti que elas tocavam muito mais a matemática do que os computadores. Eu senti que minha resposta era melhor, não demorando mais para adicionar palavras que seriam redundantes em grande parte com o que foi escrito em outro lugar. /// Quanto ao Scratch, alto nível é mais complexo, não mais simples (quando se olha para a perspectiva de entender completamente todas as partes móveis). Por essa perspectiva, o que eu estava escrevendo a partir, a montagem é mais simples do que zero em cima das outras camadas (com portas NAND eletrônicos mais simples até o momento)
TOOGAM
0

Provas matemáticas descrevem "o que" conhecimento e programas descrevem "como" conhecimento ".

Escrever programas é mais complexo porque o programador precisa raciocinar sobre todos os diferentes estados que podem surgir e como o comportamento do programa muda como resultado. As provas usam raciocínio fórmula ou categórico para provar coisas sobre outras definições.

A maioria dos erros é causada por processos que entram em estados que o programador não previu. Em um programa, você geralmente tem milhares ou, em um sistema grande, milhões de variáveis ​​possíveis que não são dados estáticos, mas que na verdade transformam a maneira como o programa é executado. Todas essas interações juntas criam comportamentos impossíveis de antecipar, especialmente em um computador moderno, onde há camadas de abstração mudando embaixo de você.

Em uma prova, não há mudança de estado. As definições e objetos de discussão são fixos. Provar exige pensar sobre o problema em geral e considerar muitos casos, mas esses casos são corrigidos por definições.

Justin Meiners
fonte
2
Eu diria que as provas matemáticas são totalmente capazes de descrever 'o que' conhecimento: faça, por exemplo, qualquer prova que construa um exemplo para provar a existência ou um método para calcular um valor. Ainda assim, concordo que estado é algo ausente nas provas, no sentido de que não há outro estado além daquele explicitamente descrito pelo autor (ou leitor!). É precisamente esse estado que permite que um programa faça algo que o leitor / autor desconhece, enquanto isso é impossível em uma prova. (com certeza, as provas podem ter características ou resultados indesejados, mas ainda há algum pensamento ativo necessário para obtê-las)
Lagarto discreto
@Discretelizard Este é um comentário útil. Eu acho que a linha entre o "quê" e o "como fazer" é certamente confusa. Provar que um algoritmo faz o que você pensa, realmente não está descrevendo "como fazer" em minha mente, apenas garantindo certas propriedades. Do ponto de vista filosófico, acho que o "como fazer" exige uma correspondência com o mundo. Os programas sempre fazem o que você lhes diz. Quando você tem um bug, o que você disse para fazer não correspondia ao mundo (o que você está modelando). A matemática, independente de uma aplicação (como problemas de física), parece ser totalmente dependente da coerência.
Justin Meiners