Ohjelmien oikeellisuus
Ohjelmien laatijoille sattuu tunnetusti virheitä.
Jotta voitaisiin olla varmoja siitä, että ohjelma todella tekee mitä pitää, ohjelma pitäisi todistaa oikeaksi.
Tämä on periaatteessa mahdollista (tietyin rajoituksin), mutta käytännössä hyvin hankalaa.
Formaalien oikeellisuustodistusten merkitys on lisääntymässä ”hankalissa” tai ”kriittisissä” ympäristöissä toimivien ohjelmien kohdalla (tietoliikenneprotokollat, reaaliaikajärjestelmät jne.)