Solução ?

Nos últimos posts eu apresentei argumentos para sustentar a idéia que a engenharia de software atual é insuficiente (e na verdade mal merece o nome). Mas qual seria a solução então ?

A idéia é simples de conceber, embora não de realizar: colocar a atividade de criação de software em sólidas bases científicas, assim como as outras engenharias. Fazer com que um projetista de software não apenas desenhe diagramas bonitos com a última moda em confecção de diagramas, mas que também possa provar propriedades sobre o projeto dele, de forma a garantir que as especificações iniciais são satisfeitas. Especificações, aliás, que devem ser expressas formalmente também. Nesse ponto das especificações aparece uma crítica comum: provar que o programa obedece às especificações é inútil se estas não capturam os requerimentos reais do sistema. E como provar que as especificações capturam os requerimentos ? Esse é um problema complicado que poderia, em primeira análise, ser uma repetição do primeiro (coerência do software com especificações), mas a especificação é bem mais simples e de alto nível, o que ajuda a fazer a verificação.

Encontrar essas bases científicas não é coisa que se faz do dia para a noite: os métodos formais atuais ainda são inadequados para as escalas de sistemas construídos. Mas, ao invés de abandonar a idéia de vez, me parece mais lógico trabalhar para melhorar os métodos até que eles se tornem suficientes. E o interessante é que isso já está acontecendo, como eu exemplifiquei neste post. Minha crença é que essa tendência deve continuar, mas ela aconteceria mais rápido se a indústria, como um todo, se preocupasse mais com a qualidade. E essa falta de preocupação vem principalmente da tolerância dos clientes. A verificação que se faz hoje em dia é através de testes, mas todo mundo sabe que testes não podem provar a ausência de erros, apenas sua presença; você confiaria sua vida num sistema que foi apenas testado ?

Em uma de suas frases famosas, Alan Perlis disse "I think that it's extraordinarily important that we in computer science keep fun in computing", com o que eu concordo plenamente. A formalização não vai tornar a criação de software mais chata; programação como artesanato e atividade técnica vai continuar existindo -- eu mesmo junto umas linhas de código para fazer algo que eu quero (ou por diversão) de vez em quando, sem grande preocupação com corretude, e não pretendo deixar de fazer isso. Mas sempre que for necessário um nível de confiabilidade maior, teremos ferramentas para garantir que os programas se comportarão como esperamos.

E isso, por incrível que pareça para quem está muito acostumado com software, é apenas o mínimo que as pessoas costumam exigir de qualquer artefato... que ele funcione.

Mais sobre lógica e formalização

During the last 10 years we have seen a number of failures in these kind of systems. I just mention four well-known examples.

The first example is the Ariadne rocket, a common European space project. The rocket exploded a few seconds after takeoff, due to a software error.

Another well known example is the baggage-handling system of the Denver International Airport. Errors in the software that controls the system required postponement of the official opening (Oct. 1993). By June 1994 the $193 million system was still not functioning, but costing $1.1 million per day in interest and other costs. In early 1995 a manual baggage system was installed in order to open the airport.

Some cancer patients in the USA have received fatal radiation overdoses from the Therac-25, a computer-controlled radiation-therapy machine.

The last example is the Sizewell B nuclear power plant in England. Some years ago it was decided to test the subsystem which is used to close down the reactor if a dangerous situation occurs. The results were not comforting: the software failed almost half of them. They were not able to find the errors in the 100,000 lines of code. Instead, they reduced the overall expectation of the plant's performance from one failure every 10,000 years to one every 1,000 years.

Bengt Nordstrom, Constructivism: A Computing Science Perspective

Esses são exemplos de sistemas críticos, nos quais foi investido muito dinheiro e que mesmo assim foram fracassos consideráveis. Não são os únicos exemplos: Larry Paulson menciona, nas notas de um de seus cursos, um sistema de controle de ambulâncias na Inglaterra que causou a morte de vários pacientes por atraso de atendimento. Tendo em vista isso, é fácil concordar que essa tal engenharia de software deixa muito a desejar. Será que eu sou o único a achar loucura confiar em sistemas assim ?

O trecho é de uma palestra proferida por Bengt Nordstrom em um evento no Vaticano. Sigam o link e leiam a coisa toda, é interessante.

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

Lógica, computação e engenharia de software

