p
а что уже придумали как?
А что, нет? О.о
Size: a a a
2020 March 25
A
Т-34 85
У тебя в принципе не возникнет высячей ссылки, если по ссылке не передаёшь. Как можно случайно передать по ссылке то, что ты не хочешь передавать по ссылке? Или ты подстраиваешься под то, что в команде есть шизофреники?
Нет. Я не подстраиваюсь. Я допускаю, что все совершают ошибки и чем больше инструментов контроля, тем лучше.
AZ
Т-34 85
У тебя в принципе не возникнет высячей ссылки, если по ссылке не передаёшь. Как можно случайно передать по ссылке то, что ты не хочешь передавать по ссылке? Или ты подстраиваешься под то, что в команде есть шизофреники?
можно передать то что не хчоеш ьпередавать
Т8
Я вот, бывает, такие глупые ошибки совершать могу. Хоть и внимателен. Вот пишешь код по 10 часов и глаза уже не видят банальных вещей.
Это понятно. Но и с логическими ошибками это случается. И теорему в идрисе ты можешь неправильно доказывать
AZ
что непонятно-то?
A
Т-34 85
Это понятно. Но и с логическими ошибками это случается. И теорему в идрисе ты можешь неправильно доказывать
Да. Ошибки будут всегда. Разница только с количеством и вероятностью возникновения.
AZ
Т-34 85
Это понятно. Но и с логическими ошибками это случается. И теорему в идрисе ты можешь неправильно доказывать
"зачем мыться если потом опять испачкаешьс" - логика такая у тебя
G
Т-34 85
Это понятно. Но и с логическими ошибками это случается. И теорему в идрисе ты можешь неправильно доказывать
Не можешь, тогда не тайп-чекнется теорема
A
Не можешь, тогда не тайп-чекнется теорема
Не, он про то, что теорему сформулировал ошибочно.
A
Которая не отражает нужную БЛ
G
Не, он про то, что теорему сформулировал ошибочно.
Может и такое быть. Но в 99% языков теорем на уровне Идриса вообще нет
G
Да что там 99%. Языков много, теоремы на уровне "каждая инволюция есть инъекция" можно только в единицах доказывать
A
В общем, я за уменьшение вероятности возникновения ошибок, путём использования системы типов и других средств. Всё, что пишется на "честном слове и внимательности" разработчика нестабильно и подлежит утилизации.
DS
Т-34 85
Это понятно. Но и с логическими ошибками это случается. И теорему в идрисе ты можешь неправильно доказывать
Вообще - нет, не можешь, иначе какой смысл в теорем прувере-то
G
В общем, я за уменьшение вероятности возникновения ошибок, путём использования системы типов и других средств. Всё, что пишется на "честном слове и внимательности" разработчика нестабильно и подлежит утилизации.
+
AZ
Вообще - нет, не можешь, иначе какой смысл в теорем прувере-то
ты вместо свойства сложения можешь доказать свойство умножения
AZ
или докажешь, что разворот списка это rev (rev list) = list
Т8
или докажешь, что разворот списка это rev (rev list) = list
Да, примерно такое и имел в виду
p
или докажешь, что разворот списка это rev (rev list) = list
А что, не так?
NL
ты вместо свойства сложения можешь доказать свойство умножения
Противники статической типизации часто приводят пример:
и вывод такой: если в таком простом случае компилятор беспомощен и пропускает ошибку, то нет смысла вообще в компиляторах и теорем пруверах. Такая вот логика.
fn add(x: i32, y: i32) -> i32 { x - y }
и вывод такой: если в таком простом случае компилятор беспомощен и пропускает ошибку, то нет смысла вообще в компиляторах и теорем пруверах. Такая вот логика.