G
В Идрисе вычисления на уровне типов хорошо, в F* не знаю как с этим, но предполагаю, что похуже
Size: a a a
2020 March 24
NL
Спасибо, возьму на заметку.
G
В F* ещё интересна система эффектов, когда можно указывать вид вычислений, которые делает функция. Таким образом,
ML Int - функция делает I/O работу и возвращает Int, это без среды выполнения.G
Эффекты в иерархии и они композируются
G
КМК, очень красиво, что язык на системе эффектов и типов с уточнениями базируется
D
В плане эффектов интересна koka
NL
А в Idris эффектов разве нет? Я по сниппетам видел, что есть
Eff (чего-то-там), насколько они плохи?G
А в Idris эффектов разве нет? Я по сниппетам видел, что есть
Eff (чего-то-там), насколько они плохи?Есть, но их _можно_ использовать, а F* на них прямо базируется
NL
Есть, но их _можно_ использовать, а F* на них прямо базируется
А, понял, хорошо.
G
На главной странице так и написано - "Effectful verification system" или как-то так
G
В плане эффектов интересна koka
Может потом тоже пощупаю
G
Но туториал по F*, КМК, сложный, т.к. они не до конца всё объясняют и ошибки - не редкость
G
Например, мне до сих пор не до конца понятно что нужно пруверу Z3, чтобы доказывать леммы, неплох был бы конкретно по этому отдельный гайд
В
Пиздец еботня
Ну так если бы не это, то
И хопа, ub
let uniq = &mut ...;
let &a = &uniq;
let &b = &uniq;И хопа, ub
RP
Ссылка на ссылку на память не есть ссылка на память
p
Пиздец еботня
Угу. У меня из-за этого вся архитектура поплыла😊
G
Угу. У меня из-за этого вся архитектура поплыла😊
p
А все из-за того, что мне нужно дыа поля у структуры деструктуризировать
p
И приходится клонироватт
p
Чтобы у клона забрать первое поле