nejako to nechapem. V com sa akoze dokazanost spravnosti programu zlepsila? (neberiem do uvahy kvalitu kodu). Transformaciou jedneho cyklu na iny? Ale mozno len nechapem dobre vasu ideu ale nevidim tam nejaky velky posun k celkovej dokazatelnosti programu (tj. lubovolny realny program ktory robi viac ako scitava 2 cisla)
