PS
Это теоритическая выгода, или кто-то уже так делает?
Компилятор Chlorophyll подобным образом устроен: https://www2.eecs.berkeley.edu/Pubs/TechRpts/2015/EECS-2015-121.pdf
Size: a a a
2020 January 05
AK
на мой взгляд это продажа солидных тормозов компиляции за + пару процентов оптимизации
Вот да, было ощущение что идея классная, но современные подходы/железо не позволяют это делать за вменяемое время
E
Компилятор Chlorophyll подобным образом устроен: https://www2.eecs.berkeley.edu/Pubs/TechRpts/2015/EECS-2015-121.pdf
не знаю почему, но я прочитал это как "Компилятор Чернобыль"
PS
не знаю почему, но я прочитал это как "Компилятор Чернобыль"
Заведомо обрекаете проект на неудачу? :) А авторы применили такие энергоэффективные оптимизации, что удалось железку с вполне практическим приложением запитать от единственной картофелины!
http://pl.eecs.berkeley.edu/projects/chlorophyll/
http://pl.eecs.berkeley.edu/projects/chlorophyll/
K
SMT ещё к выведению типов никто не прикручивал?
AK
Kir
SMT ещё к выведению типов никто не прикручивал?
Хочешь такой посмотреть тип переменной, наводишь на нее курсор и идешь пить чай пока солвер рожает? )
K
Не, SMT в качестве системы вывода типов при компиляции
AT
Kir
SMT ещё к выведению типов никто не прикручивал?
Сто лет в обед как прикручивали. Во-первых, Refinement Types: F*, Liquid Haskell.
AT
Во-вторых, я как-то студентам поручил сделать тайпчекер поверх Z3. 😄
E
Во-вторых, я как-то студентам поручил сделать тайпчекер поверх Z3. 😄
интересно, а я пузырьковые сортировки в университете писал :(
AT
Ещё есть Dafny, в которой тоже Z3, но без Refinement Types.
AT
интересно, а я пузырьковые сортировки в университете писал :(
Это пошло как диплом. Бакалавра, если не ошибаюсь.
K
Как оно работает-то? Ссылки есть?
K
Во-вторых, я как-то студентам поручил сделать тайпчекер поверх Z3. 😄
AT
AT
Там, конечно, весьма примитивный тайп-чекер.
AT
Лучше брать пример с Liquid Haskell или F*.
K
Всё равно, спасибо!
AT
Kir
Всё равно, спасибо!
Не за что. Кстати говоря, Вы знакомы с языком Nix? То, что Вы рассказываете очень мне про него напоминает...
YS
Kir
Во-вторых, я как-то студентам поручил сделать тайпчекер поверх Z3. 😄
лучше пользоваться функцией "ответить на сообщение"