утверждения не могущие быть выражены через функцию не могут быть и скомпилированы
Этот аргумент не в ту сторону, в которую вы думаете и в которую вам бы хотелось.
я приводил: наличие интегралов, производных, рядов и так далее — вещей, не могущих быть сведенными к констрейнтам
Как всегда, конкретики от вас не добьёшься, ну да ладно.
Почему они не могут быть сведены к констрейнтам-то? Чем они хуже Ферма?
покупатель не согласен платить за впариваемую ему хтонь
Из всех аналогий вы куда ближе к плоскоземельщику, чем к покупателю, которому что-то продают.
да и необходимость что-то вычислять на стадии компиляции явно преувеличена: ведь вычисления возможны исключительно около констант
Я в своё время получал хорошие деньги именно за то, что вычислял на этапе компиляции на эзотерическом языке (темплейты C++). Готовность платить большие деньги за это в куче разных мест подразумевает, что это таки востребовано.
Ну автор правильно пишет, не иметь библиотеки для стека TCP/IP в 21 веке – это за гранью добра и зла.
А смысл?
Библиотека в стандарте заведомо не может охватить все юзкейсы, потому что у автора опердня, у hft-трейдера и у разработчика браузера сильно разные задачи и сильно разные требования, которые все сразу учесть не получится. Соответственно, сеть в стандарте — это как libm, совершенно базовые функции, чтобы по-быстрому, одной строкой скачать что-нибудь откуда-нибудь, когда тебе неважны детали.
Но Комитет патологически не может выдавать простые решения, чтобы по-быстрому и одной строкой. Там наверняка будут экзекуторы какие-нибудь или вообще senders/receivers, попытка охватить все возможные протоколы, все возможные юкзейсы, и так далее, но при этом это не будет юзабельно для большинства из этих юзкейсов, а для тех, где будет, нужно будет написать грёбаную кучу неочевидного кода, который все будут копипастить из cppreference или stackoverflow (или chatgpt).
ИМХО единственное, что должно быть в стандартной библиотеке — словарные типы. variant. optional. string. unordered_map(правда, в плюсах она уродливо тормознутая по стандарту). Нужны данные. Фич не нужно. Вместо фич нужен адекватный и де-факто стандартный в коммьюнити пакетный менеджер. В хаскеле в стандартной либе нет сети, но я просто добавляю в package.yaml строчку с одной удобной мне в данный момент либой, и у меня есть сеть. Отсутствие сети в стандартной либе меня никак не напрягает.
Кто из практических программистов пользуется чем-то выходящим за рамки 11-го ну в крайнем случае 14-го стандартов ??? Может таковые и есть, но вряд ли их много.
На каждом интервью на высокоскоростного байтолюба спрашивают по текущему и иногда следующему стандарту. В 2016-м спрашивали по C++17-фичам, в 2019-м спрашивали по C++20, в 2023-м году спрашивали по C++23. Сейчас не удивлюсь, если по C++26 что-нибудь спросят.
это функция, отвечающая "да" или "нет" на вопрос "входящее значение корректно?".
Только это не функция, это утверждение. И у меня там не только проверка 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 = ??? -- не получится реализовать
Ну тут товарищ вечно молодой, вечно пьяный.
Этот аргумент не в ту сторону, в которую вы думаете и в которую вам бы хотелось.
Как всегда, конкретики от вас не добьёшься, ну да ладно.
Почему они не могут быть сведены к констрейнтам-то? Чем они хуже Ферма?
Из всех аналогий вы куда ближе к плоскоземельщику, чем к покупателю, которому что-то продают.
Я в своё время получал хорошие деньги именно за то, что вычислял на этапе компиляции на эзотерическом языке (темплейты C++). Готовность платить большие деньги за это в куче разных мест подразумевает, что это таки востребовано.
А смысл?
Библиотека в стандарте заведомо не может охватить все юзкейсы, потому что у автора опердня, у hft-трейдера и у разработчика браузера сильно разные задачи и сильно разные требования, которые все сразу учесть не получится. Соответственно, сеть в стандарте — это как
libm, совершенно базовые функции, чтобы по-быстрому, одной строкой скачать что-нибудь откуда-нибудь, когда тебе неважны детали.Но Комитет патологически не может выдавать простые решения, чтобы по-быстрому и одной строкой. Там наверняка будут экзекуторы какие-нибудь или вообще senders/receivers, попытка охватить все возможные протоколы, все возможные юкзейсы, и так далее, но при этом это не будет юзабельно для большинства из этих юзкейсов, а для тех, где будет, нужно будет написать грёбаную кучу неочевидного кода, который все будут копипастить из cppreference или stackoverflow (или chatgpt).
ИМХО единственное, что должно быть в стандартной библиотеке — словарные типы.
variant.optional.string.unordered_map(правда, в плюсах она уродливо тормознутая по стандарту). Нужны данные. Фич не нужно. Вместо фич нужен адекватный и де-факто стандартный в коммьюнити пакетный менеджер. В хаскеле в стандартной либе нет сети, но я просто добавляю вpackage.yamlстрочку с одной удобной мне в данный момент либой, и у меня есть сеть. Отсутствие сети в стандартной либе меня никак не напрягает.На каждом интервью на высокоскоростного байтолюба спрашивают по текущему и иногда следующему стандарту. В 2016-м спрашивали по C++17-фичам, в 2019-м спрашивали по C++20, в 2023-м году спрашивали по C++23. Сейчас не удивлюсь, если по C++26 что-нибудь спросят.
Как в андроиде с растом. Оставить C++ для уже написанного легаси и всё остальное делать на более других языках.
Не всё то, что вам неизвестно, отсутствует. Я уже давал рядом отсылку к вводному тексту на тему, например.
Только это не функция, это утверждение. И у меня там не только проверка 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. Там и перепутанные операторы отлавливались, и некорректные формулы расчёта стоимости коинов (скажем, они должны быть монотонными по какому-нибудь параметру — успехов поймать это тестами), и так далее. И всё это — типами.
Да не, почему? Это важная часть общения и самоактуализации, так что я не против, конечно! Просто, как говорится, употребляйте ответственно.
Ну а ваш алгоритм этого не делает, независимо от программ. Вы опять сами себя переспорили.
Правда, ваша ошибка здесь в том, что вы считаете, что и программы, и алгоритмы должны всегда завершаться, но внутренняя неконсистентность вашей же логики с вашими же определениями даже смешнее.
Окей, если все теоремы — тоже констрейнты, то какой смысл в высказывании «это просто констрейнт»? Что бывает кроме констрейнтов?
Лол.
Какое тут преобразование типа? Какой код выполняется? Можете ткнуть в это всё пальцем?
Дабл лол.
Раньше вы путали знаки сравнения в любом месте, теперь только в декларации типа. Ну ладно, давайте с декларацией.
Типы снова помогли отловить ошибку!