VG
так как доказать что типы все покрыли то? это надо делить область определения функции на возможные куски, проверять что тип твой каждый учитывает, то же самое я могу просто на каждый кусок написать тест
Size: a a a
2020 May 08
G
Но блять нахуя тебе выносить код из рантайма в декларацию типа?
чтобы вынести код из рантайма с статическую фазу
M
Блять да не сможешь ты
M
И не спорь даже
G
так как доказать что типы все покрыли то? это надо делить область определения функции на возможные куски, проверять что тип твой каждый учитывает, то же самое я могу просто на каждый кусок написать тест
да, это proof by exhaustiveness
G
тесты ты не можешь так сделать, давай напишешь тест что a + b складывает
G
и все
G
уже все случаи нельзя покрыть
M
Пздц вы блятт ебанулись
VG
property based test?
M
Нахуя тебе тратить предположим день на код если можно потратить час
M
И обложить тестами и ты получишь ошибку на косарь
M
Что удовлетворяет
G
property based test?
у тебя полюбому чтобы выразить формальную спецификацию должен быть механизм для доказательств
VG
ага, перебор
VG
рандомный
G
ну перебором не все сделаешь
M
Типикал код не ракетами рулит ты Овер инжир предлагаешь со своим пруф ба дезинг
G
перебери например инволюцию переворота списка
G
не переберешь