JIT не указывает какой вариант правильный — это раз. JIT не модульный по построению — это два. 😊

JIT может обнаружить что класс из сборки sealed и девиртуализировать вызов

Я знаю. Это всё ещё не модульный анализ. Кроме того, какое это отношение имеет к корректности?

ну Вы же про девиртуализацию начали)

Но интересные противоречия начинаются уже на уровне банального переопределения методов в ООП: если мы девиртуализируем вызов благодаря whole program analysis в случае компиляции приложения вместе с библиотекой, то добавление подклассов в новой версии библиотеки уже ни на что не повлияет без перекомпиляции всего вместе снова. А если не девиртуализируем, то добавление подкласса в библиотеке в будущем сможет что-то сломать в нашем коде. Что правильно — я вообще не знаю. 😃

А каким образом добавление подкласса в библиотеке в будущем может что-то сломать?

Обычным образом: благодаря dynamic dispatch стал вызываться метод из подкласса, а там сломали инварианты, на которые мы рассчитывали. 🤷‍♀️

ну это наверно всё таки проблема семантики этого метода и сути изменений сделанных автором библиотеки

В языке Unison, очевидно, такой проблемы быть не может, поскольку все функции идентифицируются и связываются по хешам от AST. По факту семантика версионирования становится частью языка (хотя функциональная семантика всё ещё остаётся "за кадром" — зав. типов и прочих доказательств там нет).

то что будет с использующая её ранее внешней библиотекой?..

https://grosskurth.ca/bib/1997/cardelli.pdf
"Program Fragments, Linking, and Modularization" Luca Cardelli.

Статья поднимает вопрос корректности раздельной компиляции и линковки, и потому — я считаю — обязательна к прочтению для всех авторов языков программирования! 😃

Уже во введении на простейшем примере создания воображаемой программы, состоящей всего из двух модулей, разрабатываемых независимо, автор иллюстрирует, наверное, все проблемы, при этом возникающие. Между делом Карделли упоминает публичные репозитории артефактов (типа Maven Central или Nuget. Напомню, что статья опубликована в 1996 году!). Многие из обозначенных проблем линковки раздельно скомпилированных модулей до сих пор не решены ни в мейнстримных, ни в исследовательских языках.

В качестве основного результата Карделли предлагает, вероятно, первую формальную модель раздельной компиляции и последующей линковки, позволяющую строго рассмотреть вопрос о корректности этих процессов. Корректность в этом смысле приведённой простейшей системы модулей для просто типизированного лямбда-исчисления (в качестве модельного языка) формально доказывается. Автор, конечно же, указывает на необходимость расширения модели как в сторону более развитых языков (параметрический полиморфизм, ООП), так и в сторону более сложных систем модулей (параметризованные модули, "функторы" в духе Standard ML, первоклассные модули). Существуют ли такие работы, непосредственно продолжающие это исследование, мне не известно.

Однако, в качестве related work и дальнейшего чтения могу указать на работы по формализации (и доказательству корректности) раздельной компиляции для языка C в рамках проекта CompCert.

#separatecompilation #linking #modules #stlc

Может быть это стоит перевести и выложыть, ну к примеру, на хабр?

https://grosskurth.ca/bib/1997/cardelli.pdf
"Program Fragments, Linking, and Modularization" Luca Cardelli.

Статья поднимает вопрос корректности раздельной компиляции и линковки, и потому — я считаю — обязательна к прочтению для всех авторов языков программирования! 😃

Уже во введении на простейшем примере создания воображаемой программы, состоящей всего из двух модулей, разрабатываемых независимо, автор иллюстрирует, наверное, все проблемы, при этом возникающие. Между делом Карделли упоминает публичные репозитории артефактов (типа Maven Central или Nuget. Напомню, что статья опубликована в 1996 году!). Многие из обозначенных проблем линковки раздельно скомпилированных модулей до сих пор не решены ни в мейнстримных, ни в исследовательских языках.

В качестве основного результата Карделли предлагает, вероятно, первую формальную модель раздельной компиляции и последующей линковки, позволяющую строго рассмотреть вопрос о корректности этих процессов. Корректность в этом смысле приведённой простейшей системы модулей для просто типизированного лямбда-исчисления (в качестве модельного языка) формально доказывается. Автор, конечно же, указывает на необходимость расширения модели как в сторону более развитых языков (параметрический полиморфизм, ООП), так и в сторону более сложных систем модулей (параметризованные модули, "функторы" в духе Standard ML, первоклассные модули). Существуют ли такие работы, непосредственно продолжающие это исследование, мне не известно.

Однако, в качестве related work и дальнейшего чтения могу указать на работы по формализации (и доказательству корректности) раздельной компиляции для языка C в рамках проекта CompCert.

#separatecompilation #linking #modules #stlc

Я бы хотел заняться этой работой, но мое понимание недостаточно. Ближе к середине статьи я теряю ход рассуждений. Может ли кто-то помочь?