Existe uma verdade básica sobre engenharia de software: não existe engenharia de software. Não no sentido das outras engenharias; o que se rotula de "engenharia de software" hoje em dia é parte gerência de projetos, parte coleção de métodos ad hoc para tentar assegurar que as coisas continuem nos trilhos. E os métodos frequentemente falham.

Por outro lado, vinda lá da década de 60, existe a idéia de escrever provas matemáticas de corretude de programas. O assunto foi exaustivamente pesquisado na época, mas logo se viu que o esforço necessário era muito alto para programas não-triviais. As demandas econômicas e a expectativa relativamente baixa dos clientes acabaram impulsionando a atividade de criação de software como um artesanato ao invés de engenharia. E esta é, mais ou menos alguns detalhes, a situação até hoje. Existe uma legião de "programadores" profissionais com formação deficiente, e mesmo muitas universidades que oferecem cursos de ciência da computação se contentam em dar um verniz teórico muito superficial, acompanhado por incontáveis horas de treinamento vocacional em Java ou qualquer que seja a linguagem da moda no momento.

O resultado é visível: bugs e falhas de segurança permanecem abundantes mesmo em software considerado de "alta qualidade". Os clientes se acostumaram a isso como se fosse a única forma, mas não precisa ser assim. O mesmo cliente que simplesmente balança a cabeça ao ver um bug do Word ou uma falha de segurança no seu Windows voltaria correndo para a concessionária devolver um carro que apresentasse o menor defeito. E software livre, sinceramente, não resolve este problema: eu uso Linux diariamente, em casa, mas o número de bugs e incompatibilidades nas aplicações é considerável, embora a base do sistema operacional seja sólida.

Baixas expectativas + altíssima demanda + profissionais incompetentes = software de má qualidade.

Mas as outras engenharias não nasceram da forma que são hoje; elas primeiro passaram por um período de ensino vocacional e técnico antes de chegarem ao estágio atual de assumir uma base científica. O cálculo, a análise matemática, se tornou a base das engenharias entre os séculos XIX e XX.

Pode-se ter esperança, então, que a engenharia de software siga o mesmo caminho. A lógica matemática se mostrou, nestas décadas de desenvolvimento da computação, ser uma base extremamente adequada para a atividade. Por que não dizer que a lógica está para a engenharia de software assim como a análise está para as outras ? Por que não basear a criação de software em uma fundação científica sólida ? Os problemas de gerenciamento de projetos vão continuar existindo, claro, como existem nas outras engenharias. Mas pelo menos quem precisa criar software que funcione terá um conjunto de métodos para garantir que as especificações são satisfeitas, assim como um engenheiro civil garante que uma ponte sustenta uma carga de até X toneladas, mais ou menos um porcentual de erro conhecido e controlado.

Ao ler este artigo de John Allen, eu tive vontade muitas vezes de simplesmente balançar a cabeça em concordância; os argumentos dele sintetizam muito do que eu já acreditava sobre o assunto. A teoria está se tornando cada vez mais relevante, embora a maioria dos praticantes ainda não se dê conta; por exemplo, a adição de genéricos em Java utiliza partes muito avançadas e recentes da teoria dos tipos (quantificação limitada de tipos polimórficos, alguém já ouviu falar?). Mesmo que o resultado não tenha sido excelente, a linguagem foi aumentada de forma significativa sem quebrar a compatibilidade. Esse tipo de cirurgia em linguagens já existentes há anos é quase impossível de ser feita sem deixar alguns efeitos colaterais. E quem fez isso ? Um grupo de teóricos conhecidos, entre eles o famoso Philip Wadler.

A Microsoft, por sua vez, emprega uma verdadeira legião de pesquisadores em linguagens de programação, alguns dos quais trabalharam e ainda trabalham em várias extensões para o CLR (o runtime da plataforma .NET) e para a linguagem C#. A extensão do CLR para usar genéricos, por exemplo. Mas existem várias outras coisas sendo feitas.

A questão é quando a teoria e o rigor vão atingir o Joe-Sixpack-Programmer, o programador comum que está "nas trincheiras". Isso eu não sei, mas desconfio que quem quiser trabalhar no ramo daqui a uns 20 anos deve se preparar para aprender uma boa quantidade de matemática, especialmente lógica...