История изменений

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

Зачем тебе с динамикой теги? Их смысл чтобы к информации о типе бесплатно прибавлять информацию о свойствах.

Тут вообще несколько тредов разговора, конкретно этот о том, что динамика это частный случай статики, где сущесивует один universal type, описывающий физическую структуру значения/ркфлексивный обьект, называй как хочешь, а система типов в этом динамическом языке реализуется поверх этого обьекта (как и сделано в RTS этого языка).

Ну вот вопрос в том, что нетривиального можно доказать. Вот если бы моно было бы как-то просто доказывать что ф-я сортировки сортирует - наверное, было бы достаточно полезно, но оверхед от зависимых типов - реально ужасен и реально проще написать свой легковесный верификатор под задачу.

У меня не было опыта с созданием систем требующих нетривиальных доказательств, а игрушечный пример приводить не хочется. Всякий порядок локов, да реализация байндингов к рантайму динамического языка с вытаскиванием информации в type level же не в счёт (доказывается тип возвращаемого значения исходя из входящих и убираются лишние рантайм проверки)?

Ну и кроме того асбстракция, ООП и подобные вещи со статикой не связаны, но решают задачи получения гарантий корректности лучше статики.

Не уверен.

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

Зачем тебе с динамикой теги? Их смысл чтобы к информации о типе бесплатно прибавлять информацию о свойствах.

Тут вообще несколько тредов разговора, конкретно этот о том, что динамика это частный случай статики, где сущесивует один universal type, описывающий физическую структуру значения/ркфлексивный обьект, называй как хочешь, а система типов в этом динамическом языке реализуется поверх этого обьекта (как и сделано в RTS этого языка).

Ну вот вопрос в том, что нетривиального можно доказать. Вот если бы моно было бы как-то просто доказывать что ф-я сортировки сортирует - наверное, было бы достаточно полезно, но оверхед от зависимых типов - реально ужасен и реально проще написать свой легковесный верификатор под задачу.

У меня не было опыта с созданием систем требующих нетривиальных доказательств, а игрушечный пример приводить не хочется. Всякий порядок локов, да реализация байндингов к рантайму динамического языка с вытаскиванием информации в type level же не в счёт (доказывается тип возвращаемого значения исходя из входящих и убираются лишние рантайм проверки)?