Ho già ricevuto diverse email sul nuovo font del blog. Secondo alcuni sarebbe «difficile da leggere»; secondo altri, più sinteticamente, «fa schifo». Il punto, però, è un altro: OpenDyslexic è un font concepito per facilitare la lettura alle persone dislessiche. Non significa che funzioni necessariamente per ogni persona dislessica, né che esista un font miracoloso capace di risolvere la dislessia. Significa soltanto che è stato progettato tenendo conto di alcune difficoltà che possono presentarsi durante la lettura. È successo che una persona dislessica mi abbia scritto per email. Mi ha detto che i post gli piacciono, ma che faceva molta fatica a leggere quelli più lunghi proprio a causa della dislessia.

Così ho deciso che perdere qualche punto percentuale di eleganza tipografica fosse un prezzo piuttosto modesto, se in cambio potevo aiutare concretamente una persona a leggere quello che scrivo. Era una cosa che potevo fare senza particolare fatica, e quindi ho deciso di farla.

A chi il nuovo font non piace rimangono comunque diverse alternative. Potete usare il vostro lettore RSS e scegliere il carattere che preferite, oppure iscrivervi alla newsletter, ricevere i post per email e leggerli con il font che volete.

Ma quando un essere umano chiede una mano, e quella mano gliela si può dare senza togliere nulla di sostanziale agli altri, gliela si dà. Se conoscete font migliori di OpenDyslexic, suggeritemeli.

Detto questo, comincio con l’autocompiacimento.

Sto scrivendo Xenomorph: un’istanza del Fediverso scritta in Ada/SPARK.

In passato mi avete sentito bestemmiare parecchio riguardo al fatto che ActivityPub sia uno standard scritto coi piedi, da persone che dovrebbero dedicarsi alla coltivazione dei cetrioli per uso interno.

Ed è vero.

Aktor era una fork di qualcosa che, nel corso degli anni, era riuscito a collezionare quasi tutte le stranezze consentite dal protocollo e, con quelle stranezze, a costruire qualcosa che funzionasse davvero.

Ma continuava a sapermi di resa.

E io non mi arrendo. Nessun ferrarese si arrende. Se ci fosse stato un ferrarese al comando, gli Alleati starebbero ancora cercando di conquistare Cona.

Anzi, torniamo ancora più indietro: probabilmente Alarico starebbe ancora cercando di attraversare il Po.

E quindi non mi sono arreso. Ho deciso invece di studiare come funziona un coso piccolo che funziona davvero, il cui autore, anziché aggiungere ogni possibile stravaganza prevista, tollerata o accidentalmente suggerita dal protocollo, ha seguito l’approccio opposto: ha tolto delle cose.

Sembra un metodo assurdo, specialmente nel software moderno, dove ogni problema viene affrontato aggiungendo altri tre framework, sette dipendenze e un orchestratore. Ma snac2 funziona. È piccolo, minimalista, non ha bisogno di un database ed è scritto in C.

Così, siccome il ferrarese non si arrende e, già che c’è, alza anche la posta, ho deciso prima di capirlo e poi di riscriverlo in Ada/SPARK.

Perché Ada/SPARK?

Ada, di per sé, è un linguaggio di nicchia. Viene usato soprattutto negli ambiti nei quali un errore non produce soltanto una schermata bianca o un ticket su Jira, ma può fermare un treno, compromettere un sistema aerospaziale o mandare fuori controllo un’applicazione mission critical.

Questo avviene principalmente per due ragioni.

1. Ada può essere un linguaggio estremamente sicuro perché è pedante. Il sistema dei tipi è severo, molti controlli sono incorporati nel linguaggio e il compilatore tende a rifiutare situazioni che altri linguaggi accetterebbero con entusiasmo, lasciando poi al programmatore il piacere di scoprirle in produzione.

Ma, se ci fermassimo qui, oggi si potrebbe rispondere: va bene, prendete Rust.

1. Ada dispone però anche di SPARK, cioè di un sottoinsieme del linguaggio accompagnato da strumenti di analisi e verifica formale.

