|
Os excertos abaixo são de uma comunicação que fiz no âmbito da atribuição do Prémio IBM 2010 à Alexandra Silva, que resume algumas das intuições que estiveram presentes na génese e no desenvolvimento do projeto MathIS, que desse modo viu reconhecida uma das dimensões do seu plano de trabalho:
(...) A tese de doutoramento da Alexandra generaliza um dos resultados maiores das Ciências da Computação: o teorema de Kleene. Stephen Kleene formalizou nos anos cinquenta um modelo para a dinâmica da computação, o autómato de estados finitos, e introduziu uma linguagem, as expressões regulares, para especificar o seu comportamento. O célebre teorema que tem o seu nome enuncia a equivalência entre uns e outras, fornecendo uma abstração de um processo computacional e um modo rigoroso de descrever/prescrever o seu comportamento.
Durante anos a herança de Kleene foi inspiração e desafio. Nomeadamente na procura de axiomatizações que permitissem a manipulação expedita dessas expressões, na conceção de algoritmos eficientes para o seu processamento, e sobretudo na tentativa de generalização deste resultado a modelos comportamentais mais complexos.
Ora é exatamente neste ponto que a contribuição científica da Alexandra se situa. O seu trabalho tornou possível a derivação uniforme de linguagens para especificação de um conjunto muito vasto de modelos computacionais, das respetivas axiomatizações e, para cada caso, de um resultado de equivalência no espírito do teorema de Kleene. Não apenas a sua abordagem cobre todos os casos documentados na literatura, para muitos dos quais apenas se conheciam soluções ad hoc, como permitiu tratar outros com solução até então desconhecida, nomeadamente modelos para sistemas com evolução incerta muito relevantes em aplicações onde a probabilidade de falha e o controlo de exceções tem de ser rigorosamente considerado.
(...) Finalmente, na medida em que permite modelar, calcular e verificar o comportamento de sistemas muito complexos, o trabalho tem implicações práticas de relevo para a conceção de sistemas informáticos confiáveis, isto é em que literalmente possamos confiar. Que não colapsam, que não se degradam, que fazem aquilo que muito prosaicamente se espera que façam.
(...) Infelizmente popularizou-se uma visão redutora que identifica a Informática com uma coleção de tecnologias e o desenvolvimento de software com um conjunto de metodologias empíricas e boas práticas. Habituamo-nos a conviver com “os erros do sistema”, a desculpar os seus pretensos estados de alma, a aceitar irrefletidamente que ao comprar um pacote de software recebamos não uma garantia, mas uma limitação de responsabilidade.
Não foi esta visão frouxa e sem ambição que motivou o projeto MathIS e trabalho da Alexandra e que o Prémio Científico IBM tão justamente distinguiu.
E ainda bem. Porque, de facto, se o que estiver em causa for o funcionamento de um dispositivo médico que me mantém ligado à vida ou o controlador do avião em que viajo, não estou interessado em meias certezas. Não me interessam testes em curso de execução, de resultados duvidosos para a minha sobrevivência, não quero saber de volumosos e verbosos cadernos de encargos nem de argumentos legais. Sobre a correção, a segurança e o desempenho desses sistemas não quero nada menos que o grau de certeza que me dá uma prova matemática. E não desempenha hoje a noção de prova automaticamente verificável um papel chave na garantia da segurança de uma compra on-line? Ou na certificação de software crítico cuja pertinência é já reconhecida pela indústria mais atenta e inovadora?
A verdade é que a Informática experimentou um desenvolvimento tecnológico vertiginoso bem antes de se haver constituído como ciência. E, no entanto, a complexidade crescente das suas aplicações exige a solidez e o rigor formal a que nos habituamos em outros domínios da Engenharia. Temos que construir os seus fundamentos e operacionalizá-los em técnicas e cálculos. Vivemos, mas a uma velocidade acelerada, o nosso século XVII. O trabalho hoje distinguido, e toda a área de investigação em que se insere, são parte essencial, assim o creio, do nosso passaporte para o futuro.
Por Luís Barbosa, coordenador do projeto MathIS
|