Typing avanzato per linguaggi di programmazione asset-aware

Error detection in programming languages has always been important in reducing bugs and vulnerabilities in programs and tools that help programmers in this task are crucial for the industry. Several kinds of error may occur in programs that can cause unexpected behaviours and lead to crashes. Fortunately, some of them can be detected using type systems and compilers. However, modern compilers may not be enough anymore: in fact, the range of mistakes that programmers may introduce is widely spread with the increasing complexity of today’s systems, such as blockchains. Languages for these environments should consider new classes of errors related to assets: in fact, in this context arbitrary duplication, creation or loss of assets should be avoided. These new kinds of error are strictly related to the concept of the state of objects, which are in blockchains smart contract instances. In this thesis, we discuss two typestated-oriented programming languages designed for smart contracts development, Stipula and Obsidian, and compare their expressiveness and main properties. In this analysis, we notice that Stipula adopts a safer and more flexible approach than Obsidian in legal contract writing, due to the primitives available for programmers. These features enable a simpler and more readable implementation of contracts and enforce a safer approach to development. On the other hand, Stipula lacks typical functionalities, such as user-defined data and data structures, that other object-oriented programming languages have: in particular, it does not support a full-fledged type system that ensures safety properties on asset operation. Then, an Obsidian implementation for currencies and tokens used in Stipula is provided and discussed in order to find hints to add in this new language ownership, which would help in error detection for asset references. Proofs that they are well-typed are provided: the tools used in these demonstrations give us some hints, especially on how ownership should work in Stipula statements. This thesis focused on the search for features and practises to improve the expressiveness of typestate-oriented programming languages. Obsidian is a statically-typed and typestate-oriented with careful attention to safety, security and usability. These features fall within the main goals of Stipula, a newborn typestate-oriented language for legal contracts. The insertion of such features in Stipula may be a good way to improve its safety and users’ experience.

La rilevazione di errori nei linguaggi di programmazione è sempre stata importante nel ridurre la presenza di bug e vulnerabilità del software e lo sviluppo di strumenti che aiutino i programmatori in tal senso sono cruciali per le aziende del settore. Nei programmi è possibile riscontrare diverse tipologie di errori che possono causare comportamenti inaspettati da parte del software o addirittura al crash. Fortunatamente, alcuni di questi errori possono essere individuati usando sistemi di tipi e compilatori. Tuttavia, i moderni compilatori potrebbero non essere più abbastanza: infatti, lo spettro di possibili errori introdotti dai programmatori si è molto ampliato insieme alla complessità dei sistemi informatici odierni, come ad esempio le blockchain. I linguaggi per questi ambienti dovrebbero considerare una nuova categoria di errori correlata agli asset: infatti, in questi casi la loro duplicazione, creazione o perdita arbitraria dovrebbe essere evitata. Queste tipologie di errori sono strettamente correlati al concetto di stato di un oggetto, il quale è un’istanza di uno smart contract. In questa tesi, vengono discussi due linguaggi di programmazione typestate-oriented progettati per lo sviluppo di smart contracts, Stipula e Obsidian, vengono messi a confronto in termini di espressività e proprietà. In questa analisi, si può notare che Stipula adotta un approccio più safe e flessibile di Obsidian nella scrittura di legal contracts, grazie alla disponibilità di determinate primitive di linguaggio. Queste funzionalità permettono una realizzazione più semplice e comprensibile dei contratti e costringe il programmatore a un approccio più safe nello sviluppo. D’altro canto, Stipula non possiede altre funzionalità, come tipi user-defined e strutture dati, tipiche dei linguaggi di programmazione a oggetti: in particolare, non supporta un sistema di tipi completo e che permetta di assicurare proprietà di safety per gli asset. Successivamente, viene fornita e discussa una realizzazione in Obsidian delle currencies e dei tokens usati in Stipula allo scopo di trovare un modo di aggiungere in questo nuovo linguaggio un sistema di ownership, il quale potrebbe aiutare nella rilevazione di errori per riferimenti ad asset. Vengono, dunque, fornite le dimostrazioni che gli statement presi in considerazione sono ben tipati: gli strumenti teorici usati nelle dimostrazioni forniscono effettivamente delle indicazioni su come l’ownership dovrebbe funzionare in Stipula. Questa tesi si concentra sulla ricerca di funzionalità e pratiche per migliorare l’espressività dei linguaggi typestate-oriented. Obsidian è un linguaggio staticamente tipato e typestate-oriented con una particolare attenzione alla safety, alla security e all’usabilità. Queste caratteristiche fanno parte anche dei principali obiettivi di Stipula, un nuovo linguagggio typestate-oriented per i legal contracts. L’inserimento di tali funzionalità in Stipula potrebbe essere un buon modo per migliorarne le proprietà di safety e l’esperienza d’uso del programmatore.