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

[Daniel Bristot de Oliveira]

2009/10/24 Nenhum_de_Nos 

>
> 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-pronto&id=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] [off] não sou só eu :)

[Zavam, Vinícius]

Citando irado furioso com tudo:

> Em Sat, 24 Oct 2009 19:56:10 -0300
> "Zavam, Vinícius" , conhecido consumidor de
> drogas (BigMac's com Coke) escreveu:
>
>> não gosto desse cara. pronto! falei.
>
> também não gosto de goebbels.. mas êle tinha razão quando dizia "uma
> mentira, repetida milhares de vezes, acaba por tornar-se verdade".
>
> o fato de NÃO gostar de uma pessoa não quer dizer que não possamos
> considerar suas opiniões ou conceitos. Eu também não gosto dêle
> (assim como do cão danado - risos), mas NÊSTE MOMENTO eu considero que
> tem razão. Talvez apenas porque estamos concordando em algo.

é. verdade.

> --
>  saudações,
>  irado furioso com tudo

perfeitamente de acordo.
já havia feito essa "reflexão" a um tempo.
não fosse isso, seria um xiita (;



-
Webmail SecrelNet


-
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

[Otacílio]

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-pronto&id=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] [off] não sou só eu :)

[Otacílio]

irado furioso com tudo wrote:
> algum tempo atrás eu disse que olhava com reservas para a aquisição da
> Sun pela Oracle. Eu dizia que temia por uma ação de "abandono" do
> MySQL. O próprio autor do MySQL abandonou a Sun e fundou o MariaDB com
> o objetivo de manter um sempre livre ramo de desenvolvimento do MySQL.
> O wiki é bem interessante:
> 
> http://askmonty.org/wiki/index.php/MariaDB
> 
> bem agora o Stalmann, associado a vários lideres de organizações de
> ativistas buscam conseguir que a CE não aceite a aquisição do MySQL
> (envelopado dentro da Sun) pela Oracle. O temor, expresso na carta
> aberta é exatamente aquele que mencionei tempos atrás.
> 
> Mas enfim, cada um que conclua conforme suas próprias opiniões:
> 
> http://br-linux.org/2009/dr-stallman-pede-que-comissao-europeia-impeca-aquisicao-da-sun-pela-oracle/
> 
> pra refletir num fimdi cheio de sol :)
> 
> bom fimdi pra todos.
> 
> 
> 

Quer dizer que se a minha empresa fizer um software GPL e eu vender a 
empresa eu não posso vender meu software junto com a empresa não? Meu 
software não pode nem agregar valor a minha empresa? Que danado é isso, 
comunismo? Movimento dos sem-software? Mas é fogo mesmo, para esse 
pessoal o software não pode gerar lucro para ninguém, não pode valorizar 
a empresa de ninguém, é mais importante até que as pessoas. É cada uma...
-
Histórico: http://www.fug.com.br/historico/html/freebsd/
Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd

Re: [FUG-BR] Problemas com o Gnome no FreeBSD 8.0-RC1

[Otacílio]

Otacílio de Araújo Ramos Neto wrote:
> 
> 
> 2009/10/23 Otacílio de Araújo Ramos Neto  >
> 
> 
> 
> 2009/10/23 Sergio Augusto Vladisauskis  >
> 
> Instalei tudo do zero, pois na época que saiu o 8.0-RC1 não
> existia os
> 
> pacotes binários, segui passo a passo a instalação e as dependencias
> para não dar problemas e mesmo assim estou enfrentando esses
> pequenos
> problemas, compilei até o OpenOffice e este ficou com as fontes do
> menu zoado e sem estar em pt_BR, o firefox não ficou em pt_BR tb, no
> mais está funcionando bem.
> --
> Sergio Augusto Vladisauskis
> -> Oportunix IT Services Brasil
> 
> 
> Eu compilei o OpenOffice para o 7.1 . Quando atualizei para o 7.2
> junto com os ports fui instalar o pacote do OpenOffice que eu tinha
> compilado anteriormente e o bicho ficou sem mostrar nenhuma palavra
> dos menus. Resolveu quando instalei um pacote pre compilado deste site.
> 
> http://porting.openoffice.org/freebsd/index.html
> 
> Não estou inicializando o Gnome pelo GDM e sim de um terminal mesmo,
> esta funcionando melhor assim.
> 
> 
> Ops, ia esquecendo. Neste site você encontra um pre-compilado  para 
> pt_BR. Instalei o do 7.1 (ou foi 7.0) em um FreeBSD 7.2-RELEASE-p3. Meu 
> charset é UTF8
> 

