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 ------------------------- Histórico: http://www.fug.com.br/historico/html/freebsd/ Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd
