Olha só as bobagens que diz a imprensa: "Primeiro sistema operacional 100% livre de erros está pronto."
O artigo descreve um sistema operacional embarcado desenvolvido por seis desenvolvedores em seis anos que "está 100% livre de erros de programação". Mais adiante no artigo encontramos a frase chave: "O sistema de verificação garante que o kernel atende inteiramente a toda a sua especificação." Se você ainda não viu a falácia no argumento, leia o post "a mesa errada".
Estar de acordo com a especificação não dá a menor garantia de que um programa não tem erros. O que garante é que há duas descrições equivalentes de um sistema - a especificação e o código. Se houver erros na especificação, haverá erros no código. Pior - a especificação é certamente uma abstração do código, ou seja, há inúmeros detalhes no código que não são tratados na especificação. Qualquer erro presente nesses detalhes não será apanhado pela verificação.
Não estou dizendo que a verificação formal é inútil, muito pelo contrário. É útil, como aponta o artigo, para garantir certas propriedades, como por exemplo garantir que um loop nunca terá valores fora de um intervalo específico, ou talvez garantir que todo objeto alocado será liberado mais tarde. Mas dizer que garante que o sistema não tem bugs é uma grande bobagem. Certamente é culpa do repórter, nenhum pesquisador sério alegaria isso sobre seu trabalho.
O artigo deveria se chamar "primeiro sistema operacional com 100% de conformidade à sua especificação está pronto" ou, melhor ainda, "primeiro sistema operacional que teve alguma especificação está pronto!"
ATUALIZAÇÃO: De fato, os autores do artigo original sabem o que estão falando e não falam nada sobre ausência de bugs - http://www.cse.unsw.edu.au/~kleing/papers/sosp09.html
Tudo isso depende da definição do que é "erro".
ResponderExcluirAlém disso, o SO trata-se de um microkernel, projetado e construído dentro de uma universidade. Possui apenas 8.700 linhas de código C e 600 linhas de assembler. Não é um Windows ou Linux.
E os autores falam sim sobre ausência de bugs:
"With truly small kernels it becomes possible to take secu-
rity and robustness further, to the point where it is possible
to guarantee the absence of bugs."
E parece que eles tomaram conta para que o projeto do kernel também fosse livre de erros:
"We have shown the correctness of a very detailed, low-level design of seL4 and we have formally verified its C implementation."
Não li o artigo inteiro, apenas fiquei curioso com o post e li por cima alguns pontos. Certamente posso ter negligenciado algum trecho que vá de encontro ao que postei.
Mesmo sendo pequeno e a especificação detalhada, eu truco a ausência de bugs. Mais sábias foram as palavras do Knuth: "Beware of bugs in the above code; I have only proved it correct, not tried it."
ResponderExcluirÉ possível implementar um software de calculadora de somar, subtrair e multiplicar, sem bugs?
ResponderExcluir