AG
пруверам примерно столько же лет сколько и япам
Size: a a a
2020 December 04
VD
Я про мейнстримные всякие
к
как?
ну
data I where
0 : I
1 : I
p : 0 = 1
такая странная сфера одномерная
data I where
0 : I
1 : I
p : 0 = 1
такая странная сфера одномерная
VD
Тут вроде только недавно foo != null стало протекать в тело ифа, а вы тут уже вон чо обсуждаете
VD
А до сих пор делают новые языки где null есть
AG
теория А в куррикулуме не даёт расслабиться
AG
заставляет из подсознания обмазываться нуллами и циклами
DB
Я про мейнстримные всякие
кок довольно мейнстримный прувер, и он в 2 раза старше меня
AG
ты 2000 гр?
DB
ты 2000 гр?
2001
к
Чому до этого никто матаны в языки не пытался тащить?
надо понимать что тут речь не про языки программирования
VD
кок довольно мейнстримный прувер, и он в 2 раза старше меня
Ну пруверы же не general purpose language, не?
DB
Ну пруверы же не general purpose language, не?
а в дженерал пурпус оно и не надо, наверное
VD
надо понимать что тут речь не про языки программирования
А idris не прувер считается?
к
кубики всякие и не претендуют на то чтобы быть языком для программирования, это языки для прувинга чего-то что описывается формально
к
я не могу найти где я это видел
к
но идрис себя хочет позиционироваться как язык
к
который именно что для вэлью
к
но с завтипами
VD
а в дженерал пурпус оно и не надо, наверное
Ну вот лямбды вроде тоже были не нужны. И ADT. И чего-нибудь еще пока не нужно >_>