S tím naprosto souhlasím. Můj program dává deterministické výsledky, které se liší podle strict/lazy vyhodnocení. Je záměrně tak napsaný. To už je problém uživatele, že za správnou považuje jen tu strict variantu, i když obě dělají přesně to, co dělat mají. On totiž výsledek interpretuje až uživatel, z hlediska vykonávání programu je výsledek vždy správný, pokud nebudeme uvažovat chyby překladače apod.
No tak to právě není. Ty máš nějak specifikované zadání, to zadání přetvoříš do zdrojového kódu. U jazyků postavených na operational semantics se ptáš "zdroják + operational spec == zadání"? U Haskell se ptáš "zdroják == zadání"? No, a to neplatí.
Zkusím vysvětlit ještě jinak - ty jsi tvrdil, že přechod Strict -> Lazy může ten program rozbít. Tak když to přirovnám k matematice, tak ten přechod je prostě nějaká transformace kódu. No a Strict -> Lazy je třeba jako aplikovat na obě strany rovnice exp(), a Lazy -> Strict je jako aplikovat na obě strany rovnice log(). log() to může rozbít, pokud by se tam vyskytne negativní číslo. exp() to nerozbije.
No, jenomže tvoje rovnice někde obsahuje dělení nulou a je undefined. Což je za normálních okolností crash. Jenomže ten stroj jménem překladač to i tak začne podle Operational semantics vyhodnocovat (úplně stejně, jako je ten postup v tom příkladu výše), a pak samozřejmě dojde k nějakým výsledkům - třeba, že 0=1. nebo 0=10. Nebo 5=5. A ty sis zrovna vybral 5=5 a tváříš se, že program "funguje". A pak aplikuješ nějakou pragmu a on podle toho nedefinovaného zadání dojde k 0=1. Jenomže na základě zadání, které jsi mu dal, je tohle něco, k čemu klidně může aplikací standardních pravidel dojít.
Kokrektní program přechodem Strict->Lazy nerozbiješ - stejně jako žádnou rovnici "nerozbiješ", když na obě strany aplikuješ exp() (v R). Ale když aplikuješ log(), tak to rozbít můžeš, stejně jako při přechodu Lazy->Strict.