> Jinak, protože ve vyčíslitelnosti se nevyznám, zeptám se: když budeme uvažovat nějaký pořádný statický typový systém, o jak velkou třídu programů přijdeme, když nezkontrolovatelné věci prohlásíme za chybu? Čistě ze zájmu, já fakt nevím, ale odhaduju, že malá nebude.
Pokud si vystačíme s částečnou korektností programů (program nemusí skončit), tak z hlediska vyčíslitelnosti o nic nepřicházím*, protože stále tam mohu naprogramovat třeba rekurzivní funkce (s typy nebude problém, neboť mi stačí přirozená čísla) nebo odsimulovat Turingův stroj.
Pokud požadujeme i konečnost programů, tak tam už se omezujeme na obecně rekurzivní funkce, a to navíc ty, o kterých to umíme dokázat (resp. typechecker s naší pomocí). Tady už samozřejmě přicházíme o velkou třídu programů, ale myslím si, že v praxi je velmi často žádoucí, když víme, že program pro konečný vstup skončí.
* Pokud bych předpokládal, že má počítač neomezenou paměť.
