AS
Исходить из аксиом, конечно же
но из аксиомы теории типов можно или как проведено доказательство что типизация работает? я тут скидывал исследование что строгая типизация не сниает число багов
Size: a a a
2021 February 09
p
Ты не поверишь, но это уже было. 🙂
Угу. Но люди упорно пытаются цитировать заученные определения :(
➔m
В смысле проверки корректности и однозначности. Она основана на теории множеств и (в последнее время) на теории категорий, то есть действует в тех же аксиоматиках
Да, и теоркат и теория множеств не имеют прямого отношения к качеству разработки как модели :/
N
Ну как-то мир с тобой не очень согласен. Есть какой-то незначительный процент упоротых, но большая часть проектов, приносящих овердохуя денег, про это ничего не знают. И у них всё работает.
Меня мало волнует, с чем согласен мир. Есть реальные факты, и есть кучка неучей, которые с ними спорят
AS
У Лобачевского они тоже не пересекаются, достали
ну вот пришли математики, сейчас всех разгонять будут, дайте формошлепам поругаться от души :)
AZ
Меня мало волнует, с чем согласен мир. Есть реальные факты, и есть кучка неучей, которые с ними спорят
Да да, "лучше" и "хуже" это уже "реальные факты"? 🙂
p
В реальной жизни, как мы видим на практике, всем похуй и всё работает без математики.
Вот да. И реальная жизнь отличается от вот этих абстракций из учебника :)
➔m
Меня мало волнует, с чем согласен мир. Есть реальные факты, и есть кучка неучей, которые с ними спорят
Ты тоже специально разжигаешь, да? 😅
N
Да да, "лучше" и "хуже" это уже "реальные факты"? 🙂
А я где-то использовал качественные оценки?
AZ
Коль, ещё раз, есть реальная жизнь. Она отличается от всего этого возвышенного говна из учебников математики.
SZ
Блин, вот с Яндексоидами прямо пример из реальной жизни! Мы вводили в протокол считай что "any". Потому что надо было. Прямо в grpc2, да.
"Типобезопастность"? "Некорректно"? Надо решить задачу и мы её решали. Всё. Точка. Надо, значит надо. И похуй на типы.
"Типобезопастность"? "Некорректно"? Надо решить задачу и мы её решали. Всё. Точка. Надо, значит надо. И похуй на типы.
Яндекс плохой пример
AS
Ты тоже специально разжигаешь, да? 😅
хуже, Николай реально во все это верит
AZ
А я где-то использовал качественные оценки?
Да. Тебе показать, или сам найдёшь?
N
Ты тоже специально разжигаешь, да? 😅
Ну просто когда в ход уже идут фразы типа "в реальном мире математика не работает" - приходится так
N
Коль, ещё раз, есть реальная жизнь. Она отличается от всего этого возвышенного говна из учебников математики.
Окей. На этом и закончим. Я не могу на этом уровне спорить, это бесполезно
p
но из аксиомы теории типов можно или как проведено доказательство что типизация работает? я тут скидывал исследование что строгая типизация не сниает число багов
А почему, кстати?
AZ
Яндекс плохой пример
Очень хороший. Надо было — сделали. И математика пошла на хуй, ибо бизнесу надо не математику, а что б работало и прямо сейчас.
➔m
Ну просто когда в ход уже идут фразы типа "в реальном мире математика не работает" - приходится так
А в реальном мире математика и не работает — она же чисто описательная конструкция для удобства. Теорема Геделя о неполноте и тп
N
хуже, Николай реально во все это верит
Ещё один человек, который не понимает, как работает математика и что там нет места вере
SZ
Очень хороший. Надо было — сделали. И математика пошла на хуй, ибо бизнесу надо не математику, а что б работало и прямо сейчас.
Сделали все равно по своему