Para utilizar o UTF8 editei o arquivo /etc/login.conf. Na entrada 
default adicionei

:charset=UTF-8:\
:lang=pt_BR.UTF-8:

Depois rodei um

#cap_mkdb /etc/login.conf
-
Histórico: http://www.fug.com.br/historico/html/freebsd/
Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd

Re: [FUG-BR] [off] não sou só eu :)

[irado furioso com tudo]

Em Sun, 25 Oct 2009 10:09:01 -0200
Otacílio , conhecido consumidor de drogas
(BigMac's com Coke) escreveu:

> Quer dizer que se a minha empresa fizer um software GPL e eu vender a 
> empresa eu não posso vender meu software junto com a empresa não? 

O licenciamento MySQL tem duas vertentes conhecidas: a comercial e a
FOSS. Um dos trechos dos termos de licenciamento indica, claramente:

For developers and distributors of open source software under a FOSS
license other than the GPL, Sun makes its GPL-licensed MySQL Client
Libraries available under a FOSS Exception that enables use of the
those MySQL Client Libraries under certain conditions without causing
the entire derivative work to be subject to the GPL.

 http://www.mysql.com/about/legal/licensing/oem/

embora APARENTEMENTE a briga seja pela não-venda da SUN (ou do MySQL
dentro da SUN) o fundamental é o receio de que a Oracle comece a não
fazer todo o desenvolvimento possível no MySQL, deixando-o mais ou
menos como um Oracle tôsco, ao invés de um concorrente viável.



-- 
 saudações,
 irado furioso com tudo
 Linux User 179402/FreeBSD BSD50853/FUG-BR 154
 Não uso drogas - 100% Miko$hit-free
paradoxo: quase todo mundo quer ver zézuis mas ninguém está disposto a
morrer pra isso :)
-
Histórico: http://www.fug.com.br/historico/html/freebsd/
Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd

Re: [FUG-BR] Qmail no freebsd

[Marcelo da Silva]

eu peguei em 2 servidores meus com qmail, analisando os logs
sempre tinha uma sequencia de umas 30 tentativas
de autenticacao, sempre dando failed até que em um determinado momento
conseguia a autenticacao, o que me levou a crer que parecia um brute
force..
ai eu coloquei o fail2ban para trabalhar e num aconteceu mais o
problema...


On Sat, 24 Oct 2009 22:29:22 -0300, Antônio Pessoa
 wrote:
> 2009/10/24 Anderson Alves de Albuquerque 
>>
>>  Eu utilizo qmail no freebsd. Tenho sofrido com spammers que adivinham
>> senhas dos usuários para poder mandar spams.
>>
>>  Utilizo pop3, imap e smtp com autenticação. EU precisava garantir que
>> as
>> senhas dos usuários sejam verificadas e senhas fáceis sejam impedidas
de
>> serem utilizadas.
>>
>>
>>  Alguém sabe se no freebsd tem algum meio de integrar ao qmailadmin
algo
>> para bloquear as senhas fáceis?
>>
> 
> Você tem certeza que as senhas estão sendo quebradas/adivinhadas e
> utilizadas ou o seu servidor está, sei lá, mau configurado? Não sei se
> seria viável ou possível um spammer quebrar/adivinhar senhas de vários
> usuários de um domínio. Quer dizer, é só uma suposição.
> 
> --
> Antônio Rogério Lins de A. Pessoa
> Técnico em Tecnologia da Informação
> CREA-PE
> -
> 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

