> Warto przyjrzeć się językowi Idris i typom zależnym.

Nie przekonują mnie. Jeśli je rozumiem, to typy zależne pozwalają związać warunki
między parametrami i wartością zwracaną z funkcji. Fajnie, ale to nie wyczerpuje
tematu, bo jest jeszcze stan (również globalny), który też mogę chcieć związać takimi
warunkami. Co więcej, takie warunki nie muszą mieć związku z typami - np. jedna
metoda w obiekcie może "obiecać" inne warunki końcowe, niż inna metoda, a przecież
nie jest tak, że typ obiektu jest różny w różnych metodach. Takie ograniczenie już na
poziomie terminologii wskazuje, że typy zależne to domena jakiejś niszy językowej (w
szczególności języków funkcjonalnych), więc od razu ma dla mnie ograniczoną
stosowalność.

Potrzebny jest inny formalizm. Pre- i post-conditions wydają się być bardziej
niekonfliktowym mechanizmem, tzn. możliwym do zastosowania bez niepotrzebnych
ograniczeń.

--
Maciej Sobczak * http://www.inspirel.com