Здравствуйте, FDSC, Вы писали:

FDS>>> Есть ли язык программирования, в котором есть следующие фичи:
FDS>·>Да любой интерпретируемый или managed, например java
FDS>>> 1. Необходимо задавать невозможность вызова в модулях функций (запрет файлового ввод-вывода, например), исключая разрешённые модули
FDS>·>java.lang.SecurityManager
FDS>Нет. Насколько я понимаю, это не то.
FDS>Смысл в том, чтобы точно указать, что в этом файле нет вызовов определённых функций.

FDS>Для осуществления контроля. Грубо говоря, я запускаю какую-нибудь функцию компилятора и смотрю распечатку всех модулей, где такие функции разрешены (ввода-вывода).
FDS>Все остальные модули компилятор сам проверяет, что в них ничего такого нет.
В каком файле? В .exe? Тогда компилятор тут непричём. Ибо .exe после компиляции можно пропатчить, например.
SecurityManager же гарантирует, что если код захочет обратиться к запрещённым операциям, то кинется исключение.

FDS>Это нужно, чтобы случайно не допустить ошибку и проще было бы контролировать операции ввода-вывода.
Такое решается управлением зависимостями. Т.е. "эти файлы завият от этих библиотек. Вот списочек библиотек". Тебе останется проверить, что среди этих библиотек нет таких, которые делают ввод-вывод.

FDS>>> 2. Аналогичный запрет для всех функций, которые вызываются из данной функции
FDS>·>Запрет на уровне класса.
FDS>Как? Допустим, мне нужно точно сказать, что Class1 не осуществляет операций ввода-вывода.
FDS>то есть мне нужно, чтобы компилятор это проконтролировал. Причём так, чтобы я сам не задумывался, куда этот Class1 обращается.
Это происходит в runtime. Условно говоря, если Class1 (и любой код им используемый) пытается обратиться к java.io.File, то кастомизированный ClassLoader просто кинет ClassNotFound.

FDS>Представьте себе, что я пишу код не в одиночку, а вдвоём. Или кто-то проводит аудит безопасности моего кода.
FDS>Ему нужно дать возможность точно убедится, что какие-то функции не влекут за собой определённых действий.
FDS>В принципе, это можно делать строковым поиском по шаблону, но это нужно писать отдельный инструмент. И никто не знает, насколько он будет верен.
Поиск по шаблону ясен пень не работает. Особенно в случае если кто-то явно захочет запиахать в код скрытую уязвимость.
Например, в С/С++ даже если в коде нет неправильных действий, можно (случайно или нарочно) запороть буфер и осуществить переход по не тому адресу и оказаться не в безвредной функции вычисления длины строки, а в функции записи файла. Процесс верификации байт-кода в java запрещает это.

FDS>·>Это как? Если у некоего кода нет доступа к некоему состоянию, то и изменить не может, доступа к приватным данным тоже нет (кроме как через публичные методы). Или иммутабельные объекты что-ли?
FDS>У меня есть массив данных. Я его передаю в функцию вычисления хеша. Я хочу, чтобы этот массив не был изменён этой функцией.
FDS>Мало того, функция не должна изменять никаких объектов в программе, кроме создания и изменения новых.
Самый простой подход — защитная копия. Ты делаешь копию этого массива и передаёшь в функцию вычисления хеша. Даже если она что-то там поменяет, то пофиг, а к оригинальному массиву у неё просто не будет доступа, т.к. нет его адреса.
Как вариант — делать read-only интерфейс доступа к тем же данным. Т.е. у тебя будет
public int getSize() и public byte getData(int index) — и всё. Функция может только получить размер и взять значение, а что-то поменять — тупо нечем.

FDS>>> 4. Помечать объекты дополнительными типизационными метками (в статическом виде). Например, красная строка должна быть несовместима с зелёной строкой, но зелёная неявно приводима к красной.
FDS>·>А чем просто типы не устраивают? class RedString {private final String content;}
FDS>Представим себе, что я беру один символ красной строки и его помещаю в зелёную строку. Компилятор, в идеале, должен это отловить.
FDS>То есть он должен все производные данные пометить также красной строкой.
Сделать RedSymbol...

FDS>Плюс, нужно, чтобы можно было с гарантией видеть все приведения типов, чтобы их затем отдельно просматривать.
Не делать приведения типов. Делов-то.

FDS>·>Сборщик мусора же. Объекта либо нет, либо к нему доступа нет и деструкторы не нужны.
FDS>·>Все остальные кастомные состояния контролируются кодом публичных методов.
FDS>А если я ошибся или не написал контроль?
FDS>В этом-то и смысл. Я не хочу это делать руками. Я хочу, чтобы это было автоматизированно.
Типы же. Есть и другие механизмы, такие как capabilities, но я не в курсе, если хоть один популярный живой ЯП так умеет.

FDS>Плюс, у меня не должно быть сборщика мусора. Я как раз хочу уйти от него.
Это почему?