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