W dniu środa, 21 listopada 2018 22:28:05 UTC+1 użytkownik Maciej Sobczak napisał:
> > 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.

Co masz na myśli mówiąc o pre- i post-conditions?
Jaki język?

> 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.

To trochę takie pisanie palcem na piasku.
Jak byś przedstawił konkretne przykłady, to może moglibyśmy
spróbować podyskutować.

> > 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ę.

Nie ma żadnych szans. To jest risercz, i wcale nie udaje, że
próbuje być czymś więcej. Ale może można stamtąd wydobyć jakieś
wartościowe pomysły.