История изменений
Исправление fulmar_lor, (текущая версия) :
http://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/liquid-types/
Liquid Types are refinement types, that is types that are refined with logical predicates that cannot be arbitrary expressions (like dependent types) but are expressions drawn from a sublanguage.
Liquid Types are a constraint form of refinement types in that logical predicates come from a decidable sublanguage, that is a logical language for which implication checking is decidable. Examples of such decidable languages are quantifier-free theories as arrays, integer linear, set theory etc.
Т.е. можно руками не писать доказательства. Но язык спецификации сильно ограничен.
Исходная версия fulmar_lor, :
http://goto.ucsd.edu/~ucsdpl-blog/liquidtypes/2015/09/19/liquid-types/
Liquid Types are refinement types, that is types that are refined with logical predicates that cannot be arbitrary expressions (like dependent types) but are expressions drawn from a sublanguage.
Liquid Types are a constraint form of refinement types in that logical predicates come from a decidable sublanguage, that is a logical language for which implication checking is decidable. Examples of such decidable languages are quantifier-free theories as arrays, integer linear, set theory etc.