Třeba by se hodilo mít možnost porovnávat, zda dva kódy dávají vždy stejné výsledky. Dáte programátorovi za úkol zoptimalizovat/přepsat nějaký kód a pak jen snadno zkontrolujete, že tam přepsáním nebyla zanesena žádná chyba.
No jo, to je sice hezký příklad, ale opět dost nereálný. Už to tady taky zaznělo dřív: za prvé formální verifikace se dělá jenom u hyperkritických systémů*. Normální program, se kterým se setká normální programátor, stejně nikdo formálně verifikovat nebude. Nikoho by ani nenapadlo formálně verifikovat, že Linux 2.6.3 dává stejné výsledky jako Linux 2.6.1... (stejně jako u té složitosti se stejně nakonec dostaneme k tomu, že roli hrají úplně jiné věci - matematikou obtížně postihnutelné - jako různé interrupty apod.)
Za druhé když už je nějaký program tak jednoduchý, že je na něm reálné verifikaci udělat, stejně odhaduju, že se bude dělat častěji zase nějakým druhem heuristiky (patřičné invarianty a takové ty věci) než tím, že by to někdo přepisoval na normalizovaný Turingův stroj. Opět to bude spíš otázka aplikace nějaké metodiky, kterou vymyslela jedna geniální hlava a celý svět to jenom aplikuje.
A stejně, co se týče těch systémů, kde se to asi dělá (nějaké ty marsrovery apod.), tak tam samozřejmě lidi se špičkovými znalostmi teoretické informatiky mají nepochybně svoje místo - ale nijak to nedokazuje, že jich potřebujeme tisíc ročně. Možná tak jednoho a to ještě při bujné fantazii...
* dneska už i ty realtime systémy se afaik dělají spíš systémem heuristika + naddimenzovaný HW