[Joao Rocha Braga Filho]

2009/10/25 Daniel Bristot de Oliveira :
> 2009/10/24 Nenhum_de_Nos 
>
>>
>> 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-pronto&id=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

[Julião Braga]

-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-pronto&id=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 e rros está pronto

[Davi Vercillo C. Garcia]

Fala,

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

Foi um pergunta retórica... mas tudo bem... =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

Re: [FUG-BR] [off] não sou só eu :)

[Pablo Sánchez]

2009/10/25 Otacílio :
>
> Quer dizer que se a minha empresa fizer um software GPL e eu vender a
> empresa eu não posso vender meu software junto com a empresa não? Meu
> software não pode nem agregar valor a minha empresa? Que danado é isso,
> comunismo? Movimento dos sem-software? Mas é fogo mesmo, para esse
> pessoal o software não pode gerar lucro para ninguém, não pode valorizar
> a empresa de ninguém, é mais importante até que as pessoas. É cada uma...

Aí entramos em outra seara... os direitos autorais eram seus ou da
empresa? se da empresa, vendeu a empresa, passou os direitos.

Outras pessoas não podem definir o que você fará com a licença. E é
isso que me dá raiva do pessoal do GPL, essa mania de achar que podem
ditar como outros tratam seus pertences (sim, direitos autorais são
bens).

Eu faço o que faço por acreditar que fazendo livre muita gente irá se
beneficiar com o que faço. Mas não fico forçando ninguém a não fazer o
que não quer.

E para mim, que o MySQL morra logo. Ô banquinho ruim. Pelo menos o
PostgreSQL não pipoca sem mais nem menos... E agora que colocaram
versão para windows, finalmente ele caiu no gosto dos desenvolvedores.
Viva!

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

[Pablo Sánchez]

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 :
> 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-pronto&id=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] [off] não sou só eu :)

[Nilson]

2009/10/25 Otacílio :
> Quer dizer que se a minha empresa fizer um software GPL e eu vender a
> empresa eu não posso vender meu software junto com a empresa não? Meu
> software não pode nem agregar valor a minha empresa? Que danado é isso,
> comunismo? Movimento dos sem-software? Mas é fogo mesmo, para esse
> pessoal o software não pode gerar lucro para ninguém, não pode valorizar
> a empresa de ninguém, é mais importante até que as pessoas. É cada uma...

Nada a ver meu, é uma coisa que existe a muitas e muitas décadas, o
protecionismo à monopolização do mercado. E parabéns a União
Européia por estar preocupada com o futuro desse excelente soft
que é o MySQL, e está tentando protegê-lo da Oracle. Ou você acha
que a oracle o comprou pra melhorá-lo? Torná-lo o melhor do mundo?
Implementar nele o EBS e o Forms? MySQL Enterprise Business
Suite with MySQL Forms By ORACLE?

Nunca meu caro... nunca!

[]s
Nilson



-- 
[]s
Nilson
-
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

[Pablo Sánchez]

Pô, não vi que já tinham respondido com Hello World... :-D k,
desculpem por duplicar a piada.

2009/10/24 Nenhum_de_Nos :
>
> 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-pronto&id=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

[Jean Everson Martina]

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-pronto&id=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

[Pablo Sánchez]

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 :
>
> 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-pronto&id=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

[Julião Braga]

-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] Automação eletrônica no freebsd

[Anderson Alves de Albuquerque]

 Eu gostaria de utilizar o meu servidor freebsd para ligar e desligar ar
