Без заголовка

Я очень надеюсь, что и вы, и justy_tylor понимаете, что уже сейчас можно пользоваться тем, что вы оба только проектируете. Эта штука называется зависимые типы данных и доступна в Agda2, например. Ибо то, что вы описываете, свободно выражается в этой парадигме (при этом логическое программирование встроено в инструменты поддержки Agda2).