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 $X$$Y$$X$$X$$Y$$X$$X$

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.

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.

(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

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.

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.

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.

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:

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

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

$n$$n!$

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.

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

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.

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.

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.

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 :

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.

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.

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.

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.

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.

$\pi$

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!

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!

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.

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.

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.

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.

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.

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.

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.

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.

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

Níveis básicos:

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

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.