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

[Pablo Sánchez]

Ainda assim, o que interessa é o seguinte:

é realmente um sistema operacional? Quer dizer, serve para eu operar
de verdade a máquina? Ou falavam apenas de um simples kernel que deu
boot, Hello World, e pronto?

Realmente concordo que o foco da notícia ficou equivocado. O bonito do
trabalho aí é o algoritmo de teste, e não o kernel livre de erros. O
pior é que pelo código, pode até estar certo, mas se eu coloquei um 9
onde era para ser um 10, o código estará correto em análise
computacional, mas o resultado vai ser outro e o comportamento do
sistema operacional já não será tão operacional assim. Ou seja, eu
lamento, mas acho dificílimo que o algoritmo tenha total capacidade de
analisar se um código está correto ou não. Acredito que apenas seres
com capacidade racional poderiam fazer uma análise dessas, ou seja,
perceber realmente um erro pequeno, que é código correto, mas gera
resultado errado... Temos os testes Unit que fariam isso, claro,
checando o resultado apenas. Mas mesmo com eles ainda conseguimos
coisas erradas.



2009/10/25 Jean Everson Martina <everson em inf.ufsc.br>:
>
> 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
>



-- 
=================================
Pablo Santiago Sánchez
Análise e Desenvolvimento de Sistemas Web
Zend Certified Engineer #ZEND006757
phackwer em gmail.com
(61) 9975-0883
http://www.sanchez.eti.br
http://www.corephp.com.br
"Quidquid latine dictum sit, altum viditur"
=================================