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

[Jean Everson Martina]

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


On 25 Oct 2009, at 19:57, Julião Braga wrote:

> -----BEGIN PGP SIGNED MESSAGE-----
> Hash: SHA1
>
> Sim, existe um teorema. Chama-se Teorema da Parada. Associado à  
> máquina
> de Turing e ao Teorema de Goedel. Ele não aborda a questão de  
> corretude,
> que é outra coisa, mas prova que é impossível afirmar que um programa
> está 100% correto (mesmo um simples "Hello World", onde por trás tem  
> um
> código objeto - em uma linguagem formal, representada em binário,
> seguindo os axiomas da arquitetura de von Neumman ...).
>
> Isso é um assunto conhecido nas boas escolas de Ciência da Computação.
>
> []s, Julião
>
>
> Davi Vercillo C. Garcia escreveu:
>> Fala Giancarlo,
>>
>> Acho que faltou um [OFF] no assunto dessa thread... =P
>>
>>> http://www.inovacaotecnologica.com.br/noticias/noticia.php?artigo=primeiro-sistema-operacional-100-livre-erros-esta-pronto&id=010150091020
>>
>> Não existe uma lei de Eng. de Software que diz que é impossível
>> alcançar 100% de corretude em um software ?
>>
>> Abraços,
> -----BEGIN PGP SIGNATURE-----
> Version: GnuPG v1.2.2 (MingW32)
> Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/
>
> iD8DBQFK5K3D0m/vNWbSX14RAj3jAJ9dgKNLcbF7uSPnbycdWLqqvonFcQCgvTvv
> S5tFtaLvlChgOVJbDLwG9Mk=
> =KCWI
> -----END PGP SIGNATURE-----
> -------------------------
> Histórico: http://www.fug.com.br/historico/html/freebsd/
> Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd