Stopprobleem
Bestaat er een algoritme dat van willekeurige code kan bepalen of die stopt of eeuwig doorloopt? Alan Turing (1936): nee, onmogelijk. Het klassieke bewijs van onbeslisbaarheid.
Bewijstechniek: neem aan dat Halt(P,I) bestaat; construeer P' die Halt(P', P') uitvoert en het tegenovergestelde doet, wat een tegenspraak oplevert. Praktisch gevolg: statische analyse kan oneindige lussen, undefined behavior en dergelijke nooit perfect opsporen en moet altijd op heuristieken en grenzen leunen. De stelling van Rice generaliseert dit: alle niet-triviale semantische eigenschappen van programma's zijn onbeslisbaar.