I januar 2019 var jeg til POPL2019-konferencen i Cascais; lige nu virker det som om det er mange år siden, men det er (i al fald lidt endnu) ikke længere siden end sidste år. Dengang købte jeg en bog af Adam Chlipala om bevisassistenten Coq og lovede mig selv og andre, jeg mødte til POPL2019, at jeg ville læse bogen og komme i gang med at bruge Coq. Men jeg anede ikke, at 2019 ville blive et usædvanligt hårdt år for mig og andre jeg har kendt godt, eller at 2020 ville blive et endnu hårdere år for hele verden. Så bogen blev stående på hylden, først et andet sted i et andet lokale i byen, senere på en reol i mit hjem.

Flere gange har jeg her forgæves lovet, at nu skulle der ske noget, men nogle gange er det første skridt det sværeste. I dag, da jeg endelig for alvor indså, at jeg vil komme til også at bruge de næste måneder næsten kun i selskab med mig selv og min familie, tog jeg Certified Programming with Dependent Types ned fra hylden – og kom i gang! Jeg har fået en anden computer og Coq er fremme ved version 8.12 nu, så der var nogle ting at opdatere. Det er godt at sidde og nørkle med noget helt konkret hinsides al verdens dumhed, nemlig definitioner, sætninger, beviser, programmer og typer, og det er dét, jeg holder af ved matematik og datalogi (selv om nogle sikkert ikke ville kalde det for konkret, selv om det er hvad det er).

Når det hele lysner en dag, både hvad angår dagslængden og pandemien, ved jeg forhåbentlig meget mere om Coq. Og jeg glæder mig til at gense Cascais og Portugal i det hele taget; jeg håber sådan at det vil lykkes mig i 2021.