AZ
вспомни, разворот списка доказывается в 10 строчек. А тестов надо миллион
Size: a a a
2020 June 06
AZ
и то без гарантий
AZ
а тесты ты хуяк хуяк, и ты точно знаешь что на определенных значениях программа работает как надо, остальное в 99% случае выводится правильно
ох уж эти любители хуяк хуяк
AZ
Я смотрел одну вводную лекцию мужика, который занимается формальной верификацией. Он говорил, кажется, что некоторые вещи лучше покрыть тестами, чем доказывать. А некоторые тесты покрывают доказательства
просто некоторые вещи заебешься доказывать. НО то что можно доказать - лучше доказывать
AZ
это как "можно же написать тест, что только инт передается"
AZ
ну вот верификация нужно в ракетостроении например. для банка/круда она нахуй не нужна.
лол, конечно нужна
AZ
в банке так особенно
DB
просто некоторые вещи заебешься доказывать. НО то что можно доказать - лучше доказывать
Об этом бесполезно говорить, пока кто-то не написал что-то реально большое на том же идрисе и не заебался
AZ
то есть можно допустить баги если ты нахуячишь приложение в срок
если ты допустишь баг из-за которого миллирад бачей проебутся то тебя немного трахнут
AZ
Об этом бесполезно говорить, пока кто-то не написал что-то реально большое на том же идрисе и не заебался
можно писать на идрисе как на хаскелле + парой дополнительной фич
AZ
а на хаскелле прилично крупного софта, тот же ghc
DB
можно писать на идрисе как на хаскелле + парой дополнительной фич
Без вывода типов? Спасибо не хочу
DB
Хаскель крута, знаю
DB
А Идрис сомневаюсь
AZ
Меня смущает только ваше восхищение зависимыми типами, пока не написано больше, чем умножения матриц. Куда ни глянь про зависимые типы: у нас тут можно списки конкатенировать. Ну охереть. Ещё что? Или мы целый язык пишем, чтобы хед на пустом списке не вызвать?
меня смущает ваше восхищение борровчекером, пока не написано больше, чем возврат string_view из функции
p
Зачем? Все же продажное
потому что родители сказали надо🤷♀️
AZ
Без вывода типов? Спасибо не хочу
без какого вывода типов?
VS
(Но нацистская культура Германии мне интересная)
Хм, хз как культура а их самих я призираю. Гитлер слабак который обоссался от страха и застрелился. Сами нацисты слабаки которых раком советы поставили и поимели. Ну нафиг. Спектакли ставили как чувака с со свастикой другой чувак с красным серпом и молотом пинками под зад гоняет по сцене. Ну его нафиг. Атрибутика проигравших неудачников же.
DB
потому что родители сказали надо🤷♀️
Тру модернист. Учоба нинужна, но родители сказали
p
вспомни, разворот списка доказывается в 10 строчек. А тестов надо миллион
ага и сколько нужно времени было чтобы его доказать? хирролот так и не справился без подсказок.