G
Сайшерп скорее
Почти одно и то же
Size: a a a
2020 May 23
p
DF
Почему сложнее?
KR
Хммм, да там плоскость целая, если не пространство
SP
Некоторые люди представляют статику как точку. На самом деле, это линия, где на левом краю - Java, на правом - Idris
но статика это плоскость. помимо корректности есть просто удобство
p
Формальная верификация не относится к типизации
G
Dollar Føølish
Почему сложнее?
Потому что доказательства. Если во всю орудовать доказательствами, проверифицировать всё, что от разработчика зависит, время разработки снизится. Тот же переворот списка, который на Хабре доказывали, даже статью написали. В то же время питоняга бы набацал за 30 секунд и ещё тесты 5 минут и пошёл дальше.
DF
Так не пиши док-ва кек
p
но статика это плоскость. помимо корректности есть просто удобство
ну тогда так наверное
DF
Пиши тесты на идрисе
G
Формальная верификация не относится к типизации
Относится. Посмотри на Coq, Idris. Там верификация на типах
DF
А,хотя понял , да
G
Dollar Føølish
Пиши тесты на идрисе
Зачем мне Идрис тогда?
p
Потому что доказательства. Если во всю орудовать доказательствами, проверифицировать всё, что от разработчика зависит, время разработки снизится. Тот же переворот списка, который на Хабре доказывали, даже статью написали. В то же время питоняга бы набацал за 30 секунд и ещё тесты 5 минут и пошёл дальше.
верификация в принципе не нужна
DF
Без пруфчека завтипы не сработают
G
+
SP
.headers()
.get(LAST_MODIFIED)
.and_then(|x| x.to_str().ok().map(|x| x.to_owned()));
понимаю почему хаскелисты горят от раста
p
p
вроде норм
p
не считая такого количества скобочек)