Re: [FUG-BR] Primeiro sistema operacional 100% livre de erros está pronto - OFF
-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- - Histórico: http://www.fug.com.br/historico/html/freebsd/ Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd
Re: [FUG-BR] Primeiro sistema operacional 100% livre de erros está pronto - OFF
É isso ai lista continuamos a thread... pois a aula está muito interessante... 2009/10/26 Jean Everson Martina ever...@inf.ufsc.br -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- - 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
Re: [FUG-BR] Primeiro sistema operacional 100% livre de erros está pronto - OFF
-BEGIN PGP SIGNED MESSAGE- Hash: SHA1 Quer trazer a discussão In Topic de novo? Eu falei com o Robert Watson (FreeBSD Foundation) a umas duas semanas atras, quando o paper que deu origem a isso tudo foi publicado, e perguntei quando teríamos uma coisa assim no FreeBSD, e a resposta foi: Nunca! Porque a comunidade não tem idéia de quão benéfico isso poderia ser pro projeto Entender e ter condições de discutir este tipo de tópico, é em geral o que difere um Cientista da Computação de um Micreiro (leia-se prático). Jean Paulo Henrique wrote: É isso ai lista continuamos a thread... pois a aula está muito interessante... 2009/10/26 Jean Everson Martina ever...@inf.ufsc.br 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 - - 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 -BEGIN PGP SIGNATURE- Version: GnuPG v1.4.8 (Darwin) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAkrle+AACgkQQN0Max56WicXnwCgmSgxz/IOiAmyFWIj80QHmNWA Ez0AnitUbLbgK2CBEs5jmiMfqDbe/rwM =Lr0k -END PGP SIGNATURE- - Histórico: http://www.fug.com.br/historico/html/freebsd/ Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd
Re: [FUG-BR] Primeiro sistema operacional 100% livre de erros está pronto - OFF
-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):
Re: [FUG-BR] Primeiro sistema operacional 100% livre de erros está pronto - OFF
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
Re: [FUG-BR] Primeiro sistema operacional 100% livre de erros está pronto
2009/10/25 Davi Vercillo C. Garcia daviverci...@gmail.com: Pessoal, Acho que essa thread já deu, né ? Não fiz a abordagem com o objetivo de criar um debate acadêmico. Somente para responder ao Davi. Mesmo que tenha sido uma resposta a uma pergunta retórica... hiuiha... =P Abraços, -- Davi Vercillo C. Garcia B.Sc. Student - DCC-IM/UFRJ Trainee (SysAdmin) - NACAD/COPPE A computer lets you make more mistakes faster than any invention in human history with the possible exceptions of handguns and tequila. - Unknown - Histórico: http://www.fug.com.br/historico/html/freebsd/ Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd Oi pessoal, me passaram este link numa outra lista (COMBASE) da qual faço parte. http://ertos.nicta.com.au/publications/papers/Klein_EHACDEEKNSTW_09.pdf Pretendo tirar minha dúvidas. -- Jackson S de Jesus. - Histórico: http://www.fug.com.br/historico/html/freebsd/ Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd
Re: [FUG-BR] Primeiro sistema operacional 100% livre de erros está pronto
2009/10/24 Nenhum_de_Nos math...@eternamente.info On Sat, October 24, 2009 21:25, Giancarlo Rubio wrote: Será?? http://www.inovacaotecnologica.com.br/noticias/noticia.php?artigo=primeiro-sistema-operacional-100-livre-erros-esta-prontoid=010150091020 como disse um amigo quando leu isso, este so deve fazer só umprimir hello world e a hora para ser 100% perfeito ... matheus -- We will call you cygnus, The God of balance you shall be A: Because it messes up the order in which people normally read text. Q: Why is top-posting such a bad thing? http://en.wikipedia.org/wiki/Posting_style - Histórico: http://www.fug.com.br/historico/html/freebsd/ Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd Replicando minha resposta uma outra lista... Eu acho que o enfoque ai foi mal interpretado pelo escritor da notícia, Acho que o que deveria ser exaltado é: A nova técnicas de verificação que pode garantir com rigor matemático a confiabilidade de um software. A partir disto é possível corrigir um sistema, como o sistema operacional mencionado até que não hajam mais erros. Como também mencionado na noticia, este é um sistema operacional para um sistema embarcado, isto é, é um sistema operacional para uma aplicação específica, esta não mencionada no artigo o que diminui mais ainda o mérito pois, por exemplo, este pode rodar em uma arquitetura muito simples, como a ARM 7 e ainda executar uma operação muito específica, como o de um microondas. Ainda, este pode ser um micro-kernel, o que faria com que o desenvolvimento de um Kernel sem Bugs fosse mais simples. Então, acho que foi infeliz quem fez o título desta notícia, primeiro pelo enforque errado segundo pela afirmação, pois, não se comprovou matematicamente que outros sistemas operacionais tem falhas. OBS: Quando falo de sistemas operacionais menciono todos os softwares que fazem interface entre software/hardware e o gerenciamento destes recursos. Sobre uma proposta de sistema operacional altamente confiável, existe o minix-3, que é um sistema operacional que possui um micro-kernel e consegue recuperar-se de falhas de forma rápida e transparente devido a sua arquitetura de micro kernel, como o Symbiam OS, e não como um kernel monolítico como o Linux/FreeBSD/OpenBSD/NetBSD/ Windows(todas as familias)/MAC OS/HP-UX/IRIX/Sun Solaris/VDK/um etc... bem grande/. O diferencial é que ele obedece o padrão POSIX, o que lhe da a possibilidade de executar qualquer programa para sistemas que obedecem este padrão (os Unix) e executa sobre intel 32 bits. Então, galera, dou a dica de ter um senso crítico mais aguçado quando ler notícias com um título tão alarmante, como as notícias do programa do Datena. -- Daniel Bristot de Oliveira - Histórico: http://www.fug.com.br/historico/html/freebsd/ Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd
Re: [FUG-BR] Primeiro sistema operacional 100% livre de erros está pronto
Nenhum_de_Nos wrote: On Sat, October 24, 2009 21:25, Giancarlo Rubio wrote: Será?? http://www.inovacaotecnologica.com.br/noticias/noticia.php?artigo=primeiro-sistema-operacional-100-livre-erros-esta-prontoid=010150091020 como disse um amigo quando leu isso, este so deve fazer só umprimir hello world e a hora para ser 100% perfeito ... matheus Ultimamente tenho visto muito problema com horário de verão. Acho melhor avisar a equipe de engenharia para remover a hora e deixar somente o Hello World. A hora vamos imprimir apenas na versão Enterprise. - Histórico: http://www.fug.com.br/historico/html/freebsd/ Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd
Re: [FUG-BR] Primeiro sistema operacional 100% livre de erros está pronto
2009/10/25 Daniel Bristot de Oliveira danielbris...@gmail.com: 2009/10/24 Nenhum_de_Nos math...@eternamente.info On Sat, October 24, 2009 21:25, Giancarlo Rubio wrote: Será?? http://www.inovacaotecnologica.com.br/noticias/noticia.php?artigo=primeiro-sistema-operacional-100-livre-erros-esta-prontoid=010150091020 como disse um amigo quando leu isso, este so deve fazer só umprimir hello world e a hora para ser 100% perfeito ... matheus -- We will call you cygnus, The God of balance you shall be A: Because it messes up the order in which people normally read text. Q: Why is top-posting such a bad thing? http://en.wikipedia.org/wiki/Posting_style - Histórico: http://www.fug.com.br/historico/html/freebsd/ Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd Replicando minha resposta uma outra lista... Eu acho que o enfoque ai foi mal interpretado pelo escritor da notícia, Acho que o que deveria ser exaltado é: A nova técnicas de verificação que pode garantir com rigor matemático a confiabilidade de um software. A partir disto é possível corrigir um sistema, como o sistema operacional mencionado até que não hajam mais erros. Como também mencionado na noticia, este é um sistema operacional para um sistema embarcado, isto é, é um sistema operacional para uma aplicação específica, esta não mencionada no artigo o que diminui mais ainda o mérito pois, por exemplo, este pode rodar em uma arquitetura muito simples, como a ARM 7 e ainda executar uma operação muito específica, como o de um microondas. Ainda, este pode ser um micro-kernel, o que faria com que o desenvolvimento de um Kernel sem Bugs fosse mais simples. Então, acho que foi infeliz quem fez o título desta notícia, primeiro pelo enforque errado segundo pela afirmação, pois, não se comprovou matematicamente que outros sistemas operacionais tem falhas. OBS: Quando falo de sistemas operacionais menciono todos os softwares que fazem interface entre software/hardware e o gerenciamento destes recursos. Sobre uma proposta de sistema operacional altamente confiável, existe o minix-3, que é um sistema operacional que possui um micro-kernel e consegue recuperar-se de falhas de forma rápida e transparente devido a sua arquitetura de micro kernel, como o Symbiam OS, e não como um kernel monolítico como o Linux/FreeBSD/OpenBSD/NetBSD/ Windows(todas as familias)/MAC OS/HP-UX/IRIX/Sun Solaris/VDK/um etc... bem grande/. O diferencial é que ele obedece o padrão POSIX, o que lhe da a possibilidade de executar qualquer programa para sistemas que obedecem este padrão (os Unix) e executa sobre intel 32 bits. Então, galera, dou a dica de ter um senso crítico mais aguçado quando ler notícias com um título tão alarmante, como as notícias do programa do Datena. Achoq ue não levaram e conta a lei máxima que rege o Universo, a Lei de Murphy. Certamente esqueceram de algo. Ele pode estar perfeito pelos critérios usados, mas podem ter esquecido de usar também algum outro critério, que um dia será necessário. João Rocha. -- Daniel Bristot de Oliveira - Histórico: http://www.fug.com.br/historico/html/freebsd/ Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd -- Sempre se apanha mais com as menores besteiras. Experiência própria. goffr...@gmail.com - Histórico: http://www.fug.com.br/historico/html/freebsd/ Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd
Re: [FUG-BR] Primeiro sistema operacional 100% livre de erros está pronto
-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-prontoid=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
Re: [FUG-BR] Primeiro sistema operacional 100% livre de erros está pronto
Leis surgiram para serem quebradas! :-D Mas a verdade é que eu duvido que não tenha um erro sequer. Só se o sistema só faz dar boot e printa Hello World na tela. Mas aí, não é operacional... 2009/10/24 Davi Vercillo C. Garcia daviverci...@gmail.com: 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-prontoid=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, -- Davi Vercillo C. Garcia B.Sc. Student - DCC-IM/UFRJ Trainee (SysAdmin) - NACAD/COPPE A computer lets you make more mistakes faster than any invention in human history with the possible exceptions of handguns and tequila. - Unknown - 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 phack...@gmail.com (61) 9975-0883 http://www.sanchez.eti.br http://www.corephp.com.br Quidquid latine dictum sit, altum viditur = - Histórico: http://www.fug.com.br/historico/html/freebsd/ Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd
Re: [FUG-BR] Primeiro sistema operacional 100% livre de erros está pronto
Pô, não vi que já tinham respondido com Hello World... :-D k, desculpem por duplicar a piada. 2009/10/24 Nenhum_de_Nos math...@eternamente.info: On Sat, October 24, 2009 21:25, Giancarlo Rubio wrote: Será?? http://www.inovacaotecnologica.com.br/noticias/noticia.php?artigo=primeiro-sistema-operacional-100-livre-erros-esta-prontoid=010150091020 como disse um amigo quando leu isso, este so deve fazer só umprimir hello world e a hora para ser 100% perfeito ... matheus -- We will call you cygnus, The God of balance you shall be A: Because it messes up the order in which people normally read text. Q: Why is top-posting such a bad thing? http://en.wikipedia.org/wiki/Posting_style - 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 phack...@gmail.com (61) 9975-0883 http://www.sanchez.eti.br http://www.corephp.com.br Quidquid latine dictum sit, altum viditur = - Histórico: http://www.fug.com.br/historico/html/freebsd/ Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd
Re: [FUG-BR] Primeiro sistema operacional 100% livre de erros está pronto
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-prontoid=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
Re: [FUG-BR] Primeiro sistema operacional 100% livre de erros está pronto
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 ever...@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-prontoid=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 phack...@gmail.com (61) 9975-0883 http://www.sanchez.eti.br http://www.corephp.com.br Quidquid latine dictum sit, altum viditur = - Histórico: http://www.fug.com.br/historico/html/freebsd/ Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd
Re: [FUG-BR] Primeiro sistema operacional 100% livre de erros está pronto
-BEGIN PGP SIGNED MESSAGE- Hash: SHA1 O Teorema da Parada, prova a indecidibilidade, para qualquer programa. É um teorema. O Teorema de Goedel não é meramente matemático. É um teorema! Meramente matemático é um termo novo para mim. Não sei o que significa. Nem vou lhe pedir para explicar. A referência a Goedel foi para lembrar da incompletude de sistemas formais. Uma linguagem de programação é um sistema formal. Logo, a linguagem de programação é incompleta. Portanto, cuidado quando usá-la. A aritmética (ou a matemática) é incompleta, portanto, cuidado ao usá-la. O Teorema da Parada, não me parece ser de Turing (Turing, provou que ele não tem solução). Turing provou usando sua máquina (a famosa máquina de Turing, importantíssima para os teóricos de complexidade de algorítmos). Mostrou, na realidade que não se pode criar um procedimento efetivo (do ponto de vista da Tese de Church). Provado, ele passou de uma conjectura, para teorema. Qual a visão prática de Goedel e Turing x o Teorema da Parada? Nenhum progamador sério, pequeno, grande ou em equipe irá desenvolver programas achando que ele estará correto. Um bom programador, pratica a humildade, claro. E, leva em conta alguns colorários: C1. Programar é difícil. C2. Programar é uma arte. C3. Não é possível desenvolver procedimentos automáticos para provar que um programa está correto. (Os grandes players não são malucos. Portanto, não gastam dinheiro procurando por isso. O que eles devem ter é algo que indique com grande chance, que um programa pode estar correto. Ou alguma ferramenta parecida.) ... Cn. Outros. 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. Assim como Pitagoras, que achou a nossa conhecida solução para a**2 + b**2 = c**2. Você iria tentar resolver a**n + b**n = c**n, para n=3, sabendo que existe um Teorema (provado, em 1965) dizendo que qualquer equação dessas para n = 3, não tem solução? Não fiz a abordagem com o objetivo de criar um debate acadêmico. Somente para responder ao Davi. []s, Julião Jean Everson Martina escreveu: 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 -BEGIN PGP SIGNATURE- Version: GnuPG v1.2.2 (MingW32) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iD8DBQFK5N/j0m/vNWbSX14RAufMAKCbQ0poH+CZyo5iA/QdfIer4mZL1ACgrbQM 8N7TnXBFgPK1RvFijiD5n8g= =wcYB -END PGP SIGNATURE- - Histórico: http://www.fug.com.br/historico/html/freebsd/ Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd
[FUG-BR] Primeiro sistema operacional 100% livre de erros está pronto
Será?? http://www.inovacaotecnologica.com.br/noticias/noticia.php?artigo=primeiro-sistema-operacional-100-livre-erros-esta-prontoid=010150091020 -- Giancarlo Rubio - Histórico: http://www.fug.com.br/historico/html/freebsd/ Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd
Re: [FUG-BR] Primeiro sistema operacional 100% livre de erros está pronto
On Sat, October 24, 2009 21:25, Giancarlo Rubio wrote: Será?? http://www.inovacaotecnologica.com.br/noticias/noticia.php?artigo=primeiro-sistema-operacional-100-livre-erros-esta-prontoid=010150091020 como disse um amigo quando leu isso, este so deve fazer só umprimir hello world e a hora para ser 100% perfeito ... matheus -- We will call you cygnus, The God of balance you shall be A: Because it messes up the order in which people normally read text. Q: Why is top-posting such a bad thing? http://en.wikipedia.org/wiki/Posting_style - Histórico: http://www.fug.com.br/historico/html/freebsd/ Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd
