Modern programming languages like Kotlin or Rust have advanced features to statically ensure data and memory safety, like nullable and ownership types. Other languages like C, Erlang, Go, Haskell, Java, or Scala, have static analysis tools to help the developer detect at compile-time possible safety violations that might lead to run-time errors. Most of these, however, force the developer to adopt a defensive programming style, trying to cover all possible scenarios where things might go wrong. Nevertheless, bad things still happen, being a testimony of this the Jedis bug uncovered after 9 years in Jan 2018 (issue closed 14 months later), or the MonoX Finance smart contract vulnerability exploited in December 2021. Since many applications implement protocols, as not all functionalities are available all the time (e.g., one can only pop from a non-empty stack; write in a not full buffer), behavioural types are a natural way to model and validate code enforcing that only the correct sequences of actions are allowed to happen. Static type systems ensure protocol compliance and, in some conditions, completion. Tools to use them with functional, imperative, or O.-O. mainstream languages are available, but still not widely adopted.

Idioma: Inglés

Requisitos: Familiaridad con lenguajes de programación. Idealmente, conocimiento de C, y algún lenguaje al estilo Java.