MB
В зависимости от компилятора интерфейс борроучекера может выглядеть как
fn do_borrowcheck(full_program_text:String)->bool;
fn do_borrowcheck(full_program_text:String)->bool;
Size: a a a
2020 September 04
VB
Читал код борроу-чекера rustc'шного. Подверждаю, что @MikailBag все верно говорит. С выводом типов, кстати та же история. Там нет какого-то маленького набора постулатов, из которых все выводится. Растовые типы (как и борроучекер) - это огромный гигантский невиданных размеров список всяких спешл-кейсов, из которых и состоит весь их код. Любая попытка это формализовать будет не меньше собственно реализации
BV
Читал код борроу-чекера rustc'шного. Подверждаю, что @MikailBag все верно говорит. С выводом типов, кстати та же история. Там нет какого-то маленького набора постулатов, из которых все выводится. Растовые типы (как и борроучекер) - это огромный гигантский невиданных размеров список всяких спешл-кейсов, из которых и состоит весь их код. Любая попытка это формализовать будет не меньше собственно реализации
я про это пытался донести людям что описание про что-то без описания как это произошло бесполезно
T1
Борроучекер общается только с другими подсистемами компилятора. У него нет API для пользователя, поэтому непонятно какой интерфейс борроучекера предлагается стандартизировать.
Да какое апи пользователя тут? Интерфейс, ало. Программа может не скомпилироваться только из-за нарушений правил спецификации, и значит должна отвергаться и вторым компилятором (экстеншены не в счёт)
T1
Читал код борроу-чекера rustc'шного. Подверждаю, что @MikailBag все верно говорит. С выводом типов, кстати та же история. Там нет какого-то маленького набора постулатов, из которых все выводится. Растовые типы (как и борроучекер) - это огромный гигантский невиданных размеров список всяких спешл-кейсов, из которых и состоит весь их код. Любая попытка это формализовать будет не меньше собственно реализации
Ну то что формализация большая ничего не меняет это
VB
Ну то что формализация большая ничего не меняет это
В таком случае уже имеется подробная формализация на языке Rust
T1
В таком случае уже имеется подробная формализация на языке Rust
Ну и в чем проблема тогда?
VB
Нахуя углубляться в имплементацию, боже
ну, скажем, это ответ на этот вопрос
MB
Да какое апи пользователя тут? Интерфейс, ало. Программа может не скомпилироваться только из-за нарушений правил спецификации, и значит должна отвергаться и вторым компилятором (экстеншены не в счёт)
Борроучекер не ищет нарушения правил лайфтаймов.
Он ищет места, где он не может доказать корректность лайфтаймов.
И разные боррокчекеры доказывают корректность с разной степенью качества.
Так что в стандарте будет написано: "если программа не удовлетворяет правилам 1.8.1-1.8.10000000 (которые просто пересказывают исходники борроучеккра), то она должна быть отвергнута"
Он ищет места, где он не может доказать корректность лайфтаймов.
И разные боррокчекеры доказывают корректность с разной степенью качества.
Так что в стандарте будет написано: "если программа не удовлетворяет правилам 1.8.1-1.8.10000000 (которые просто пересказывают исходники борроучеккра), то она должна быть отвергнута"
MB
Ну и в чем проблема тогда?
А тогда возникает вопрос, нафига стандарт, если у всех компиляторов все равно будут общие кишки.
MB
Во всяком случае, нафига полный стандарт
T1
А тогда возникает вопрос, нафига стандарт, если у всех компиляторов все равно будут общие кишки.
Стандарт как раз таки нужен чтобы задекларировать эти общие кишки и чтобы пользователь знал что он ожидает от языка
VB
Вообще я тем не менее считаю, что спецификацию для раста неплохо было бы написать. Но в основном по той причине, что в процессе ее написания будет найдено бесчисленное количество костылей, которые будет вписывать в спецификацию настолько стыдно, что их заранее исправят
в🧇
Вообще я тем не менее считаю, что спецификацию для раста неплохо было бы написать. Но в основном по той причине, что в процессе ее написания будет найдено бесчисленное количество костылей, которые будет вписывать в спецификацию настолько стыдно, что их заранее исправят
😅
T1
Транслятор это лишь огромный инструмент который помогает запускает программы языков на современных компьютерах, а сам язык это огромная теоретическая куча, которая выходит за рамки информатики
T1
Вообще я тем не менее считаю, что спецификацию для раста неплохо было бы написать. Но в основном по той причине, что в процессе ее написания будет найдено бесчисленное количество костылей, которые будет вписывать в спецификацию настолько стыдно, что их заранее исправят
Естественно спецификация нужна, о чём тут речь может быть вообще
T1
Спецификация и будет определять сам язык, без неё никак
MB
Я думаю, что стандартизовать надо всякие модели памяти, unsafe code guidelines и так далее. Это реально и полезно.
в🧇
Спецификация и будет определять сам язык, без неё никак
"никак" это громко сказано, пока все живы вроде ¯\_(ツ)_/¯
T1
Нет, не нужно. По крайней мере если эти модели памяти довольно точные, а не поверхностые