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

[Jean Everson Martina]

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


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

Você esta confundido a abrangência do teorema de parada. Ele diz que não
existe algorítimo genérico para decidir a parada para todos os pares
entrada-programa. O que não quer dizer que não existe solução para casos
específicos.

Sobre a validade empírica, você pode explicar o que é uma validade
formal então?

De novo, se você estiver correto de que tudo é empírico, um player como
a MS, não investiria mais de 2 milhões de libras no projeto Terminator
(o que prova que não é brincadeirinha acadêmica):

http://research.microsoft.com/en-us/um/cambridge/projects/terminator/default.htm

O Terminator é um dos maiores responsáveis pelo aumento de estabilidade
do XP, Vista e 7. Você vê hoje muito menos telas azuis e crashes, porque
o drivers certificados foram sendo verificados quanto a não parada. Sim,
se está longe de ter a verificação formal completa de um SO de uso
genérico. Mas eu digo que em 15 anos isso será um fato.

Na verdade, tem outros projetos semelhantes sobre verificação de chips
usando métodos automatizados e logica de ordem mais alta, que são usados
pela ARM (100% do que a ARM faz é verificado formalmente, e eles são a
maior plataforma de Micro-processadores hoje). A Intel e AMD também
fazem mas não em 100% dos casos.

Aqui mesmo (Grupo de Teoria da Computação de Cambridge), temos projetos
com a NSA pra verificação formal de micro-processadores criptográficos,
, com a Cisco e Boeing na área de roteamento, com a IBM na área de
módulos java e com a Intel na verificação de assembly x86, etc

Meu PhD é sobre verificação formal de protocolos criptográficos, onde
parte da pesquisa já foi bancada pela VISA (verificação do SET) e pelo
Internet Consortium (Verificação do SSL). Hoje o governo brasileiro (que
me banca) tem interesse em verificar os grandes protocolos no cenário
nacional, tais como SPB, NF-e e OpenHSM. É por isso que eu to aqui.

Sobre uma outra pergunta na discussão sobre a usabilidade deste
microkernel: Sim ele é utilizável e funcional, mas dentro da plataforma
e objetivos à que se propõe.


Jean
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.8 (Darwin)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAkrldh0ACgkQQN0Max56Wid4KwCggkNfAxKzj/B5oLBn4Bt1uPty
Ow0AoKbvPMBAmEbKWTe6eQHsN45ULGP8
=CheR
-----END PGP SIGNATURE-----