> Nie wiem, czy to wyczerpuje temat, ale na pewno jest
> przykładem czegoś, co zwiększa ilość rzeczy, które możemy
> statycznie powiedzieć o naszym programie.

Zwiększa względem czego?
Względem w ogóle braku takich mechizmów? Tak. Jest to postęp.
Względem pre- i post-conditions? Nie widzę tego.

Mam wrażenie, że języki funkcjonalne za bardzo fiksują się na pojęciu typu. O ile typ
nadaje się do opisania dozwolonych stanów, to nie za bardzo nadaje się do opisania
przejść między stanami.

> Jest też język ATS (trochę protoplasta Rusta), który
> ma system "typów liniowych" służących do wyrażania twierdzeń
> o poprawności korzystania z zasobów. Ale wydaje się raczej
> trudny do używania:

Skoro jest trudny, to tym bardziej nie ma szans na rynkową akceptację.

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