Verifica formale significa che posso specificare, mediante precondizioni, postcondizioni, invarianti e altri contratti, ciò che una funzione può ricevere, ciò che deve produrre e quali proprietà deve conservare.

A quel punto GNATprove genera gli obblighi di prova e tenta di dimostrare matematicamente che l’implementazione rispetta quei contratti. Può inoltre dimostrare, entro il perimetro analizzato e sotto le assunzioni dichiarate, l’assenza di intere classi di errori a runtime: accessi fuori dai limiti, overflow, letture di variabili non inizializzate e altre amenità normalmente lasciate all’utente finale.

Non significa che basta scrivere una postcondizione e il computer, per educazione, la dichiara vera. Significa che il verificatore deve riuscire a dimostrarla. Quando non ci riesce, occorre modificare il codice, rendere più precise le specifiche, aggiungere invarianti oppure riconoscere che una certa proprietà non è stata dimostrata.

L’ecosistema Rust sta sviluppando strumenti di verifica formale come Kani, Creusot e Verus, e sarebbe assurdo fingere che non esistano. Ma si tratta ancora di strumenti differenti, con approcci e livelli d’integrazione diversi, che non costituiscono un ambiente unico e maturo paragonabile a quello costruito intorno ad Ada e SPARK.

Anche nel mondo Go esistono progetti accademici di verifica, come Gobra. Del resto Go ha finito per riscoprire diverse idee che un programmatore Ada trova familiari: semplicità deliberata, compilazione severa, concorrenza trattata come parte centrale del linguaggio e una certa ostilità verso le acrobazie sintattiche. Non direi che Go discenda direttamente da Ada, ma in alcuni punti sembra essere arrivato, per un’altra strada, nello stesso quartiere.

SPARK, invece, non è un esperimento appena uscito da un laboratorio universitario. Le sue radici risalgono a parecchi decenni fa; la generazione moderna, SPARK 2014, è disponibile da oltre dieci anni ed è impiegata nello sviluppo di software ad alta integrità e mission critical.

In altre parole, è un prodotto maturo.

Ed è precisamente per questo che ho deciso di usarlo per scrivere un server ActivityPub: perché, quando il protocollo è stato progettato da persone che sembrano considerare l’ambiguità una forma d’arte, l’unica risposta ragionevole è costruire l’implementazione usando un linguaggio che considera l’ambiguità un crimine.

---

Naturalmente, non tutto è matematicamente dimostrabile.

Se mando una richiesta a un server remoto, devo attraversare la rete, arrivare fino al server, ottenere una risposta e riceverla senza che qualcosa si rompa nel frattempo. Non ho un accidente di metodo per prevedere che cosa mi ritornerà il server, se risponderà davvero, se la connessione cadrà a metà o se, dall’altra parte, qualcuno abbia implementato ActivityPub consultando i fondi di caffè.

Quella parte del sistema rimane esterna, impura e sostanzialmente ostile.

Ma non ho bisogno di prevedere ogni possibile modo nel quale possa andare storta.

Posso decidere in anticipo che cosa considero una risposta accettabile.

Per esempio:

«Voglio una risposta HTTP entro un certo timeout, con uno dei codici che considero validi, un corpo entro una certa dimensione e un oggetto ActivityPub che rispetti le condizioni che mi servono».

Quella è la proprietà che mi interessa.

Tutto il resto può essere cassato con un unico verdetto:

«Non è ciò che volevo».

Non devo necessariamente distinguere, nel resto del programma, tra DNS fallito, connessione rifiutata, certificato scaduto, timeout, 404, 503, JSON deforme, campo mancante o server remoto posseduto dal demonio.

Posso anche distinguere questi casi, se mi servono per i log, per decidere quando ritentare o per produrre diagnostica. Ma questa è gestione operativa degli errori, non è il cuore della verifica formale. Il cuore della verifica è un altro.

Costruisco un wrapper che esegue la richiesta, applica i timeout, riceve la risposta e la sottopone a tutti i controlli necessari. Alla fine, il wrapper restituisce soltanto uno di due risultati:

