Stannproblemet Halting problem
Finns det en algoritm som givet vilken kod som helst kan avgöra om koden kommer att avsluta eller köra för evigt? Alan Turing (1936): nej, omöjligt. Klassiskt undecidability-bevis.
Bevisteknik: anta att Halt(P,I) finns; konstruera P' som kör Halt(P', P') och gör motsatsen → motsägelse. Konsekvenser för praktiken: statisk analys kan aldrig perfekt detektera oändliga loopar, undefined behavior, etc. Måste alltid använda heuristik + bound. Rice's teorem generaliserar: alla icke-triviala semantiska egenskaper av program är undecidable.