AK
нет
это бага текущих тайпчекеров, что они не умеют читать английский
это бага текущих тайпчекеров, что они не умеют читать английский
Size: a a a
2018 February 26
λO
Тогда и программисты будут не нужны. Описал бизнесс процесс, и херак!
λO
А проблема ТЗ еще и в том что писатели не умеют писать по английски (или других языках)
АГ
объясняю
идеальный тайпчекер читает техзадание и проверяет, что программа ему соответствует
всё, все ошибки стали ошибками типов
(да, такой тайпчекер реализовать невозможно, пофиг)
идеальный тайпчекер читает техзадание и проверяет, что программа ему соответствует
всё, все ошибки стали ошибками типов
(да, такой тайпчекер реализовать невозможно, пофиг)
Погодите, я правильно понимаю, что нечто невозможное приводится как валидный аргумент?
AK
Погодите, я правильно понимаю, что нечто невозможное приводится как валидный аргумент?
да
АГ
Но это же нонсенс
λO
А кто будет переводить процесс с английского на формальный?)
Программист тайпчекера. Новая специальность.
АГ
Я бы мог тогда сказать - вот будет бесконечно продвинутый ИИ, и он докажет, что гипотеза Римана верна. Значит, она верна
λO
Но это же нонсенс
Вы истину выясняете в споре, или тупо посраться пришли?
AK
нет, мой аргумент не такой
λO
За истиной сюда не занимайте
AK
ок, пусть дана спека на формальном языке
какие ошибки считаются тогда логическими?
какие ошибки считаются тогда логическими?
λO
ок, пусть дана спека на формальном языке
какие ошибки считаются тогда логическими?
какие ошибки считаются тогда логическими?
ошибки в спеке, чо
АГ
Если вы упираете на то, что иногда сложно разделить логические ошибки и ошибки типизации, то да, грань размыта.
АГ
Но не на столько, чтобы это было проблемой в определении.
λO
http://web.cs.unlv.edu/stefika/research.html вот тут 17 - 21 ссылка. Без реферала с этого сайта ACM не даёт скачать pdf.
тут можно послушать беседу с автором https://www.functionalgeekery.com/episode-55-andreas-stefik/
тут можно послушать беседу с автором https://www.functionalgeekery.com/episode-55-andreas-stefik/
спорим что опять никто не прочитает
АГ
Для начала можно считать, что там, где при замене динамических базовых типов на базовые статические возникает ошибка компиляции, - это не логические ошибки.
Y
Тут можно так переформулировать: "для любого сколь угодно малого е существует такая система типов, что доля ошибок логики, не покрывается типами, меньше е". В пределе с идеальным тайпчекером получаем отсутствие логических ошибок как класса, но даже и в неидеальном - произвольность выделения такого класса.
АГ
спорим что опять никто не прочитает
В списке пейперов 40 позиций!