Tutti i programmi hanno dei bug. Non è possibile scrivere un programma senza bug. E più e grande il programma, più righe di codice ha, più aumenta il numero di bug presenti. Queste sono convinzioni che molte persone condividono. Peccato (si fa per dire!) che siano sbagliate.

Quando avete letto o sentito l’ultima volta che una centrale nucleare sia andata in palla per un problema informatico? Lo avete mai sentito? No? Ebbene, (non) avete sentito bene. Non è mai successo. Le centrali nucleari sono andate in palla, diverse di quelle, ma per altri problemi, non quelli informatici. Il problema principale notoriamente sta tra la sedia e lo schermo/tastiera.

Quando avete sentito o letto l’ultima volta che un’apparecchio medico ha ucciso un paziente per problemi di difetti di progettazione informatica? Non avete mai letto ne sentito? Ebbene, era successo, eccome, ma quei casi hanno portato come conseguenza le leggi che imponevano/impongono restrizioni e rigidi controlli formali del codice, affinché i casi come queli non si ripetano.

Come si fa a fare verifiche formali del codice? Stiamo preparando diversi corsi inerenti a questi argomenti (qualcosa potete già visionare seguendo il collegamento indicato) e aziende ed enti interessati potrebbero far bene a seguire questa pagina, come anche il nostro indice generale. Presto questi corsi saranno aggiunti al listino. Nel frattempo, di tanto in tanto, conviene anche dare un’occhiata alla nostra sezione delle conferenze, sempre sulla pagina dell’indice generale. Presto ci saranno anche lì delle novità.

Questa pagina, però, è dedicata a un sottoinsieme di conoscenze propedeutiche per implementare programmi privi di difetti (a questo servono le menzionate verifiche formali) e in particolar modo ai sistemi di logica formale da utilizzare nei programmi per verifiche formali del codice.