История изменений
Исправление Manhunt, (текущая версия) :
Такие инварианты должны быть частью типажа/класса типов.
чистый функциональный язык
Сейчас абстракции чаще всего специфицируют как набор сигнатур методов. Иными словами, описывают список сообщений, которые умеет принимать объект.
А мне кажется, что в идеальном мире абстракция должна описываться чем-то вроде (обобщенного/факторизованного) конечного автомата, у которого смена состояния происходит при вызове метода / получении сообщения. На этапе компиляции должна доказываться теорема о том, что реализация на самом деле ведет себя в соответствии со спецификацией. Это даст zero overhead в рантайме и оставит нам низкоуровневый императивный контроль над императивным железом.
Исходная версия Manhunt, :
Такие инварианты должны быть частью типажа/класса типов.
чистый функциональный язык
Сейчас абстракции чаще всего специфицируют как набор сигнатур методов. Иными словами, описывают список сообщений, которые умеет принимать объект.
А мне кажется, что в идеальном мире абстракция должна описываться чем-то вроде (обобщенного/факторизованного) конечного автомата, у которого смена состояния происходит при вызове метода / получении сообщения. На этапе компиляции должна доказываться теорема о том, что реализация на самом деле ведет себя в соответствии со спецификацией.