Ещё пару вопросов насчёт выбора языка программирования.

Есть ли язык программирования, в котором есть следующие фичи:

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

2. Аналогичный запрет для всех функций, которые вызываются из данной функции

3. Помечать код как неизменяющий состояние программы

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

5. Контролировать состояние объекта как конечного автомата, в идеале, в статике. Грубо говоря, объект не инициализирован, объект инициализирован, объект в работе, объект завершил работу, объект подвергся деструкции.


F-star знаю, но его очень не хочется. Всё очень глючно, на костылях и очень сложно.