condicionados. Eu poderia fazer via rede ou portas (serial/USB/paralela).

 Alguém já fez isto?

 alguém conhece algum software de automação no freebsd?

  Alguém conhece algum produto chave ou disjuntor que faça isto?

-- 
[], Anderson Alves de Albuquerque.
---
E-mails: andersonalvesdealbuquerque#hotmail.com (replace # by @)
andersonaa#gmail.com (replace # by @)
ICQ: 73222660
---
-
Histórico: http://www.fug.com.br/historico/html/freebsd/
Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd

Re: [FUG-BR] Automação eletrônica no freebsd

[Eduardo Antonio Bortolini]

Olá,

creio que para desligar/desligar o ar condicionado a solução mais baixo
custo é usar a paralela (uma saída digital) provavelmente vais ter que fazer
um buffer para proteger a porta e acionar um transistor por exemplo para
chavear um relé..
Como a porta parelela é limitada em distância, não sei q distância está o
ar, podes usar a porta serial e  usar módulos com saídas digitas (ou
diretamente a relé), que trabalham com protocolos com Modbus/RTU ou Modbus
ASCII ou protocolos orientados a caracteres e escolher em usar RS-232 ou
se seu servidor já possuir uma porta RS-485(ou usar um conversor RS-232 ou
USB para RS-485) pois RS-485 é para distâncias maiores e por ser diferencial
é mais imune a ruídos é apenas uma dica.



Normalmente, se fores comprar um produto, o fabricante fornece DEMOS para
ajudar no desenvolvimento, existem módulos de aquisição de dados que são
USB, não sei se tem drivers para FreeBSD, com a National Instruments, por
exemplo.

Atenciosamente,Eduardo

2009/10/25 Anderson Alves de Albuquerque 

>  Eu gostaria de utilizar o meu servidor freebsd para ligar e desligar ar
> condicionados. Eu poderia fazer via rede ou portas (serial/USB/paralela).
>
>  Alguém já fez isto?
>
>  alguém conhece algum software de automação no freebsd?
>
>  Alguém conhece algum produto chave ou disjuntor que faça isto?
>
> --
> [], Anderson Alves de Albuquerque.
> ---
> E-mails: andersonalvesdealbuquerque#hotmail.com (replace # by @)
> andersonaa#gmail.com (replace # by @)
> ICQ: 73222660
> ---
> -
> 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] Automação eletrônica no freebsd

[Pablo Sánchez]

Caro, só faltou fazer a pesquisa certa no Google. Achei este link

http://www.drivemeinsane.com/khowtos/relay

Acho que responde tudo que você precisa (exceto como programar as
postas no FreeBSD, mas isso vc encontra lá no site do FreeBSD, na
parte destinada a developers).



2009/10/25 Eduardo Antonio Bortolini :
> Olá,
>
> creio que para desligar/desligar o ar condicionado a solução mais baixo
> custo é usar a paralela (uma saída digital) provavelmente vais ter que fazer
> um buffer para proteger a porta e acionar um transistor por exemplo para
> chavear um relé..
> Como a porta parelela é limitada em distância, não sei q distância está o
> ar, podes usar a porta serial e  usar módulos com saídas digitas (ou
> diretamente a relé), que trabalham com protocolos com Modbus/RTU ou Modbus
> ASCII ou protocolos orientados a caracteres e escolher em usar RS-232 ou
> se seu servidor já possuir uma porta RS-485(ou usar um conversor RS-232 ou
> USB para RS-485) pois RS-485 é para distâncias maiores e por ser diferencial
> é mais imune a ruídos é apenas uma dica.
>
>
>
> Normalmente, se fores comprar um produto, o fabricante fornece DEMOS para
> ajudar no desenvolvimento, existem módulos de aquisição de dados que são
> USB, não sei se tem drivers para FreeBSD, com a National Instruments, por
> exemplo.
>
> Atenciosamente,Eduardo
>
> 2009/10/25 Anderson Alves de Albuquerque 
>
>>  Eu gostaria de utilizar o meu servidor freebsd para ligar e desligar ar
>> condicionados. Eu poderia fazer via rede ou portas (serial/USB/paralela).
>>
>>  Alguém já fez isto?
>>
>>  alguém conhece algum software de automação no freebsd?
>>
>>  Alguém conhece algum produto chave ou disjuntor que faça isto?
>>
>> --
>> [], Anderson Alves de Albuquerque.
>> ---
>> E-mails: andersonalvesdealbuquerque#hotmail.com (replace # by @)
>> andersonaa#gmail.com (replace # by @)
>> ICQ: 73222660
>> ---
>> -
>> 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] Automação eletrônica no freebsd

