W dniu poniedziałek, 19 listopada 2018 08:14:45 UTC+1 użytkownik Maciej Sobczak
napisał:
> > > Tak, to ważna obserwacja. Może da się te rzeczy rozdzielić?
> >
> > To następna obserwacja: jeśl wpływa to na runtime release należy to
> > odrzucić.
>
> więc odrzućmy. Niech sobie będą statyczne asercje oraz dynamiczne, ale sterowane
opcjami kompilatora.
>
> > Jest, ale w przypadku nadmiaru checkerów nie da się pisać czytelnie.
> [...]
> > Jednak dalej brakuje mi czegoś takiego jak int a<4-200>
>
> Czyli ogólnie: type invariants (niezmienniki typów). Wtedy warunek poprawności dla
danego typu opisuje sie w jego definicji i nie trzeba już zaciemniać kodu pisząc co
chwilę asercje, czy obiekt ma dobry stan. Tzn. zminimalizujmy zaciemnienie zbierając
je do jednego miejsca, z dala od algorytmu.
> Ciekawe, że wtedy można odróżnić niezmienniki typów (takie jak zakres zmiennej) od
niezmienników obliczeń (np. pętli) i wraz z tym rozróżnieniem dać im osobne miejsce w
kodzie. Przecież nie wszytko musi być klasycznym assertem.

Warto przyjrzeć się językowi Idris i typom zależnym. Twórca Idris, Edwin Brady,
opowiada tutaj o nim z humorem:
https://www.youtube.com/watch?v=zSsCLnLS1hg