это функция, отвечающая "да" или "нет" на вопрос "входящее значение корректно?".
Только это не функция, это утверждение. И у меня там не только проверка x^a + y^a = z^a, а ещё и указание, что это (не) выполняется для любых a ≥ 3.
«Все крокодилы зелёные» — это функция? Что она принимает на вход?
2x = y или даже Фермовый x^a + y^a = z^a теоретически можно записать в констрейнтах.
А можно таки конкретный пример теоремы, которая по-вашему так не записывается?
Но в тот момент, когда внутри констрейнта требуется, например, интегрировать, дифференцировать, вычислять минимумы/максимумы и так далее, в этот момент компилятор поднимет лапки и скажет "автоматически такое делать я не умею".
Про автоматику тут вообще никто не говорит. Утверждение выше точно так же надо доказывать руками — компиляторы его доказывать не умеют, к сожалению.
Вывод
Вывод неверный, потому что вы то ли не понимаете, что такое теоремы, то ли сейчас начнёте подгонять понятие констрейнта под ответ.
символы Unicode (кстати, что это за фетиш? Для чего он?)
Чтобы читать легче было.
это не теоремы, а нечто, могущее иметь с ними дальнее сходство.
Только вот, опять же, любую теорему можно там выразить.
Смотрим в языки программирования с динамической типизацией. Видим констрейнты и без типов. Мало того, можем запрограммировать констрейнт даже там, где они не предусмотрены синтаксисом
И где здесь проверки на этапе компиляции?
Как будет выглядеть утверждение теоремы Ферма? Только чтобы у вас не получилось реализовать неправильные утверждения.
Всё это разные технологии и продать их мне пакетом под видом "типы" не выйдет.
Потому что у вас нулевые способности к восприятию информации, безусловно.
Почему они перестали пользоваться формальными методами? Как их пустили в столь респектабельный журнал?
Они и не начинали, увы. Потому что ещё, к сожалению, значимая часть математиков не считает наличие возможных ошибок достаточной проблемой, но обсуждение этого вопроса уведёт нас сильно в сторону социологии науки.
В программировании тоже вон науки до фига - ИИ тот же.
А где в ИИ наука?
Если проход через турникет метро будет требовать счётчика Гейгера, то это создаст неудобства.
Это скорее ситуация с тестами и повальным юнит-тестированием всего и вся, за которую вы топите.
Написав import module, Вы выполняете код, который реализует присвоение значения переменной foo. И этот код будет исполняться пока идёт import. Полный аналог кода, исполняемого в момент компиляции.
А можно так же, но с языками, где есть полноценный шаг компиляции, вроде C? И чтобы произвольная bar могла выполняться.
Впрочем, это всё на самом деле неважно, потому что в случае типов выполнение кода при тайпчекинге — это, опять же, сугубо техническая и неинтересная для пользователя языка деталь.
Что значит «понимание»? Интуитивное понимание операции объединения или пересечения двух множеств, как с кружочками на диаграммах? Интуитивное понимание инъективной функции? Умение построить ультрафильтр на булевых решётках?
Я код начал писать где-то в 10-11 лет, и лет в 13 уже писал даже что-то осмысленное и полезное не только мне. Понимание теории множеств у меня было не более чем интуитивное. Что я потерял?
Что, кстати, подтверждает самое начало дискуссии - термин в логику пришёл из религии. :)
От сторонника ООП это слышать очень странно, смотрите: преобразования типов, так часто используемые в ООП, называются type conversion. Так и в религии conversion подразумевается как обращение в свою религию. То есть, ООП — это такая религиозная секта, которая стремится преобразовать всех прочих типов (уничижительное название для людей, не практикующих ООП, вроде «идёт какой-то хмурый тип») в свою веру.
Я помню, что вам лень отвечать, но «мне лень отвечать, почему вы не показали, но не показали, пнятненько?» — это очередное пробитое дно уровня ведения дискуссии с вашей стороны.
Вы математик или где?
Нет, конечно. Какой из меня математик?
Но в то же время "теорема всегда сводится к констрейнту" - нет.
Я у вас выше прямо спросил, является ли теорема Ферма констрейнтом, и вы сказали да. На неявный вопрос о том, есть ли теоремы-не-констрейнты, вы там не ответили положительно, поэтому я спрошу здесь: приведите, пожалуйста, пример теоремы, которая не является констрейнтом в вашей терминологии.
когда оппонент говорит "только" достаточно привести ему один контрпример.
А когда оппонент говорит «не только» (как это сделал я), то что надо привести?
А во-вторых, констрейнт - это уже не про типы, а про самостоятельную сущность.
Кто сказал? Есть вообще целые системы типов вроде всяких refinement types, чей смысл существования — именно что навешивать констрейнты и оперировать с ними удобно для программиста (сиречь иметь разрешимую автоматизацию).
Или, на более привычном вам языке, вы говорите «Int — это не тип, а самостоятельная сущность».
но весь этот пакет относится не к типам и я предлагаю таки спорить по каждому пункту отдельно.
Вы написали очень много слов, но ни одно из них не связано с тем, что вы процитировали из моего комментария перед этим.
при языках, примеры которых Вы приводите
Линейные типы дают мутабельность и в тех языках, примеры которых я пишу. Монада ST даёт мутабельность.
Ага, но вы этого не сделали.
Если бы я не сделал, то оно бы не скомпилировалось.
тип у вас внутри всего один и он ничего не подсказал
Не понял, что это вообще значит? Мне компилятор говорит что-то в духе «cannot match i of type Fin n with argument of type Fin (n + 1)». Вот прям подсказка: скоуп индекса другой, увеличился на единицу, и надо это как-то обработать теперь.
большинство кода, что пишется в современное время в теоремах не выразить. ибо снова мутабельность впереди всего.
Вы, главное, про это не рассказывайте тем, кто придумывает алгоритмы за этим кодом, а то они рискуют умереть со смеху, и больше не будет никаких алгоритмов.
Видите? Вы во-первых, сами нашли пример, опровергающий Ваш тезис.
И пример, якобы опровергающий то, что типы ловят ошибки, состоит в том, что люди, не пользующиеся формальными методами и системами типов, допустили ошибку, которую я поймал благодаря использованию типов?
Это у вас очень серьёзная заявка на первое место на чемпионате среди ретардов хабра.
А во-вторых, у Вас всё настолько сложно, что приходится писать и читать научные статьи с авторством больше одного человека. И при этом всё равно ошибки.
Ну не всем же микросервисы по кэшированию жсонов разрабатывать, кому-то приходится и что-то более сложное делать, сорян.
Но вообще да, согласен, бесовское всё это. Науку отменить, журналы закрыть, грабли в руки — и пахать. Пол Пот грит малаца.
Чтобы было максимально просто, то когда Вы пишете import foo, то в этот момент производится загрузка файла в память, его парсинг, разбор всяких AST-деревьев и проч. В этот момент выполняется код внутри foo.py.
Не понял. Загрузка, парсинг и разбор AST-деревьев — это выполнение кода внутри анализируемого исходника? Лол.
Вы результатами моего труда скорее всего пользовались.
Последний раз я пользовался, наверное, яндекс.маркетом лет 20 назад, потом им стало пользоваться невозможно. Остальными результатами яндекса я не пользовался, и не пользовался бы даже если бы жил в России (просто потому, что они мне не нужны).
Но, впрочем, куда чаще я пользуюсь результатами труда местных фермеров и скотоводов, но это не делает их авторитетами в области программирования.
Вы мыслите только математически выразимыми категориями, а потому не видите картины в целом.
Почему же? Цельная картина в том, что вы не понимаете, когда сужение требований помогает, а когда — мешает.
я много раз говорил: типы помогают.
Вы только что говорили, что типы не помогают отличить > от ≥. Я показал, как они помогают [это сделать]. Вы теперь говорите, что много раз говорили, что типы помогают [это сделать]. Или вы уже потеряли контекст?
И констрейнты в типах, которые Вы по недоразумению зовёте "теоремами" тоже.
Почему по недоразумению? Вы же сами сказали, что утверждения теорем — это тоже констрейнты. Что не так?
типизацию: решает проблемы перепутывания арбузов с автомашинами
Далеко не только, и ваше игнорирование любых ответов на этот неверный тезис начинает надоедать.
Радикально упрощает написание компилятора.
Ну вообще нет. Писать компилятор с тайпчекером куда сложнее (и тем сложнее, чем сложнее система типов).
Радикально усложняет жизнь программисту.
Херак-херак-в-продакшен-программисту — да. Но ему много что жизнь усложняет, от типов до линтера, процесса код-ревью и гита.
иммутабельность
Вообще ни при чём тут.
Радикально усложняет жизнь программисту, поскольку ему (программисту) требуется моделировать реальный мир, а он (реальный мир) мутабелен в своей основе
Реальный мир в своей основе — это иммутабельная комплекснозначная функция на вещественном пространстве-времени, причём строго детерминированная (потому что эволюция квантовых систем описывается унитарными операторами).
Так что кто тут ещё упрощает или усложняет.
упрощённый синтаксис записи констрейнтов
Вы так и не смогли определить, что такое констрейнты и чем они отличаются от теорем. И какой синтаксис был бы не упрощённым, да.
Кстати, многие языки давно умеют запускать код на стадии компиляции: вот Python
Что за стадия компиляции у Python?
Такой запуск кода не имеет вообще никакого отношения к типам.
и как же типы тут помогали?
Ну как, индекс должен иметь тип Fin (n + 1), а имел тип Fin n. Соответственно, надо либо weaken делать, либо прибавлять единичку: система типов на этапе написания этого кода сказала, что я что-то из этого забыл, и, значит, надо прям вот здесь сесть и подумать, что я хочу. Потом, когда я про этот код сел доказывать теоремы, то, если бы я (неверно) выбрал weaken вместо прибавления единички, то теоремы бы не доказались, а так они доказались.
При этом похожая ошибка (там не добавили единичку, что сломало свойства описываемой системы) была в отрецензированной и опубликованной научной статье за авторством этак трёх человек, на которой я основывал свою работу.
злоумышленники использовали сложный метод подмены транзакции, который позволил им получить полный контроль над активами.
Ровно то, что мы искали в аудитах и обмазывали типами, лол. Им просто надо было к нам обратиться (только жаль, что у эфира не та же модель, что у кардано).
Речь о том, что требования могут быть любыми: не нравятся требования — не ходи в наш садик, противный покупаешь там дом, и всего делов.
Всё так. Прелести свободного рыночка!
Во-первых, ассоциация должна быть в курсе, что правила нарушаются. Вы в менеджмент писали/звонили (с приложением аудио/видеодоказательств)?
Там собачники, и они игнорируют претензии к собакам.
Ну и там реально ленивые раздолбы, потому что на моё уведомление о соларах, на которое они по закону обязаны ответить утвердительно за типа 30 дней, они отвечали месяца четыре.
Закон шизоидный, кстати: HOA обязана аппрувнуть установку соларов, но единственный повод им этого не делать по закону — если я их не уведомил. Почти как arrested for resisting arrest.
А во-вторых, если менеджмент совсем мышей не ловит — изберитесь в правление своей ассоциации и начните вставлять пистоны.
Ща, комментарий допишу и пойду изберусь, ведь это так просто!
да в любом месте, почему бы не в декларации типа их перепутать?
Тут бы вам помогло, кстати, понимание разницы между ковариантностью и контравариантностью, но ирония этого замечания от вас ускользнёт, боюсь.
а ваш синтетический пример и лень комментировать.
Конечно, потому что сказать-то нечего, а признать, что типы помогают, никак нельзя.
Ну и да, даёшь короткий пример — «синтетика! нинужно!», даёшь длинный пример — «не совпадает с моей областью деятельности! нинужно! я командую парадом микросервисами!»
попробуйте воспроизвести перепут < и <= на вашем любимом факториале, или Фибоначчи
Ну это, конечно, не синтетика.
Путал на практике, упрощая, добавление единицы к индексу и его отсутствие. Типы помогали это ловить, код тупо не тайпчекался.
Или, опять же, на практике занимался аудитом формального доказательства смарт-контракта на isabelle/hol. Там и перепутанные операторы отлавливались, и некорректные формулы расчёта стоимости коинов (скажем, они должны быть монотонными по какому-нибудь параметру — успехов поймать это тестами), и так далее. И всё это — типами.
Ну а ваш алгоритм этого не делает, независимо от программ. Вы опять сами себя переспорили.
Правда, ваша ошибка здесь в том, что вы считаете, что и программы, и алгоритмы должны всегда завершаться, но внутренняя неконсистентность вашей же логики с вашими же определениями даже смешнее.
Раньше вы путали знаки сравнения в любом месте, теперь только в декларации типа. Ну ладно, давайте с декларацией.
-- декларирую тип с ошибкой `<` вместо `≤`:
data PersonOrder (p1, p2 : Person) : Type where
MkPO : p1.name < p2.name → PersonOrder p1 p2
poReflexive : (p : Person) → PersonOrder p p
poReflexive = ??? -- не получится реализовать
там, где имеет место HOA (HomeOwner Assocation) — сообщество домовладельцев — и там в правилах сообщества прописаны требования к участникам (типа «крыша только красная, трава не длиннее 2 дюймов, собак кормить только мраморным стейком и т. п.»)
У далеко не всех HOA такие требования. Трава должна быть просто опрятной, крышу я спокойно поменял на слегка другого цвета вообще без согласования с HOA, окна — тоже, солары поставил в уведомительном порядке (лан, тут законы Техаса обязывают их разрешить, если уведомление направлено, так что я даже не ждал ответа).
А даже те правила, что есть, энфорсятся не всегда. Например, собакам запрещено «excessive barking», но это не мешает одному товарищу четыре раза в день по 15 минут выгуливать свою незатыкающуюся и триггерящуюся на любое движение псину, что несколько мешает держать окна открытыми и при этом заниматься требующими концентрации делами. Это практически невозможно починить в данной полураздолбайской HOA, и я был бы рад жить там, где это энфорсится куда строже.
Ну то есть всё это социальные конструкты, только одни получше, а другие похуже.
Да, и?
Я говорю не о том, какие это конструкты, а о том, откуда идёт инициатива по их насаждению. Снизу вверх — может, норм, может, плохо. Сверху вниз — практически всегда плохо.
А теперь возьмем ситуацию, когда команда разработчиков не может договориться про выбор методики работы. Что тогда делать бизнесу, садиться и плакать? Нет же, top-down-процесс спешит на помощь!
Во-первых, бизнес ничего не делает. В нормальной группе что-то решает в данном случае тимлид, а не весь бизнес целиком. Это совсем не тот же top-down-процесс, как если бы CEO посмотрел буллшит-доклад какого-нибудь Мартина на какой-нибудь конферфенции с задорно выглядящими графиками и решил «мы теперь все работает по аджайлу».
Во-вторых, устраиваясь на работу в данную группу к данному тимлиду, я в том числе осознанно и открыто делегировал ему часть ответственности и больший вес по принятию решений (по крайней мере, выяснить, хочу ли я ему это делегировать — моя цель на интервью как нанимающегося). Рождение в данном государстве с данной политической системе (или пересечение отрезка жизни с революцией) не является настолько же осознанным и добровольным.
В-третьих, поменять группу (или работу) куда проще, чем государство. Настолько проще, что по факту дисбалансом власти между тимлидом и линейным программистом можно пренебречь.
С учётом всего этого говорить, что там характеристики top-down-процессов одинаковые, и
не только государства воплощают этот принцип, а и любая (почти, так как bottom-up бизнесов крайне мало) другая организация
а вы попробуйте выразить Ферма на ваших типах и убедитесь, что это именно констрейнты
Как раз выразил выше (опустив не сильно важную для дискуссии деталь).
Так всё же, слова «уравнение a^n + b^n = c^n не имеет решения в целых ненулевых числах для n ≥ 3» являются просто констрейнтом на подмножество (и чего), или нет?
Я понимаю, что очень хочется уязвить собеседника, но в следующий раз попробуйте привязываться к контексту его комментария целиком, а не к одному ключевому слову.
Только это не функция, это утверждение. И у меня там не только проверка x^a + y^a = z^a, а ещё и указание, что это (не) выполняется для любых a ≥ 3.
«Все крокодилы зелёные» — это функция? Что она принимает на вход?
А можно таки конкретный пример теоремы, которая по-вашему так не записывается?
Про автоматику тут вообще никто не говорит. Утверждение выше точно так же надо доказывать руками — компиляторы его доказывать не умеют, к сожалению.
Вывод неверный, потому что вы то ли не понимаете, что такое теоремы, то ли сейчас начнёте подгонять понятие констрейнта под ответ.
Чтобы читать легче было.
Только вот, опять же, любую теорему можно там выразить.
И где здесь проверки на этапе компиляции?
Как будет выглядеть утверждение теоремы Ферма? Только чтобы у вас не получилось реализовать неправильные утверждения.
Потому что у вас нулевые способности к восприятию информации, безусловно.
Они и не начинали, увы. Потому что ещё, к сожалению, значимая часть математиков не считает наличие возможных ошибок достаточной проблемой, но обсуждение этого вопроса уведёт нас сильно в сторону социологии науки.
А где в ИИ наука?
Это скорее ситуация с тестами и повальным юнит-тестированием всего и вся, за которую вы топите.
А можно так же, но с языками, где есть полноценный шаг компиляции, вроде C? И чтобы произвольная bar могла выполняться.
Впрочем, это всё на самом деле неважно, потому что в случае типов выполнение кода при тайпчекинге — это, опять же, сугубо техническая и неинтересная для пользователя языка деталь.
Ровно в это и превратится. Посмотрите любой промышленный компилятор вроде llvm или gcc.
Что значит «понимание»? Интуитивное понимание операции объединения или пересечения двух множеств, как с кружочками на диаграммах? Интуитивное понимание инъективной функции? Умение построить ультрафильтр на булевых решётках?
Я код начал писать где-то в 10-11 лет, и лет в 13 уже писал даже что-то осмысленное и полезное не только мне. Понимание теории множеств у меня было не более чем интуитивное. Что я потерял?
От сторонника ООП это слышать очень странно, смотрите: преобразования типов, так часто используемые в ООП, называются type conversion. Так и в религии conversion подразумевается как обращение в свою религию. То есть, ООП — это такая религиозная секта, которая стремится преобразовать всех прочих типов (уничижительное название для людей, не практикующих ООП, вроде «идёт какой-то хмурый тип») в свою веру.
В чём недоступность мутабельности для математики?
Пример выше. Показал.
Я помню, что вам лень отвечать, но «мне лень отвечать, почему вы не показали, но не показали, пнятненько?» — это очередное пробитое дно уровня ведения дискуссии с вашей стороны.
Нет, конечно. Какой из меня математик?
Я у вас выше прямо спросил, является ли теорема Ферма констрейнтом, и вы сказали да. На неявный вопрос о том, есть ли теоремы-не-констрейнты, вы там не ответили положительно, поэтому я спрошу здесь: приведите, пожалуйста, пример теоремы, которая не является констрейнтом в вашей терминологии.
А когда оппонент говорит «не только» (как это сделал я), то что надо привести?
Кто сказал? Есть вообще целые системы типов вроде всяких refinement types, чей смысл существования — именно что навешивать констрейнты и оперировать с ними удобно для программиста (сиречь иметь разрешимую автоматизацию).
Или, на более привычном вам языке, вы говорите «Int — это не тип, а самостоятельная сущность».
Вы написали очень много слов, но ни одно из них не связано с тем, что вы процитировали из моего комментария перед этим.
Линейные типы дают мутабельность и в тех языках, примеры которых я пишу. Монада ST даёт мутабельность.
Если бы я не сделал, то оно бы не скомпилировалось.
Не понял, что это вообще значит? Мне компилятор говорит что-то в духе «cannot match i of type Fin n with argument of type Fin (n + 1)». Вот прям подсказка: скоуп индекса другой, увеличился на единицу, и надо это как-то обработать теперь.
Вы, главное, про это не рассказывайте тем, кто придумывает алгоритмы за этим кодом, а то они рискуют умереть со смеху, и больше не будет никаких алгоритмов.
И пример, якобы опровергающий то, что типы ловят ошибки, состоит в том, что люди, не пользующиеся формальными методами и системами типов, допустили ошибку, которую я поймал благодаря использованию типов?
Это у вас очень серьёзная заявка на первое место на чемпионате среди ретардов хабра.
Ну не всем же микросервисы по кэшированию жсонов разрабатывать, кому-то приходится и что-то более сложное делать, сорян.
Но вообще да, согласен, бесовское всё это. Науку отменить, журналы закрыть, грабли в руки — и пахать. Пол Пот грит малаца.
Не понял. Загрузка, парсинг и разбор AST-деревьев — это выполнение кода внутри анализируемого исходника? Лол.
Последний раз я пользовался, наверное, яндекс.маркетом лет 20 назад, потом им стало пользоваться невозможно. Остальными результатами яндекса я не пользовался, и не пользовался бы даже если бы жил в России (просто потому, что они мне не нужны).
Но, впрочем, куда чаще я пользуюсь результатами труда местных фермеров и скотоводов, но это не делает их авторитетами в области программирования.
Почему же? Цельная картина в том, что вы не понимаете, когда сужение требований помогает, а когда — мешает.
Вы только что говорили, что типы не помогают отличить
>от≥. Я показал, как они помогают [это сделать]. Вы теперь говорите, что много раз говорили, что типы помогают [это сделать]. Или вы уже потеряли контекст?Почему по недоразумению? Вы же сами сказали, что утверждения теорем — это тоже констрейнты. Что не так?
Далеко не только, и ваше игнорирование любых ответов на этот неверный тезис начинает надоедать.
Ну вообще нет. Писать компилятор с тайпчекером куда сложнее (и тем сложнее, чем сложнее система типов).
Херак-херак-в-продакшен-программисту — да. Но ему много что жизнь усложняет, от типов до линтера, процесса код-ревью и гита.
Вообще ни при чём тут.
Реальный мир в своей основе — это иммутабельная комплекснозначная функция на вещественном пространстве-времени, причём строго детерминированная (потому что эволюция квантовых систем описывается унитарными операторами).
Так что кто тут ещё упрощает или усложняет.
Вы так и не смогли определить, что такое констрейнты и чем они отличаются от теорем. И какой синтаксис был бы не упрощённым, да.
Что за стадия компиляции у Python?
Такой запуск кода не имеет вообще никакого отношения к типам.
Ну как, индекс должен иметь тип
Fin (n + 1), а имел типFin n.Соответственно, надо либо weaken делать, либо прибавлять единичку: система типов на этапе написания этого кода сказала, что я что-то из этого забыл, и, значит, надо прям вот здесь сесть и подумать, что я хочу. Потом, когда я про этот код сел доказывать теоремы, то, если бы я (неверно) выбрал weaken вместо прибавления единички, то теоремы бы не доказались, а так они доказались.При этом похожая ошибка (там не добавили единичку, что сломало свойства описываемой системы) была в отрецензированной и опубликованной научной статье за авторством этак трёх человек, на которой я основывал свою работу.
А-а-а! Яндекс! Политики, пропагандисты и неумехи!
Нет, и я вообще не занимался эфиром.
Ровно то, что мы искали в аудитах и обмазывали типами, лол. Им просто надо было к нам обратиться (только жаль, что у эфира не та же модель, что у кардано).
Всё так. Прелести свободного рыночка!
Там собачники, и они игнорируют претензии к собакам.
Ну и там реально ленивые раздолбы, потому что на моё уведомление о соларах, на которое они по закону обязаны ответить утвердительно за типа 30 дней, они отвечали месяца четыре.
Закон шизоидный, кстати: HOA обязана аппрувнуть установку соларов, но единственный повод им этого не делать по закону — если я их не уведомил. Почти как arrested for resisting arrest.
Ща, комментарий допишу и пойду изберусь, ведь это так просто!
Почему это? Вам просто нужны зависимые типы!
Тут бы вам помогло, кстати, понимание разницы между ковариантностью и контравариантностью, но ирония этого замечания от вас ускользнёт, боюсь.
Конечно, потому что сказать-то нечего, а признать, что типы помогают, никак нельзя.
Ну и да, даёшь короткий пример — «синтетика! нинужно!», даёшь длинный пример — «не совпадает с моей областью деятельности! нинужно! я командую
парадоммикросервисами!»Ну это, конечно, не синтетика.
Путал на практике, упрощая, добавление единицы к индексу и его отсутствие. Типы помогали это ловить, код тупо не тайпчекался.
Или, опять же, на практике занимался аудитом формального доказательства смарт-контракта на isabelle/hol. Там и перепутанные операторы отлавливались, и некорректные формулы расчёта стоимости коинов (скажем, они должны быть монотонными по какому-нибудь параметру — успехов поймать это тестами), и так далее. И всё это — типами.
Да не, почему? Это важная часть общения и самоактуализации, так что я не против, конечно! Просто, как говорится, употребляйте ответственно.
Ну а ваш алгоритм этого не делает, независимо от программ. Вы опять сами себя переспорили.
Правда, ваша ошибка здесь в том, что вы считаете, что и программы, и алгоритмы должны всегда завершаться, но внутренняя неконсистентность вашей же логики с вашими же определениями даже смешнее.
Окей, если все теоремы — тоже констрейнты, то какой смысл в высказывании «это просто констрейнт»? Что бывает кроме констрейнтов?
Лол.
Какое тут преобразование типа? Какой код выполняется? Можете ткнуть в это всё пальцем?
Дабл лол.
Раньше вы путали знаки сравнения в любом месте, теперь только в декларации типа. Ну ладно, давайте с декларацией.
Типы снова помогли отловить ошибку!
Их действительно можно перепутать, но не потому, что вы не знаете, какой значок что означает, а потому, что предметная область сложная.
Да, там ведь используются совершенно одинаковые навыки. Матан — это про зубрёж, как таблица умножения.
Таблицу умножения по какому основанию, кстати? По основанию 30 запомнить и вы вряд ли сможете уже, но что это говорит?
У далеко не всех HOA такие требования. Трава должна быть просто опрятной, крышу я спокойно поменял на слегка другого цвета вообще без согласования с HOA, окна — тоже, солары поставил в уведомительном порядке (лан, тут законы Техаса обязывают их разрешить, если уведомление направлено, так что я даже не ждал ответа).
А даже те правила, что есть, энфорсятся не всегда. Например, собакам запрещено «excessive barking», но это не мешает одному товарищу четыре раза в день по 15 минут выгуливать свою незатыкающуюся и триггерящуюся на любое движение псину, что несколько мешает держать окна открытыми и при этом заниматься требующими концентрации делами. Это практически невозможно починить в данной полураздолбайской HOA, и я был бы рад жить там, где это энфорсится куда строже.
Да, и?
Я говорю не о том, какие это конструкты, а о том, откуда идёт инициатива по их насаждению. Снизу вверх — может, норм, может, плохо. Сверху вниз — практически всегда плохо.
Во-первых, бизнес ничего не делает. В нормальной группе что-то решает в данном случае тимлид, а не весь бизнес целиком. Это совсем не тот же top-down-процесс, как если бы CEO посмотрел буллшит-доклад какого-нибудь Мартина на какой-нибудь конферфенции с задорно выглядящими графиками и решил «мы теперь все работает по аджайлу».
Во-вторых, устраиваясь на работу в данную группу к данному тимлиду, я в том числе осознанно и открыто делегировал ему часть ответственности и больший вес по принятию решений (по крайней мере, выяснить, хочу ли я ему это делегировать — моя цель на интервью как нанимающегося). Рождение в данном государстве с данной политической системе (или пересечение отрезка жизни с революцией) не является настолько же осознанным и добровольным.
В-третьих, поменять группу (или работу) куда проще, чем государство. Настолько проще, что по факту дисбалансом власти между тимлидом и линейным программистом можно пренебречь.
С учётом всего этого говорить, что там характеристики top-down-процессов одинаковые, и
просто неверно и подмена тезиса.
Как раз выразил выше (опустив не сильно важную для дискуссии деталь).
Так всё же, слова «уравнение a^n + b^n = c^n не имеет решения в целых ненулевых числах для n ≥ 3» являются просто констрейнтом на подмножество (и чего), или нет?
Вы:
Я:
Я понимаю, что очень хочется уязвить собеседника, но в следующий раз попробуйте привязываться к контексту его комментария целиком, а не к одному ключевому слову.
Я именно к этому контексту и отсылаю. Или мне нужно все ваши комментарии целиком сюда копировать, а то иначе вы не вспомните, что вы сами писали?
И моя религия выражается в том, что я имею наглость регулярно вам напоминать, что от
>вместо≥типы тоже спасают, и показывать, как?