X
ну я могу судить по примеру F*
Size: a a a
2021 November 16
BV
интересное отделение касты
BV
Гвидо емнип был больше математиком всё же
X
они взяли кусок ocaml — не самый лучший, если вы спросите меня — и начали вокруг него наворачивать нужные себе синтаксис и семантику
IN
имхо, если не учить итеративные языки программирования и сразу сесть за хаскель
s
В итоге на них доказывают обычно семантику языков и логик, корректность программ, и прочие подобные вещи.
BV
Джон Макарти тоже пхд по математике
IN
то рвотные рефлексы будут вызывать уже другие языки
X
(ну окей, может быть, предположение про не самый лучший кусок было некорректным в свете того, из чего вообще выбор)
s
Lean, кстати, сделал пару шагов навстречу математикам.
X
но у меня такое впечатление, что за все 5 лет совершенно некому было дёргать их за руки
X
решения по синтаксическим конструкциям — эстетически уродливые
X
решение, что все идентификаторы должны начинаться с малой буквы, и нежелательно кэмельКейсить (а надо_вот_так) — мягко говоря эстетически сомнительно
s
Добавив в язык аксиомы для фактор-множеств вместо того, чтобы мучить математиков сетоидами.
BV
рвотные рефлексы это не про иное мышление это про синтаксическую нестрогость языка
IN
а в хаскеле синтаксическая нестрогость?
X
решение, что автогенерированные имена конструкторов имеют вид `Mktype` (я не шучу, даже доски после Mk нет!) -- омг ребята алё
BV
да, там 100500 способов сделать казалось бы один и тот же набор действий
IN
в плюсах 18 инициализаторов, на секундочку
BV
тут мы говорим pure а рядом запилим нечто что будет давать возможность нарушать инварианты