Por José Nuno Oliveira, investigador sénior do HASLab – Laboratório de Software Confiável
O 3º Congresso Mundial sobre Métodos Formais (FM’19 – http://formalmethods2019.inesctec.pt/) decorre de 7 a 11 de outubro, na Alfândega do Porto. Este congresso só se realiza de 10 em 10 anos, tendo o primeiro da série tido lugar em Toulouse (França) em 1999 e o segundo em Eindhoven (Holanda) em 2009. O congresso FM’19 contará com o número record de mais de 30 eventos paralelos, todos relacionados com a promoção de produtividade e a garantia de qualidade do software através do uso de métodos científicos que se possam ensinar às novas gerações de programadores.
Mas, afinal o que são os métodos formais e para que servem? É hoje do conhecimento geral que os serviços eletrónicos, vulgarmente identificados pelo prefixo “e-” acrescentado à sua designação (por exemplo, “e-banking”, “e-learning”) são baseados em programas (software) que operam sobre a internet. Mas o software é muito mais do que isso. Na verdade, todos os sistemas militares, de segurança, de energia, de saúde, de ensino, todos os back-offices e sistemas operacionais das empresas – enfim, todos os sistemas em que a nossa civilização assenta – dependem de software sofisticado que se desenvolve continuamente para que possam operar e servir-nos.
Este processo de softwarização da civilização em que vivemos começou nos anos 50 do século passado. E é quase exclusivamente nele que assenta “I4.0”, a quarta revolução industrial em curso nos nossos dias que deverá conduzir a uma robotização sem precedentes à escala industrial. Tem-se discutido o inevitável impacto social desta revolução no mercado de emprego, tal como o conhecemos hoje. Ainda que as opiniões aqui não sejam totalmente consensuais, trata-se de um problema que o público em geral percebe bem e sente como seu. Já outros problemas associados a esta transformação não são tão discutidos, nem mesmo na comunidade dos técnicos que são seus atores principais. Refiro-me aqui aos riscos que corremos e aos custos em que incorremos quando optamos pela referida robotização.
O software é a camada fisicamente invisível que dota um pedaço de hardware (computador) de inteligência capaz de fazer tarefas consideradas úteis num determinado contexto, muitas delas realizadas por humanos anteriormente. Ora, uma dúvida que legitimamente se coloca é se essa capacidade é real, definitiva e segura. Não poderá um programa que esteja a funcionar bem durante algum tempo vir a ter, de repente e quando menos se espera, uma falha que origine um problema sério que ponha em risco um serviço de que todos dependamos para viver?
Um caso que teve alguma repercussão em Portugal foi o do atraso na colocação dos professores do ensino secundário, em 2004, devido a um problema de software. No entanto, a 30 de setembro desse ano sairia um artigo no jornal Público noticiando que uma pequena empresa havia resolvido finalmente o problema com um novo algoritmo “pensado na íntegra durante seis dias e baseado em princípios matemáticos muito sólidos”, tal como referido por um dos jovens quadros da empresa numa conferência de imprensa. Foi assim que o Ministério da Educação conseguiu divulgar online as listas de professores dois dias antes do prazo quando, uma semana antes, havia anunciado que a colocação voltaria a ser feita manualmente, depois do software que existia ter colapsado.
O que o artigo não refere é que os “princípios matemáticos muito sólidos” com que a jovem empresa resolveu o problema eram o que já na altura se chamava “métodos formais” de programação – precisamente o tema central do congresso de outubro próximo, no Porto. Tais métodos já se ensinavam nalgumas universidades portuguesas desde os anos 80, nomeadamente nas de Lisboa, Minho e Porto.
Quinze anos depois, é com alguma perplexidade que se apura que o ensino desses “princípios matemáticos muito sólidos” não se expandiu como devia, preferindo os académicos ensinar métodos mais empíricos (mas falíveis) por serem mais acessíveis à maioria dos alunos – um fenómeno que não é exclusivo de Portugal.
O resultado é algo frustrante, já que agora que a necessidade de software seguro e fiável é maior do que nunca, em todos os domínios e numa escala há anos inimaginável, temos a espinha dorsal dos recursos de programação enfraquecida e cara. Cara porque errar, mesmo que não resulte num desastre, tem custos acrescidos. E é daí que resulta, em parte, a voraz necessidade de sempre mais recursos em programação dos nossos dias.
Trinta anos depois de 1999, será no Porto que se desenrolará o FM’19, a terceira edição deste congresso, sob o tema “The Next 30 Years” (http://formalmethods2019.inesctec.pt/). A organização está a cargo do Laboratório de Software Confiável (HASLab) do INESC TEC e da Universidade do Minho, por convite da Associação Internacional Formal Methods Europe (FME), que promove esta série de eventos científicos.
Numa galeria de oradores convidados de grande reputação, teremos o gosto de ter connosco Tony Hoare, o prémio Turing que a maioria dos programadores conhece por ter sido o inventor de um célebre algoritmo de ordenação (“quicksort”). Mas a sua atividade na promoção de uma verdadeira ciência da programação vai muito para além disso. Será no congresso do Porto que Tony Hoare, que apesar dos seus 85 anos continua ativo na investigação, dará a palestra que marcará os 50 anos exatos (outubro de 1969) da publicação do seu célebre artigo “An axiomatic basis for computer programming”.
Esse artigo está na origem de um método que, com o tempo, se viria a designar por “lógica de Hoare” e que foi, aliás, o usado pelos jovens informáticos que em 2004 solucionaram quase milagrosamente o problema da colocação dos professores em Portugal. Mas a questão que se coloca é a que está implícita no lema do congresso do Porto, “The Next 30 Years”. O rápido crescimento em diversidade e complexidade das TI tem sido desafiante para comunidade dos métodos formais, que vem adaptando, generalizando e melhorando os modelos e as técnicas de análise que foram o foco dos congressos anteriores. O tema do FM‘19 é uma reflexão sobre o ponto a que a comunidade chegou e as lições que podemos aprender com essa evolução para entender e desenvolver melhor software em tecnologias futuras.
Todos são bem-vindos ao FM’19 para participar nessa reflexão!
O investigador mencionado no artigo tem vínculo à Universidade do Minho.
Notícias, atualidade, curiosidades e muito mais sobre o INESC TEC e a sua comunidade!
