The congress that analyses the impacts of society’s «softwarisation»

The 3rd World Congress on Formal Methods  – FM’19 will take place between 7 and 11 October at the Alfândega Porto Congress Centre. This congress only takes place every 10 years, with the first one taking place in Toulouse (France) in 1999 and the second one in Eindhoven (the Netherlands) in 2009. The FM’19 congress will have a record number of over 30 side events, all of them related to the promotion of productivity and the assurance of software quality through the use of scientific methods that can be taught to the new generations of programmers.

But, after all, what are the formal methods and what are they used for? As we all know, electronic services, commonly identified by the prefix “e-” that is added to their name (i.e. “e-banking”, “e-learning”) are based on (software) programmes that operate on the internet. But software is so much more than that. In fact, all military, security, energy, health, education systems, all back offices and company’s operating systems — well, all the systems in which our civilisation is based on — rely on sophisticated software that is continuously being developed so that they can operate and serve us.

This softwarisation process of the civilisation we’re living in began in the 1950s. And it is almost exclusively on it that “I4.0” is based upon, the ongoing fourth industrial revolution that should lead to unprecedented robotisation at an industrial scale. The inevitable social impact of this labour market’s revolution, as we know it today, has been permanently discussed. While opinions are not entirely consensual on this topic, this is a problem that the general public understands and feels as their own. Other problems associated with this transformation are not discussed so much, not even by the community of technicians who are its main actors. I am thinking of the risks we’re running and the costs we’re incurring when opting for such robotisation.

Software is the physically invisible layer that endows a piece of hardware (computer) with intelligence capable of performing tasks considered to be useful in a given context, many of them being previously performed by humans. Now, a legitimate question arises: is this ability real, final and secure? What if a programme that is working well for a while, suddenly and unexpectedly crashes, resulting in a serious problem that puts a service in which we all depend on for a living at risk?

One case that had some repercussions in Portugal was the delay in the placement of secondary school teachers in 2004 due to a software problem. However, on 30 September of that year, an article would appear in the Público newspaper reporting that a small company had finally solved the problem with a new algorithm, which was “completely conceived in six days and was based on very solid mathematical principles” as mentioned by one of the company’s young employees at a press conference. This was how the Ministry of Education was able to disclose the lists of professors online, two days ahead of schedule when, a week earlier, it announced that teacher placement would be done again manually after the existing software collapsed.

What the article does not mention is that the “very solid mathematical principles” with which the young company solved the problem were the so-called “programming formal methods” – precisely the main theme of October’s congress in Porto. Such methods have been taught in some Portuguese Universities since the 1980s, namely in Lisbon, Minho and Porto.

Fifteen years later, it is with some astonishment that the teaching of these “very solid mathematical principles” was not extended as it should have, while academics prefer to teach more empirical (but unreliable) methods because they are more accessible to the majority of students – a phenomenon that it is not exclusive to Portugal.

The result is frustrating, as the need for secure and reliable software is now higher than ever, in every domain and on a scale that would have been unthinkable a few years ago, we have the backbone of the programming resources weakened and expensive. It’s expensive because making mistakes, even if it doesn’t result in a disaster, involves extra costs. And this is, to some extent, the result of the voracious need of always having more programming resources.

Thirty years after 1999, the third edition of this FM’19 congress will be held in Porto, with the theme “The Next 30 Years”. INESC TEC’s High-Assurance Software Laboratory (HASLab) and the University of Minho will be responsible for the organisation of the congress. Both were invited by the International Association Formal Methods Europe (FME), which promotes this series of scientific events.

In a gallery of reputable guest speakers, it will be our pleasure to have Tony Hoare with us, the Turing award that most programmers know for inventing a famous quicksort algorithm. But its activity in promoting a true programming science goes far beyond that. It will be at the Porto’s congress that Tony Hoare, who, despite his 85 years, remains active in research, will give a talk that will mark the exact 50 years (October 1969) of the publication of his famous paper “An axiomatic basis for computer programming”.

This paper is at the origin of a method that, over time, would end up being called “Hoare logic” and which was, in fact, the one used by the young computer scientists who, in 2004, almost miraculously solved the problem of the teacher placement in Portugal. But the question that arises is the one that is implicit in the motto of Porto’s congress, “The Next 30 Years”.  The rapid growth in IT diversity and complexity has been challenging for the formal methods community, which has been adapting, generalising, and improving the models and analysis techniques that were the focus of previous congresses. The theme of FM‘19 is a reflection on where the community has come from and the lessons that we can learn from this evolution in order to better understand and develop software in future technologies.

Everyone is welcome to visit FM’19 in order to take part of this reflection!

The researcher mentioned in this news piece is associated with Universidade do Minho.