Я был бы признателен, если бы получил объяснения в процессе досконального разбора

^

Ну, это тогда лучше созвониться где-нить на неделе, в среду или пятницу, глядя на мой календарь...

Так-то формулы там начинаются с Simply Typed Lambda Calculus — это лучше бы знать заранее.

С другой стороны, видимо, для Хабра дальше введения читать и пересказывать и не нужно. 🤷‍♀️

Для хабра - может быть, но я бы хотел полностью понять статью, потому что сама эта проблема меня очень интересует. В частности я бы хотел распространить ее на динамическую линковку.

Технически я готов закрывать пробелы по мере их обнаружения, не считаясь с затратами, но нужен человек, который подскажет что изучать/читать и т п

Если Вы не знакомы с STLC, то начать можно с TAPL aka "Типы в языках программирования" Бенджамина Пирса.

Этого как я понимаю будет недосточно. Что читать следующим?

^

Да Вы начните — может, для этой-то статьи хватит, или даже запас останется. 😉

Звучит обнадеживающе, приступаю

Конкретно типы — и TAPL уж за компанию — можно обсуждать в отдельном чате: https://t.me/typeslife

спасибо, зашел

Кстати насчёт
> я бы хотел распространить ее на динамическую линковку

Во-первых, возвращаясь конкретно к статье Карделли, она Вам в этом не поможет: ещё раз напомню, что она была опубликована 15(!) лет назад, видимо, была первой на эту тему, поэтому рассматривает самый-самый простой сеттинг, какой только возможно. Поэтому она очень далека от реалий фактической (бинарной) линковки, хоть статической, хоть динамической.

Во-вторых, там рассматривается не столько линковка как таковая, сколько система модулей для ЯП, позволяющая (или не мешающая) компилировать раздельно и потом линковать "бинарно".

Вероятно, более актуальны работы по раздельной компиляции для проекта CompCert. Не помню, где читал, вероятно в "The next 700 compiler correctness theorem". Но там и степень "зубодробительности" формальных построений и доказательств выше порядка на два. Потому что реальность компиляции и линковки C устрашающе сложна.

Гм, я разобрался в том, как линкуются (статически и динамически) программы на С и ассемблере. Не то чтобы там было все "очень" сложно. Есть некоторые нетривиальности, но у них вполне объяснимые причины

Так что если Вы разрабатываете свой язык, желательно со своими же правилами и инструментами линковки — тогда Вы можете "постараться" и сделать весь "конвеер" корректным по построению. Если же Вы работаете с чем-то существующим (много лет), надежды что-то формально доказать почти нет.

Да, я разрабатываю свой язык и мне хотелось бы сделать его корректным "по построению", поддерживая возможность линковки в стиле Си (или что-то подобное).

Мне бы хотелось более точных ссылок, я боюсь закопаться в проекте CompCert

Ага, осталось "всего лишь" формально сформулировать что значит "корректность" для этого процесса, потом вывести (хотя бы) достаточные критерии для компиляции исходников, а дальше — "дело техники": доказать, что компилятор реально обеспечивает эти достаточные условия. 😉

Понимаю сложность проблемы.

Я же сослался на https://dl.acm.org/doi/abs/10.1145/3341689

Но до TAPL её читать скорее всего полностью бесполезно...