«Sì: ho ottenuto esattamente una risposta appartenente all’insieme di quelle che considero accettabili».

Oppure:

«No: non ho ottenuto ciò che avevo richiesto».

A quel punto posso verificare formalmente che non esista una terza possibilità.

Il wrapper non può restituire al resto del programma un oggetto mezzo valido, un JSON parzialmente decodificato, una struttura inizializzata a metà o qualche avanzo radioattivo del parser. O produce un valore che soddisfa le condizioni stabilite, oppure dichiara il fallimento.

Non sto dimostrando matematicamente che Internet funzioni.

Sto dimostrando che il programma accetta soltanto ciò che ho definito formalmente come valido, e che tutto il resto viene respinto.

Questo è molto diverso dal tentativo di modellare ogni possibile disgrazia della rete.

La rete può fallire in un milione di modi, alcuni dei quali non sono ancora stati inventati. Non mi interessa elencarli tutti. Mi interessa dimostrare che nessuno di quei modi possa produrre accidentalmente un risultato che il programma tratti come buono. Il timeout fa parte dello stesso confine.

Non dimostra che il server risponderà entro il tempo previsto. Stabilisce che una risposta arrivata fuori da quel limite non appartiene all’insieme delle risposte che accetto. Dal punto di vista del contratto, è semplicemente un altro caso di:

«Non è ciò che volevo».

Lo stesso vale per i codici HTTP.

Posso decidere che, per una certa operazione, accetto soltanto 200 OK. Oppure 200 e 202. Oppure un insieme più complesso di codici, purché associati a un contenuto che soddisfi determinate condizioni.

Qualsiasi altra risposta viene respinta.

Non devo formalizzare filosoficamente la differenza tra un 401, un 429 e un 503, a meno che quella differenza non mi serva davvero. Per la proprietà che voglio dimostrare possono essere tutti ricondotti allo stesso risultato:

«La postcondizione richiesta non è stata ottenuta».

In altre parole, posso scegliere il risultato che voglio e trattare tutto il resto come mancato soddisfacimento del contratto operativo.

È precisamente questo che rende utile il wrapper.

Trasforma un universo incontrollabile di comportamenti esterni in una domanda binaria:

«Ho ottenuto qualcosa che soddisfa la proprietà richiesta?»

Sì oppure no.

Ed è questa riduzione a essere verificabile.

Lo stesso principio vale per la scrittura su disco.

Quando chiamo una funzione di scrittura non so davvero che cosa stia accadendo sotto di me. Posso essere su un disco locale, su NFS, su un volume fornito da Amazon, dentro una macchina virtuale o sopra una catena di cache che promettono tutte di essere affidabili con l’aria di chi sta per vendermi un’assicurazione.

Ma anche qui non devo modellare ogni possibile guasto.

Posso decidere quale risultato considero sufficiente.

Per esempio, posso stabilire che l’operazione abbia successo soltanto se:

il file viene scritto;

viene chiuso senza errore;

viene riaperto;

il contenuto viene riletto;

la lunghezza e i byte , o un hash, corrispondono a quelli originali.

Oppure posso confrontare un hash, se questo è sufficiente per la proprietà che voglio ottenere.

A quel punto il wrapper restituisce soltanto:

«Sì: il file è stato scritto, riaperto e verificato secondo i criteri stabiliti».

Oppure:

«No: non ho ottenuto quella proprietà».

Anche qui, non devo necessariamente esportare al resto del programma la differenza tra disco pieno, permessi insufficienti, mount NFS scomparso, errore di rete, file troncato o contenuto differente.

Posso registrarli separatamente, naturalmente. Ma per la logica verificata possono essere tutti un solo caso:

«Il risultato richiesto non è stato ottenuto».

La riapertura del file non dimostra che quei dati sopravvivranno per sempre, né che si trovino davvero su un supporto fisico non volatile. Dimostra una proprietà più limitata e molto precisa:

