Continuando a discussão

Depois do post passado, Herval escreveu no Geek4Life um post sobre "computação úbiqüa", computação pervasiva ou como queira chamar. Por acaso, essa é justamente uma das minhas maiores preocupações com a questão de computação confiável; quando se tem software em todo lugar, em todos aspectos da vida, é de extrema importância que tudo funcione bem. Então escrevi um comentário:

Relacionado ao meu post sobre engenharia de software, não dá medo usar software em todos esses lugares, considerando a qualidade média do que se produz hoje ? :)

Ao que Herval respondeu:

Acho que desenvolvimento de software hoje é meio que um artesanato com gerência e prazos.

ps.: software embarcado, imho, é uma das áreas menos problemáticas da tecnologia (talvez pelo pequeno tamanho da coisa). Meu celular costuma travar bem menos que meu PC. Meu cartão de crédito com 'chipinho inteligente' nunca travou durante uma compra ou autorização de crédito. Só não sei como vai ser quando a casa toda começar a ficar automatizada e inteligente... :)

E eu, por fim, fiz como resposta um outro comentário que tem mais alguns exemplos:

Sim, concordo que software embutido dá muito menos problema, não por que sabemos fazer esse tipo de software melhor, mas porque ele é menos complexo. Como você disse, seu celular "trava bem menos" que o PC, mas ainda trava :)

E o problema é, cada vez mais nossas vidas vão dependendo de software, em muitos aspectos. Esse nível de qualidade é claramente inaceitável quando coisas mais críticas começam a depender de software que é essencialmente imprevisível.

Uma coisa que pouca gente tem idéia é que desde o fiasco do bug de divisão do Pentium, a Intel investe pesado em métodos formais para verificação do projeto dos seus chips; as concorrentes, obviamente, seguiram a mesma direção e hoje em dia nenhum chip sai da sala de projeto para a planta da fábrica sem ter sido verificado formalmente, com provas matemáticas que ele funciona como especificado.

Outro ponto onde métodos formais são usados corriqueiramente é no projeto de protocolos. Um conhecido meu está trabalhando na Microsoft Research atualmente nesse ramo.

E por falar em Microsoft, existe uma ferramenta desenvolvida internamente pelo pessoal da MSR que verifica drivers. Usa essas técnicas de métodos formais e verificação de modelos (model checking) e foi escrita em OCaml.

Esses exemplos seriam quase impensáveis há meros 10 anos. Imagine o que pode acontecer 10 anos para frente...