A volte mi capita di iniziare un lavoro, dopo un po’ notare una qualche regolarità in quello che sto facendo, e pensare: «non avrebbe alcun senso proseguire imponendosi di mantenere questa regola che è emersa in maniera del tutto casuale dal modo in cui ho lavorato fino ad adesso… quindi facciamolo!». (Sì, lo so, sono un tipo un po’ strano.)
Nello specifico ci sono ricascato una decina di giorni fa, quando, dovendo riprendere un po’ di dimestichezza con il proof assistant (“assistente dimostrativo”?) Coq, ho deciso di leggermi il primo volume di Software Foundations. Per chi non lo sapesse (ovvero — a naso — il 99,9999% della popolazione mondiale), si tratta di un corso sui fondamenti logici della programmazione con la peculiare caratteristica di essere completamente formalizzato (nel calcolo delle costruzioni induttive, che è appunto la teoria implementata da Coq). Ah, e per la cronaca è anche (gratuito e) liberamente disponibile dal sito sopra linkato.
La cosa era partita, giovedì 18 Aprile, in maniera del tutto innocente, ovvero scaricando l’archivio con i sorgenti del libro, spacchettandolo e iniziando a leggere (e a fare gli esercizi incorporati nel testo). La domenica mi accorgo che, bene o male, stavo riuscendo a tenere il ritmo di un capitolo al giorno, compatibilmente con gli altri impegni che avevo. Per cui mi sono detto: perché non provare a continuare così fino alla fine? La settimana dopo ci sarebbe oltretutto stato il ponte del 25 aprile, quindi la cosa non sembrava completamente impossibile.
Per farla breve, i risultati li vedete nello screenshot qui sopra: tutto sommato direi che lo speedrun è effettivamente riuscito, con l’eccezione del capitolo IndProp che ha richiesto due giorni e peraltro, come potrà testimoniare chiunque abbia fatto il corso, contiene sostanzialmente il doppio del materiale del capitolo medio. (I capitoli in fondo, quelli che non ho modificato, sono opzionali, anche se conto di fare pure quelli.)
Ma gli esercizi, direte voi?
Quasi tutti ok, come si può notare dal resoconto qui sopra. (Il comando Admitted. è quello che si usa all’interno di una dimostrazione per dire a Coq «basta, non ne posso più, va’ a quel paese e fammi andare avanti». Più o meno.) Con l’eccezione di alcuni esercizi inutilmente noiosi su cui non sono stato a perdere tempo (in Induction e in Logic; i match in Basics sono spurii), gli unici che mancano sono in IndProp e in Imp, e riguardano comunque parti opzionali e/o addizionali (su cui comunque conto di ritornare con più calma).
Mica male, no? E adesso sotto con il volume 2, dove inizia la parte più interessante; ma stavolta senza vincoli di tempo, perché un bel gioco dura poco!