«Nel momento della verifica, ciò che ho riletto corrispondeva a ciò che volevo scrivere».

È questa la proprietà che il contratto deve esprimere.

Non bisogna promettere più di quanto il wrapper possa osservare. Ma non bisogna neppure promettere meno.

Se il wrapper si limita a controllare il valore restituito da write, potrà garantire soltanto che la chiamata ha dichiarato di avere accettato i dati.

Se chiude, riapre e confronta, potrà garantire qualcosa di più forte.

Se aggiunge una sincronizzazione, potrà appoggiarsi alle garanzie che quella sincronizzazione offre nel sistema concreto.

In ogni caso, la struttura logica rimane la stessa:

• definisco la proprietà che voglio;
• eseguo tutte le operazioni necessarie per verificarla;
• restituisco vero soltanto quando quella proprietà è stata osservata;
• riduco ogni altra situazione a falso.

SPARK non rende deterministici Internet, NFS o Amazon.

Permette di costruire un confine nel quale il programma dice:

«Questo è esattamente ciò che considero accettabile».

E poi dimostrare formalmente che soltanto ciò che supera quel confine può essere trattato come valido.

Il resto non deve essere compreso, catalogato o trasformato in una tassonomia bizantina degli errori.

Il resto è semplicemente:

«Non è quel che volevo».

---

Voi capite che aggiungere alla sfida anche la verifica formale, come se stessi scrivendo il codice dell’istanza federata destinata a girare sulla ISS, è una specie di «vedo e rilancio» che piace molto ai ferraresi etnici come me.

Non lo capisco?

Nessun problema.

Adesso lo capisco, lo ripeto con parole mie e, già che ci sono, ve lo dimostro pure.

Potete quindi immaginare il burst di autostima che sto ricevendo dal fatto che Xenomorph, a questo punto, stia federando correttamente.

Ho finalmente capito il codice di snac2. L’ho preso, l’ho smontato mentalmente, ne ho ricostruito la logica e l’ho ripetuto con parole mie: in Ada.

E siccome limitarsi a vincere sarebbe stato poco ferrarese, adesso sto anche umiliando l’avversario sconfitto mediante verifica formale.

Non snac2, sia chiaro, non era quello l'avversario.

snac2 ha fatto il suo lavoro, e lo ha fatto bene. Chapeau.

L’avversario sconfitto è ActivityPub: uno standard scritto coi piedi, che prima ho dovuto capire, poi tradurre in un linguaggio decente e infine costringere a rispettare dei contratti matematicamente verificabili. Insomma: prima l’ho capito.

Poi l’ho riscritto.

Adesso gli sto spiegando perché funziona.

Godi, troia.

---

Così ho deciso di vantarmene un po’.

Come si dice a Ferrara: «A fag tut mi».

Faccio tutto io.

Ricapitolando:

1. Ho adottato OpenDyslexic come font del blog, nel tentativo di rendere la lettura meno faticosa almeno per alcune persone dislessiche. Se conoscete un font sostenuto da prove più solide, possibilmente dimostrato efficace e non soltanto pubblicizzato come tale, fatemelo sapere.
2. Ho finalmente creato la mia istanza del Fediverso, alla faccia di quel protocollo austroungarico e ritardato che è ActivityPub.
3. Mi sento particolarmente bene per entrambe le cose, in un modo che soltanto i ferraresi possono capire davvero: quella soddisfazione un po’ autarchica che deriva dal guardare un problema, constatare che nessuno ha intenzione di risolverlo come si deve e concludere, serenamente, che toccherà fare tutto da soli.
4. Se vi ho incuriosito su Ada/SPARK, e volete scrivere codice certificabile per missili e aerei di sesta generazione, ecco QUI.

A fag tut mi, appunto.

E poi dicono.

---

UPDATE: DIETRO SUGGERIMENTO DI ALCUNI UTENTI, SONO PASSATO AD UN FONT IDEATO DAL BRAILLE INSTITUTE, DISTRIBUITO GRATUITAMENTE, ATKINSON HYPERLEGIBLE