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

Segunda Outubro 26 09:37:13 BRST 2009

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

Jean,

Se você está em um programa de doutorado, deve saber bastante sobre o
exercício da abstração.

Também, não posso imaginá-lo fazendo afirmações sobre desvios da
pesquisa de computação na universidade brasileira (como abordou em seu
e-mail anterior). É uma grande surpresa, o equívoco vindo de um
estudante de PhD em Cambridge.

A abstração nos permite separar o contexto. A questão aqui na lista (que
não é uma lista acadêmica), foi se existia ou não uma lei abordando a
questão de corretude. Embora tenha visto (durante, antes e depois) que a
ingenuidade dominava o ambiente do debate (veja as referências a,
retórica e quebra de lei) me meti a responder. Provável falha minha ...

Debate dessa natureza numa lista como a FUG-BR é perigoso, pois foge do
interesse da grande maioria dos participantes. Mesmo que sua intenção
seja a de contribuir, sob a ótica da informação.

Por outro lado, são questões muito localizadas e, reconheço ser
necessário estar convivendo diariamente na área para que o conhecimento
fundamental não o deixe se perder.

Portanto, não vou discutir com você esse tema. Ele envolve, fortemente,
paradigmas e, portanto é um terreno minado. Há muitos anos deixei de
lado minhas iniciativas acadêmicas. Sou empresário mas, não me esqueci
dos fundamentos.

Há um exemplo clássico, muitas vezes esquecido, por vergonha (talvez),
no qual grupos fortemente armados de conhecimento sólido se envolveram.
Inclusive grandes empresas, lideres e alguns países.

Começou no Japão, por iniciativa de um grupo de pesquisas
reconhecidamente competente (final da década de 1970, inicio da de 1980,
me parece). O objetivo era em 10 anos, obter o protótipo de um
computador não-von Neumman (em 1992, precisamente). O Japão colocou
US500 milhões de dólares no projeto e recrutou pesquisadores do mundo
inteiro. Pouco tempo depois, animada, a comunidade européia entrou no
jogo, com a chamada "máquina de fluxo de dados", onde células de memória
teriam capacidade de computação. O Brasil e a Argentina se juntaram para
o desenvolvimento de um outro protótipo, pequeno. Somente os EEUU
atrasaram um pouco no início de movimento tão grande. Me lembro,
perfeitamente, da capa da CACM, abordando esse atraso. Alguns anos
depois (2 ou 3 após a iniciativa do Japão), houve a capitulação. O
argumento é de que dificilmente teríamos tecnologia/conhecimento para
escapar da arquitetura de von Neumman.

Embora um fracasso ou, um exercício sobre áreas do conhecimento forçadas
por paradigmas e, iniciativas de mentes brilhantes, o resultado foi
fantástico. Dessa experiência, resultou o Japão com uma competência
reconhecida na área de robótica (o projeto acima pretendia usar,
sobretudo, técnicas de Inteligência Artificial). Está ai a vitoriosa
computação em nuvem, baseada na distribuição de processadores von
Neumman (por favor, abstratamente falando), consolidada a partir dos
conceitos de "máquina de fluxo de dados" do subprojeto europeu. E outros
mais.

Estou comentando sobre isso porque não me sinto confortável em fazer
julgamentos sobre iniciativas de empresas em caminhos obscuros da
ciência. Essa é a forma de fazer ciência e de movimentar o conhecimento
humano. Um bom exemplo é o computador quântico (que talvez venha a ser
eficaz nas suas pesquisas de criptografia). Fico torcendo para que
recursos sejam dispendidos nos caminhos obscuros, do presente. Ficaria
surpreso em saber quanto minhas empresas gastam fazendo pesquisas e
desenvolvimento de novos produtos.

Finalmente, sobre a questão de validade empírica x validade semântica,
acho que você não interpretou correto o que eu disse. Sua interpretação
de "validade" sob a ótica da computação, não faz sentido. Não falei
sobre isso. Agora sim, temos uma confusão, entre alhos e bugalhos.

Bem lembrado o OFF no assunto. Estou lhe respondendo porque você
estabeleceu algumas questões e se dirigiu a mim. Mas, lhe livrei das
minhas, como por exemplo "meramente" matemático. Vindo de um estudante
de PhD, em áreas não tradicionais, fiquei bastante intigrado!

Mas, se responder, por favor, faça-o em privado. Esse tema,
decididamente, nem em OFF interessa a esta lista.

[]s, Julião

Jean Everson Martina escreveu:
> 
>> 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.2.2 (MingW32)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iD8DBQFK5Ynp0m/vNWbSX14RAr61AJ0S5IV0PPECu+mEweqh5rkEAwfA4ACg304e
KxCRyGftYYzJ17xBIS9Q41A=
=s0OV
-----END PGP SIGNATURE-----