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

No właśnie dowolny i to jest ich zaletą, bo koncepcję można dokleić do dowolnego
języka, również do rzeczy, które niekoniecznie byśmy od razu skojarzyli z językiem
programowania, np. opis maszyny stanów.

https://en.wikipedia.org/wiki/Precondition
https://en.wikipedia.org/wiki/Postcondition

Tu jest kilka przykładów w SPARKu, zobacz gdzie są i jaką rolę pełnią słowa Pre i
Post w tych przykładach.

Da się to nawet dokleić do języka C, patrz np. Frama-C.

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

Przykład jest taki, że światło na skrzyżowaniu może być czerwone, żółte, zielone,
żółto-czerwone albo migające. To jest zbiór wartości, daje się to opisać typem
wyliczeniowym.
Da się też napisać funkcję zmieniającą stan świateł albo zwracającą kolejny stan w
sekwencji, itp. Wiem, jak ładnie napisać system obsługujący np. szlaban na
przejeździe kolejowym przy użyciu takich pojęć jak pre- i post-conditions, po te
pojęcia nadają się do pracy z systemami, w których np. coś ma być spełnione żeby coś
mogło być po czymś. Tu pojęcia "przed" i "po" pojawiają się naturalnie i podobnie
jest w każdym innym systemie, dającym się opisać maszyną stanów (pralka, zmywarka,
skrzynia biegów, samolot, itd.).

Widziałem kilka teoretycznych przykładów z dependent types, ale żadnego praktycznego,
który mógłby pomóc w takich właśnie stanowo-sekwencyjnych systemach. A łaśnie takie
są w systemach krytycznych, bo przypadkiem ich krytyczność wynika z tego, że są
związane z procesami fizycznymi, w których jest czas a jak jest czas, to jest też
"pre" i "post".
Właśnie dlatego wsparcie dla "pre" i "post" w języku programowania jest czymś bardzo
cennym. Pytanie, czy dependent types cokolwiek tu jeszcze wnoszą, czego nie da się
pokryć samym "pre" i "post".

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