[FUG-BR] Primeiro sistema operacional 100% livre de erros está pronto

[Julião Braga]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

O Teorema da Parada, prova a indecidibilidade, para qualquer programa. É
um teorema. O Teorema de Goedel não é "meramente" matemático. É um
teorema! "Meramente" matemático é um termo novo para mim. Não sei o que
significa. Nem vou lhe pedir para explicar.

A referência a Goedel foi para lembrar da incompletude de sistemas
formais. Uma linguagem de programação é um sistema formal. Logo, a
linguagem de programação é incompleta. Portanto, cuidado quando usá-la.
A aritmética (ou a matemática) é incompleta, portanto, cuidado ao usá-la.

O Teorema da Parada, não me parece ser de Turing (Turing, provou que ele
não tem solução). Turing provou usando sua máquina (a famosa máquina de
Turing, importantíssima para os teóricos de complexidade de algorítmos).
Mostrou, na realidade que não se pode criar um procedimento efetivo (do
ponto de vista da Tese de Church). Provado, ele passou de uma
conjectura, para teorema.

Qual a visão prática de Goedel e Turing x o Teorema da Parada? Nenhum
progamador sério, pequeno, grande ou em equipe irá desenvolver programas
achando que ele estará correto. Um bom programador, pratica a humildade,
claro. E, leva em conta alguns colorários:

C1. Programar é difícil.
C2. Programar é uma arte.
C3. Não é possível desenvolver procedimentos automáticos para provar que
um programa está correto. (Os grandes "players" não são malucos.
Portanto, não gastam dinheiro procurando por isso. O que eles devem ter
é algo que indique com grande chance, que um programa "pode" estar
correto. Ou alguma ferramenta parecida.)
...
Cn. Outros.

Um pequeno programa é uma exceção. Algum programa (como esse que você
falou, talvez), com o espírito acadêmico (principalmente), pode tratar
exceções. O que não deixa de ter validade empírica, mesmo sabendo da
existência do Teorema da Parada.

Assim como Pitagoras, que achou a nossa conhecida solução para a**2 +
b**2 = c**2. Você iria tentar resolver a**n + b**n = c**n, para n=3,
sabendo que existe um Teorema (provado, em 1965) dizendo que qualquer
equação dessas para n >= 3, não tem solução?

Não fiz a abordagem com o objetivo de criar um debate acadêmico. Somente
para responder ao Davi.

[]s, Julião


Jean Everson Martina escreveu:
> Voce está misturando completamente as coisas. Os Teoremas de  
> imcompletude de Goedel não tem nada a ver com a história. Na verdade a  
> aplicação de Goedel é meramente matemática e em computação sua  
> aplicação é restrita teorema de parada de Touring. Mas o teorema de  
> parada também não se aplica nesse caso porque ele só trata se   
> programas com entrada nula tem ou não parada, o que não quer dizer que  
> todos os programas não tem parada. Existem programas que tem sim  
> parada garantida (estão corretos), por exemplo o Hello World que você  
> mencionou
> 
> Eu conheço (pessoalmente) o pessoal de New South Wales e o projeto  
> prova a decidibilidade de todas as entradas de todas as rotinas  
> implementadas pelo micro-kernel de forma indutiva. Voce pode verificar  
> a prova você mesmo, usando o Isabelle.
> 
> Pra finalizar, se o que você escreveu fosse verdade, a Intel, a  
> Nvidia, a Microsoft, a NSA americana e muitos outros players enormes  
> do mercado não poderiam usar usar provadores de teoremas pra garantir  
> decidibilidade.
> 
> Nas boas escolas de computação hoje, se ensina, além de lógica, também  
> semântica e provadores de teoremas. Pena que o Brasil está anos atras  
> em métodos formais aplicados.
> 
> 
> Jean
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.2.2 (MingW32)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iD8DBQFK5N/j0m/vNWbSX14RAufMAKCbQ0poH+CZyo5iA/QdfIer4mZL1ACgrbQM
8N7TnXBFgPK1RvFijiD5n8g=
=wcYB
-----END PGP SIGNATURE-----