p
Т-34 85
И всё это жутко тормозит
Ну , думаю можно так ограничить завтипы чтобы их можно было zero cost оптимизировать
Size: a a a
2020 May 21
DS
Т-34 85
И всё это жутко тормозит
Нет, потому что лишь верификация делается на языке с зав типами, код на чём угодно
p
Нет, потому что лишь верификация делается на языке с зав типами, код на чём угодно
Не понял предложения
Т8
Нет, потому что лишь верификация делается на языке с зав типами, код на чём угодно
А где гарантия, что перенесён код на конечный язык корректно?
G
Т-34 85
Завтиповые микросервисы, завтиповое ядро ОС...
Второе есть уже
DF
Хде?
Т8
Второе есть уже
И это реально юзают?
G
Т-34 85
И это реально юзают?
Конечно нет. Это исследовательский проект.
G
Т-34 85
А где гарантия, что перенесён код на конечный язык корректно?
Да, где???
Т8
Конечно нет. Это исследовательский проект.
Ну, по приколу можно что угодно соорудить
G
Т-34 85
Ну, по приколу можно что угодно соорудить
Например мои анонимные макросы!
G
Анонимные макросы реализованы! Использование:
Выдаёт
Теперь рассмотрим как это работает.
Затем макрос
Говоря словами, лямбда-макрос - это просто список, ненужные элементы которого игнорируются, части тела остаются неизменными, а аргументы подставляются.
EXEC_MLAMBDA(MLAMBDA(ARG + ARG), 1)
Выдаёт
1 + 1, как и ожидалось.Теперь рассмотрим как это работает.
MLAMBDA(ARG + ARG) раскрывается в:((_0, _1 ),(poica_pri_arg, _0, _1),(_0, _1),( + ),(poica_pri_arg, _0, _1),(_0, _1),( _0, _1))
Затем макрос
EXEC_MLAMBDA к каждый элемент списка применяет к другому макросу, перегруженному по кол-ву аргументов. Так происходит подстановка:(_0, _1) - <пробел>(poica_pri_arg, _0, _1) - раскрывается во второй аргумент EXEC_MLAMBDA(X) - раскрывается в XГоворя словами, лямбда-макрос - это просто список, ненужные элементы которого игнорируются, части тела остаются неизменными, а аргументы подставляются.
S
Ну , думаю можно так ограничить завтипы чтобы их можно было zero cost оптимизировать
в общем случае невозможно вроде
p
в общем случае невозможно вроде
Хз я пока не изучалтот вопрос
G
в общем случае невозможно вроде
Си тоже нельзя скомпилировать)
p
Если есть чё почитать, почитаю с удовольствием
DS
Т-34 85
А где гарантия, что перенесён код на конечный язык корректно?
Там, насколько я знаю, используются плагины, которые автоматически переносят спецификации, которые необходимо доказать, из си в утверждения на языке с зав типами
S
Си тоже нельзя скомпилировать)
эмм аа что
G
эмм аа что
Потому что макросы Тьюринг-полные
Т8
Ну , думаю можно так ограничить завтипы чтобы их можно было zero cost оптимизировать
Мне кажется, что даже если так, писать код на таком языке будет некому. Слишком сложно!