Názor ke zprávičce Bezpečnostní audit TrueCryptu bude pokračovat od Lael Ophir - Nepotřebujete řešit halting problém. Potřebujete zaručit, že kód...

Nepotřebujete řešit halting problém. Potřebujete zaručit, že kód nemá vedlejší efekty. Například že konkrétní metoda nezasahuje do jiných dat, než vstupních a výstupních. Tohle a řada jiných věcí se dá ověřit kombinací vhodného jazyka a systematického strojového ověření zdrojáku.
Dá se to dokonce dovést tak daleko, že celý OS může běžet v jednom procesu, protože je formální verifikací ověřeno, že žádný kód nebude lézt kam nemá. Bohužel to stojí nějaký výkon, a vyžaduje to přepsání prakticky veškerého SW, takže si na to ještě počkáme.
http://research.microsoft.com/pubs/69431/osr2007_rethinkingsoftwarestack.pdf