Теория тегированных (маркированных) объектов

В связи с классификацией объектных концепций вспомнил про Wyvern ... и deep-econom обрати внимание на статью A Coq implementation of a Theory of Tagged Objects  ... 

Почти синхронно (случайно) ... один из авторов, допускаю что, не плохой компьютерной системы акцентировал попытку обобщение своей практики вместо описания архитектуры и интерфейса - вот эта попытка - The Links Theory 0.0.2 и тоже с "притягиванием за уши" пруф-агента, перед этим была попытка "наводить тень на плетень" с помощью теории категорий.

В свзи с чем, посчитал необходимым сфопмулировать свое отношение к автоматизации интерпретации формальных систем ... Понравился комментарий здесь ... 

Как-то была попытка погружение в базы данных математических утверждений, позже можно будет здесь в комментариях добавить соответствующие ссылки. Любопытные проекты и, скорее всего, полезные ... Но верификации софта с помощью другого софта - это, как уже здесь замечено, просто очередная интерпретация, демонстрирующая аналогии, изоморфизм и прочее ... двух систем, их сравнение, но ничего более того ... Доказательство - это вычислительный процесс ... любая вычислительная система - формальная система ... со своей системой аксиом и правлами вывода ... Да сравнивать надо ... но для оптимизации и стандартизации ... Акиомы - банальные определения и можно было развивать совместно старый добрый Prolog, расширяя его сферу приложений, вместо того, чтобы генерировать новые системы, поддержка которых может быть заброшена вместе с амбициями их авторов, кстати (Implementation of a Proof Assistant in Prolog).

P.S. Начало создание постов вместе с интеллектальными ботами отложилось, в связи с этим эскурсом ... Но это тоже стоило того, акцентировать ещё раз вычислительный процесс, как символическое моделирование, кодификацию как классификацию и детерминацию, ещё проще говоря, ДЕФИНИРОВАНИЕ ... Определения, определение определений ... и так далее ... Ради утверждения МЕТАМОДЕЛИРОВАНИЯ! ... На пути к своему QED-манифесту! А ещё в сухом остатке тема POPLmark вызова ... а точнее её более точное выражение - ПРОБЛЕМА ВЫРАЖЕНИЯ!

Цель состоит в том, чтобы определить абстракцию данных, которая является расширяемой как в своих представлениях, так и в своих поведениях, где можно добавлять новые представления и новые поведения к абстракции данных, без перекомпиляции существующего кода и при сохранении статической безопасности типов (например, без приведения типов). Постановка проблемы выявляет недостатки в парадигмах программирования и языках программирования , и ... она все еще считается нерешенной ...