PROMETHEUSS GRUP
WHO WE ARE
Members
Dr. Joost J. Joosten (mathematical logic, team leader)
Ana Borges (mathematical logic)
Joaquim Casals Buñuel (computer science)
Mireia González Bedmar (mathematical logic)
Dr. Eduardo Hermo Reyes (mathematical logic)
Dr. Moritz Müller (mathematical logic)
Eric Sancho Adamson (philosophical logic)
Aleix Solé Sánchez (philosophical logic)
CONTACT
Dr. Joost J. Joosten
University of Barcelona. Montalegre 6
08001 Barcelona, Catalonia, Spain
jjoosten@ub.edu
+34 9340 37984
PROMETHEUSS GRUP
Software unreliability and the legal system
Software malfunction can appear in one or several layers of the software development cycle, including: natural language specifications, technical specifications, formal specifications, coding, compilation, installation, and execution. The consequences of software malfunction in legal and administrative settings arguably imply the violation of legal principles, loss of valuable resources, attacks on civil rights (such as well-documented cases of automated racial discrimination), and degradation of legal systems. Also, in the future as well as in the present, it may aggravate the societal loss of confidence in technology and in government alike. Legally binding decisions taken based on data produced by software, or even decisions which are automated outright, very rarely acknowledge the existence of several crucial potential problems inherent to the nature of software.
Some striking legal challenges posed by software malfunction include: liability in the presence of software bugs, loss of legal certainty, loss of access to justice, loss of contestability, and, most common of all, de facto handing over the competence to interpret the law to legally-illiterate programmers. Software malfunction has been identified as one of the crucial challenges in addressing disinformation by STOA in its 2019 report for the European Parliament. (PE 624.278 – March 2019. pp. 40-42)
As society moves towards digitization, the problems inherent to software development eventually spill over into other aspects of the functioning of our society. Our team specializes in the crossover between the legal system and computer systems. More precisely, the research group is interested in those laws that are applied by means of software systems, that is, those laws that end up being translated into a digital language and executed by a computer. In these cases, due to the lack of control and the high probability that the programs contain internal errors, many potential problems emerge that can affect both the civil rights of individuals and companies and the proper functioning of the judicial system itself.
In this sense, formal verification of software can deal with a valuable part of these problems, from the elimination of internal bugs to ensuring the correspondence between the meaning of the laws and the instructions that programs are meant to execute.
Formal Verification of Software
Verifying software consists in ensuring that the software behaves according to its specification and that it does not contain coding errors, otherwise known as bugs. It is widely known and accepted throughout the software industry that any piece of software will most likely contain bugs. For most applications, the industry reduces bugs and mismatches between specifications and implementation by applying extensive testing and debugging. However, in many cases testing cannot feasibly guarantee correctness, since usually the amount of possible inputs or states of a piece of software is either infinite or finite but too large for exhaustive testing. Therefore, for a wide range of critical applications, including computable laws, obtaining a more reliable paradigm is paramount.
Our technique consists of using a powerful Type Theory that is expressive enough to write both algorithms and theorem statements. In particular we use the Coq proof assistant, where we can write the code, state and prove theorems about its correctness, and mechanically check that the mathematical proof is correct.
With these tools, one can reason about properties of programs with the same degree of certainty with which we prove mathematical theorems. This is an especially interesting and worthwhile technique for showing that a program is correct with respect to its specifications, as long as we can symbolize its specifications in a trustworthy manner in a type-statement.
Once the correctness of the program is proven, we can extract the code in a functional programming language (such as OCaml) and compile it. This results in a software with all the credentials of mathematical certainty: error-free software.
Industrial and Social Applications: Strategic Importance of Formal Verification
Obviously, a tool with the potential to ensure accuracy and lack of errors in a program is of great use to any industry sector. Therefore, critical sectors and large technology companies are increasingly interested in and investing heavily in the development and application of this programming paradigm.