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

Segunda Outubro 26 10:41:57 BRST 2009

2009/10/26 Julião Braga <juliao at braga.eti.br>:
> -----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-----
> -------------------------
> Histórico: http://www.fug.com.br/historico/html/freebsd/
> Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd
>

Julião,

A discussão tá bem interessante... é muito bom um debate/troca de
idéias de alto nível.

-- 
Celso Vianna
BSD User: 51318
http://www.bsdcounter.org

63 8404-8559
Palmas/TO