Odporuješ si. Pokud typem zajistíš, že nedojde k souběhu, a runtime to pak nedodrží tak jsi zase na začátku.
Říkal jsem, že
nevím, jestli je to vůbec možné, pomocí typového systému něco takového garantovat, popř. do jaké míry, zas tak moc do té teorie nevidím, o tom by se musel rozepsat asi spíš Radek...
Runtime musí dodržet sémantiku jazyka. Nemůže si dělat co chce. Může dělat cokoli, ale jenom tak, aby zachoval
význam programu.
Ono stačí prohlásit, že předpis je funkcionální, a už nesmí dojít k souběhu.
Já vlastně nevím, co tohle tvrzení říká. Asi bys to musel rozepsat víc formálně, abysme vůbec věděli, o čem je řeč.