Brand
Informatica, Intelligenza artificiale, Interazione uomo-macchina, ICT

Teoria dei tipi come "sale" dei linguaggi di programmazione

Il progetto ha affrontato le sfide della programmazione di sistemi distribuiti, come i server bancari disseminati nel mondo che gestiscono i conti correnti in maniera trasparente rispetto alla locazione, proponendo soluzioni flessibili e affidabili per la progettazione del software di tali sistemi

Le infrastrutture software oggi includono sistemi complessi, auto-adattativi, autonomi e dipendenti dal tempo, caratteristiche che pongono nuove sfide per quanto riguarda la flessibilità e l’affidabilità delle applicazioni, due proprietà complementari, ma spesso in conflitto tra loro.
Il nostro progetto si è concentrato sulla proposta di soluzioni per la progettazione di un software flessibile e affidabile tramite l’utilizzo di sistemi di tipi.
La teoria dei tipi ha trovato un significativo campo di applicazione, soprattutto nell’ambito della progettazione dei linguaggi di programmazione. Si tratta di uno strumento che permette di dimostrare l’assenza di determinati comportamenti nei programmi (assenza di errori in fase di esecuzione, assenza di situazioni di stallo, ecc.).

Durante il progetto abbiamo ideato sistemi tipi che assicurano flessibilità e affidabilità del software di sistemi distribuiti per tre scenari di crescente complessità.
Primo scenario: consideriamo un negozio on-line dove acquirenti e venditori possono interagire seguendo le regole del negozio. Prima di impegnarsi in una transazione, i partecipanti negoziano le condizioni. I dati scambiati possono essere sensibili: tipicamente solo agenti certificati possono ricevere i numeri di carte di credito. Il sistema di tipi sviluppato nel progetto permette di verificare che il comportamento dei partecipanti non violi le regole del negozio e che i dati sensibili vengano protetti.
Secondo scenario: i comportamenti dei partecipanti possono essere diversi da quelli negoziati e possono violare le norme del negozio. Sono anche previsti cambiamenti delle norme stesse. Questo obbliga gli acquirenti e i venditori ad adattarsi a situazioni inaspettate. In questo caso il sistema di tipi progettato permette di controllare l’assenza di errori nella fase di riadattamento dopo le violazioni. Sono stati anche modellati meccanismi per la fiducia, la reputazione e le sanzioni, indispensabili per aumentare la fiducia dei clienti nel negozio.
Terzo scenario: la trattativa tra acquirenti e venditori del negozio on-line utilizza come criterio di base la soddisfazione individuale rispetto alle diverse alternative offerte; l’obiettivo è massimizzare la soddisfazione generale. I tipi sono evoluti in modo da riuscire a esprimere la soddisfazione dei singoli partecipanti.

L’impatto atteso a lungo termine è di favorire lo sviluppo di nuovi linguaggi e strumenti di calcolo per la programmazione delle interazioni nelle reti informatiche sfruttando i tipi per garantire la sicurezza, l’affidabilità e la flessibilità delle applicazioni progettate.

un racconto di
Mariangiola DEZANI
DIPARTIMENTO / STRUTTURA

Pubblicato il

09 gennaio 2017

condividi

approfondimenti

potrebbero interessarti anche