AG
мне хватает конкаренси пруфов по работе и двух сайдпрожектов по логике :)
Size: a a a
2020 December 15
A
я давно забил уже
лучше водки выпить с мужиками возле гаражей!
A
мне хватает конкаренси пруфов по работе и двух сайдпрожектов по логике :)
ну или так
AG
еще и деревья вертеть на конкурсе для души уже не охота
AG
лучше водки выпить с мужиками возле гаражей!
скорее вермута с женой на кухне
AG
ну или с профессорами в баскской харчевне, но чота уже третий месяц никак не соберемся для этого :)
AG
то один затемпературит, то у другого дедлайн подгорает
NI
мне хватает конкаренси пруфов по работе и двух сайдпрожектов по логике :)
А вы там не затеваете на CoQ (или даже Idris) описание низкоуровневой части ATS?
Получилось бы заметно покруче Ivory, хотя и Haskell некоторые преимущества даёт.
(5 языков упомянул!)
Получилось бы заметно покруче Ivory, хотя и Haskell некоторые преимущества даёт.
(5 языков упомянул!)
AG
не, мы "реальным" ничем пока не занимаемся
AG
сейчас научник сочиняет конструктивную теорию для доказательств линеаризуемости через ЧКМ историй
AG
а постдок наш копает методы для не-линеаризуемых алгоритмов
AG
я лично немного поковырял локфришню на расте и теперь задумался про то, можно ли нашей логикой доказывать что-то в сеттинге слабой памяти
AG
потому что пока там всё предполагает как минимум sequential consistency
AG
а как максимум собственно линеаризуемость :)
AG
вообще в следующем году надо наверное будет заняться поплотнее мультикор окамлем и экстракцией в него
AG
но там засада в том что он тоже предполагает слабую память
NI
Что ж они все такие? ;-)
AG
ну это известная проблема
AG
что всё железо любит вращать порядок инструкций
AG
уже не один десяток копий в PL сломано на тему, нужно ли вообще программисту открывать доступ к этому факту, или это по сути сломанная абстракция