[Davi Vercillo C. Garcia]

Fala Anderson,

>>>  Alguém já fez isto?

Eu tenho um projeto pessoal que buscar automatizar meu quarto,
utilizando microcontroladores (PIC16F887) e o FreeBSD. Ainda não tenho
nada concreto, mas não é complicado... só falta tempo...

Se o que você quer automatizar é simples, você não vai precisar usar o
microcontrolador, podendo se comunicar diretamente através da porta
serial ou paralela.

>>>  alguém conhece algum software de automação no freebsd?

Acho que pra essa aplicação será complicado de achar pronto, mas é
simples fazer um programinha Python pra controlar isso.

>>>  Alguém conhece algum produto chave ou disjuntor que faça isto?

Como j[a responderam, o dispositivo que você procura se chama Relay
(http://en.wikipedia.org/wiki/Relay) e seu funcionamento é bem
simples.

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

Re: [FUG-BR] Primeiro sistema operacional 100% livre de e rros está pronto

[Davi Vercillo C. Garcia]

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

Re: [FUG-BR] [off] não sou só eu :)

[Otacílio]

Nilson wrote:
> 2009/10/25 Otacílio :
>> Quer dizer que se a minha empresa fizer um software GPL e eu vender a
>> empresa eu não posso vender meu software junto com a empresa não? Meu
>> software não pode nem agregar valor a minha empresa? Que danado é isso,
>> comunismo? Movimento dos sem-software? Mas é fogo mesmo, para esse
>> pessoal o software não pode gerar lucro para ninguém, não pode valorizar
>> a empresa de ninguém, é mais importante até que as pessoas. É cada uma...
> 
> Nada a ver meu, é uma coisa que existe a muitas e muitas décadas, o
> protecionismo à monopolização do mercado. E parabéns a União
> Européia por estar preocupada com o futuro desse excelente soft
> que é o MySQL, e está tentando protegê-lo da Oracle. Ou você acha
> que a oracle o comprou pra melhorá-lo? Torná-lo o melhor do mundo?
> Implementar nele o EBS e o Forms? MySQL Enterprise Business
> Suite with MySQL Forms By ORACLE?
> 
> Nunca meu caro... nunca!
> 

Gostar pode até gostar, mas dizer que é excelente aí já é exagero, é só 
dar uma olhada aqui:
http://en.wikipedia.org/wiki/Comparison_of_relational_database_management_systems
Queria ver se o mascote do mySQL não fosse aquele simpático golfinho se 
ele teria ido tão longe.
Fazer software de código aberto porque é divertido, passa tempo, como um 
novo modelo de negócio ou para escapar de um monopólio tudo bem. Agora 
tornar o software mais importante que as pessoas aí vamos parar com isso 
né? É derrubar a laranjeira da informática. E se a Oracle fez isso está 
mais do que certa, você gostaria se o seu concorrente fizesse dumping no 
seu mercado? Admiro muitíssimo todos os desenvolvedores que usam licença 
BSD like. Estes sim fazem software para o bem de todos.

-
Histórico: http://www.fug.com.br/historico/html/freebsd/
Sair da lista: https://www.fug.com.br/mailman/listinfo/freebsd