а заниматься почти тем же, чем ты и так занимаешься на работе только бесплатно
«почти» здесь под довольно большой нагрузкой.
На работе я решаю рабочие задачи, делая то, что нужно работодателю. Нужно переложить ещё несколько жсонов — перекладываю. Нужно поковыряться в махровом легаси — ковыряюсь. Есть какой-то мерзкий неприятный баг — чиню. Нужно в 2017-м году работать с C++03, потому что махровая легаси-кодовая база не переехала на свежий компилятор, потому что от этого вылезают мерзкие баги — плююсь, но работаю. Сколько при этом я получаю фана — работодателю совершенно неважно (и чем больше платят, тем это менее важно и мне самому).
Дома я делаю то, что весело мне самому, и с нулевой ответственностью (что, пожалуй, самое главное). Баги хочу — чиню, не хочу — нет. Фичреквесты хочу — делаю, не хочу — нет. Прошлую версию компилятора хочу — поддерживаю, не хочу — нет. Не хочу — не поддерживаю даже текущую, извольте собирать clang HEAD, там же новую вкусняшку завезли! Хочу — вообще забиваю на проект. Хочу — делаю однодневку как proof-of-concept. Хочу — выбираю маргинальные инструменты и зарываюсь в yak shaving так глубоко, как хочу (захотелось сделать монте-карло-оценку разных стратегий инвестиций по историческим данным ⇒ взял идрис, а там генератора случайных чисел нормального нет ⇒ взял разобрался в PCG, начал писать реализацию ⇒ а в идрисе верифицированных битовых операций нет ⇒ пошёл делать ⇒ отвлёкся, забыл, забил, ну и пофиг, фана получил достаточно).
Ну, смысл понятен.
Это твой выбор и твоё право, но это не делает тебя лучше других.
С точки зрения работодателя — делает. Как специалиста — делает.
А абстрактного единого «лучше» нет, есть только «лучше для $X». Вот что лучше — велосипед или самолёт?
Дальше расскажи сколько времени в день ты уделяешь семье, детям, хобби, пет-проектам и физической активности.
На всякий случай — работаю удалённо, в средний будний день часов 6 в день работа съедает, физическая активность — три похода в тренажерку в неделю по два часа каждый, в качестве пет-проектов сейчас в основном зашариваю разный матан, по 3-4 часа в будний день уходит (и в пару раз больше в выходные), плюс просто читаю всякую ерунду — от блогов до статей с arxiv и этак сорокета книг в год. Ну и ещё всякая мелочёвка есть на несколько часов.
Детей и семьи нет (этого я никогда не хотел), и не жалею об этом. Жалею, что в вузовские годы «не нагулялся», факт (и мета-жалею о том, что разрешил себе в этом признаться только совсем недавно), но эти годы уже всё равно не вернёшь, а сейчас контекст не тот. Да и в вузе было жёстче, чем на работе, и после пар всё равно приходилось заниматься самообразованием. Стоило не поддаваться на peer pressure и идти в халявный вуз только ради отмазы от армии, где надо появляться дважды в год на сессии — всё равно толку с этих всех урматов, диффуров и функанов на работе нет, а для меня самого мне сильно интереснее немного другие ветви математики, которых в вузе нет.
но я до сих пор не понимаю, зачем оно нужно в реальной жизни.
Один из вариантов — таки типобезопасный printf. Вон, плюсисты нетривиально приседают, чтобы в std::fmt (или как его там, не игрался на практике с этой частью новых плюсов) известные в компилтайме строки позволяли проверять типы аргументов. В шланге и gcc добавили проверки (и аннотации для кастомных строк), чтобы проверять соответствие строки формата аргументам у обычного сишного printf. Наверное, это нужно.
Другой вариант из личной практики, когда я по фану делал на идрисе обёртку вокруг постгреса — можно описать структуру таблицы обычным языком термов, и потом обычными функциями Schema → Type создать что тип, значения которого соответствуют схеме, что все эти обёртки над create table / insert / update / etc.
В мейнстримных языках для этого обмазываются какой-нибудь рефлексией, и всё даёт нечитаемые ошибки и разваливается (в рантайме, если рефлексия — рантайм).
Зачем вы опровергаете то, что я не говорил и даже не подразумевал?
Карантин нужен для остановки болезни в том числе. Если вы посмотрите статистику по гриппу за 2020-й и 2021-й, особенно в странах с сильными карантинными мерами, то увидите, что гриппа там было очень мало. Почему? Потому, что он не особо распространялся. Потому, что если вы ограничиваете число контактов, то вы снижаете эффективное R болезни, и эпидемия заканчивается быстрее и с меньшим числом заболевших, особенно если болезнь не зоонозная, как большинство штаммов гриппа (в отличие от того же ковида, к слову).
И особенно если болезнь сезонная.
Кстати, да, про зоонозность я забыл — было бы прикольно, если бы тут взяли пример с Дании (где уничтожали норок) и Китая (где уничтожали домашних животных), добавили американского колорита и позволили добровольцам отстреливать невоспитанных тявкающих собак (которые в тявке могут потенциально выделять много вируса, ну и вообще это шумно, а я имею право на тихую и спокойную жизнь без этого гавканья вокруг). Совместить, так сказать, приятное с полезным.
в момент повышенной нагрузки на всю систему медицины
А, то есть, вы и опровергаете не то, что я говорил, и читаете не до конца? Ну это многое объясняет.
Перегрузки госпиталей в разных странах регулярно случаются и от гриппа. Более того, учитывая, что и распространение болезни, и оценка её динамики, и принятие мер имеет некоторый лаг, выглядит разумной мерой предосторожности просто без всяких условий сажаться на карантин в период гриппа.
«За»: сохранение жизни кучи людей. «Против»: хммм… а что против?
Когда с медициной все хорошо, очередей нет, делайте что хотите.
Нет, конечно, никакого «делайте что хотите» даже после того, как перегрузка госпиталей закончилась, в ковидные времена не было. Гоалпосты двигались всё дальше и дальше, two more weeks было всё больше more.
Считайте это тестом, что n — действительно обычный терм, а не костыль уровня DataKinds.
Я решил, что мне будет проще (по крайней мере, на первых порах) поддерживать код, в которых NonNegative будет дисчарджиться разработчиком.
Так а что у вас SMT-то тогда делает? Большая часть практических применений RT сводится к тому, что для использования { ν : T | ρ } там, где ожидается { ν : T | ρ' }, достаточно проверить ρ ⇒ ρ', а это вполне себе решается солверами в значимой части практически полезных применений.
Да, и я тогда ошибался, что на обычном уровне (социализация не является априори неважной), что на метауровне (потому что это было не настоящим убеждением, а скорее компенсаторной реакцией, хотя извне разница, конечно, невелика).
А у меня есть были знакомые, которые умерли от гриппа, но предложения садиться на карантин на несколько месяцев в грипповый сезон почему-то не находят должного отклика. Почему? Вам не жаль тысяч людей, погибающих от гриппа, в особо тяжёлые годы перегружающих госпитали?
Вопрос неироничный, я серьёзно жду ответ.
Ещё у меня были знакомые, которые суициднулись от карантинных мер так или иначе, а вот умерших от ковида знакомых нет. Не знаю, какие из этого выводы делать.
Не столько карантин, сколько цензуру и бан за намёки на то, что вирус мог сбежать из лабы (что сейчас вообще одна из официальных, если не основная, гипотеза). Или что правило 6 футов взято с потолка (потом все, конечно, переобулись Dr. Anthony Fauci, who headed the National Institutes of Allergy and Infectious Diseases during the height of the pandemic, told Congress that the CDC's social distancing rule was “an empiric decision that wasn’t based on data.”). Или что маски для детей взяты с потолка (оттуда же — Dr. Anthony Fauci said in congressional testimony that he reviewed no scientific evidence behind the specific recommendations for masking children or maintaining 6-foot social distancing before advocating these policies during the height of the COVID-19 pandemic.), хотя лично я детей, конечно, не люблю, а с масками им орать тяжелее, поэтому было бы прикольно, чтобы маски на детях остались с нами на всю жизнь, и я уверен, что это предложение не вызовет ни у кого никаких возражений. Или резко негативное отношение к словам о том, что подобный карантин может негативно повлиять на психическое здоровье взрослых, развитие детей, и так далее, и баланс выгоды надо бы обсудить. Или что у вакцин таки есть сайд-эффекты, и баланс рисков для каждой из групп надо бы обсудить. Или что текущие FDA'шные правила pre-trial'ов вакцин (и лекарств в целом) позволяют исключать из экспериментальной группы людей с тяжёлыми сайд-эффектами по причине «перестали следовать протоколу приёма лекарств» (канеш перестали — сайд-эффекты не дают), но не учитывать это в статистике сайд-эффектов. Или что в ряде стран «умерших с ковидом» записывали как «умерших от ковида» некоторое время, и это раздувало статистику смертности. Или всякие такие вещи.
Но все всё уже забыли, конечно. В памяти остался только карантин.
Обычное ℕ. На машинах с конечной памятью (и в тетрадках с конечным числом листов) вы вполне себе можете доказывать вещи про бесконечный ℕ.
И это на самом деле полезно, потому что как-то очень глупо перепроверять все доказательства и ждать 2^100500 времени после того, как вы просто купили железку с памятью чутка побольше.
Refinement type — это type Positive = {i: Int | i > 0}.
Плюс движок для работы с refinement'ами, чтобы Positive спокойно передавалось в функцию, ожидающую NonNegative . В этом основной смысл RT — можно сэкономить на доказательствах, которые спокойно дисчарджатся солвером.
Такие есть во всех недоязыках, претендующих на корректную имплементацию типов.
Можно весь список плз? Потому что мне известно очень мало таких языков — по большому счёту из более-менее готовых к проду это LH и F*.
Dependent type — это типы, которые зависят от других типов
От других термов.
Зависимость от других типов — это простой параметрический полиморфизм, бастардизированная версия которого есть даже в плюсах.
n — переменная типа
В нормальных завтипизированных языках это обычный терм.
У вас можно считать n из файла (или из сети) в рантайме обычной функцией toNat . readFile, получить вектор соответствующей длины (считав его тоже из файла, или replicate : (n : ℕ) → a → Vect n a) и что-то с ним сделать?
Так-то в хаскеле тоже есть DataKinds, но есть некоторые причины, почему он не завтипизированный.
переменная типа, которая может проникать в рантайм
Нет ни заказчика на этот волшебный инструмент, ни исполнителей. Иначе хотя бы Идрис допилили до хоть какого-нибудь состояния, похожего на «готов к продакшену в разумных пределах».
Ну там в хаскеле что-то шевелится на тему dependent haskell. Может, придём к готовому к проду завтипизированному языку с хорошим компилятором, просто с другой стороны. Пропозалы крутятся, завтипы мутятся.
Правда, учитывая скорость принятия (маленькую) и скоуп (ещё меньше, по пропозалу на каждую пердюшку в синтаксисе), придём туда мы году к 2050-му, не раньше.
Если к системам с конечной памятью относиться не как к реальным реализациям идеализированной бесконечной МТ, то на этих системах даже коммутативность сложения на ℕ не докажешь, потому что непонятно, терм
+-comm : (x y : ℕ) → x + y ≡ y + x
тотален «потому», что он логически консистентен и действительно выражает известное утверждение о ℕ, или же потому, что на данной конкретной машине просто тупо перебрали все влезающие в память натуральные числа, и утверждение это, соответственно, не о всех натуральных числах, а о числах меньше данного.
Зачем такое нужно, непонятно.
Правда, зачем называть обёртку над SMT прувером и ставить её в один ряд с завтипами, тоже непонятно, но это уже вопрос ОПу. Среди других вопросов ОПу: @cupraer, типобезопасный printf на вашей версии завтипов пишется? Какой положняк по экстенсиональности и всяким другим умным словам?
Слегка оффтоп, но если у вас вдруг завалялся ECS G732 (или любая его брендированная версия), то исключительно из ностальгических соображений будет интересно почитать обзор с хайрес-фоточками и вернуться в свой 2007-й 2003-й.
«Постнатальные аборты», о поддержке которых вы неоднократно писали, тоже «не являются нормой поведения». Проясните тогда сразу, сарказм ли это.
Нет. Это, на мой взгляд, наиболее консистентная с некоторыми другими вещами позиция, не зависящая от подгоняемых под ситуацию эмоций и прочих вайбов.
На хабре к комментарию можно написать ответ и спросить «а почему вы за $smth топите?» Кстати, к тому, на что вы сослались изначально, задать такой вопрос тяжелее, что, в принципе, тоже могло бы вам на что-то намекнуть.
А то может оказаться, что декларируемые вами анкап‑взгляды — один сплошной сарказм.
Может, конечно. Может оказаться, что я вообще кот и пишу эти комментарии лапками (в перерывах между поеданием выданного государством вискаса, конечно).
Не надо просто слепо слушать буковки в интернете. Буковки в интернете призваны максимум подкинуть вам чуть больше данных и чуть больше возможных цепочек рассуждений, часть которых вы могли упустить, а не заменять вам голову.
Попытка запутать собеседника печенегами и половцами story vomit‑ом не удалась
Сорри, не распарсил изначально, что именно вас смутило. Подумал, что вы какие-то фактологические нестыковки нашли, потому что несаркастическое восприятие моего коммента в том контексте мне в голову не пришло ни сегодня, ни когда я его писал изначально.
пришлось прибегнуть к гениальнейшему приёму It's a prank! «Яжпошутил», на который можно свалить буквально всё на свете.
Мне просто интересно — процитированную часть исходного комментария, на который я отвечал, вы тоже восприняли как серьёзное предложение?
Люди иногда действительно сарказмируют. Люди не всегда делают факт сарказма достаточно явным. Моя оценка вероятности не-восприятия сарказма в данном контексте очевидно неверна и занижена.
А сколько людей жалуются «Тогда я жил моментом и был раздолбаем, а лучше бы думал о будущем»?
Сколько-то жалуется, конечно.
Вы можете заметить, что я отвечал на комментарий, где прямо написано, что учёба должна стать смыслом жизни. Следовательно, предлагается устремить долю времени, выделяемого на учёбу, к 100%. «Я жил моментом» — это аналогично бредовый вариант, когда на инвестиции в будущее выделяется стремящаяся к 0% доля времени. Говорят, есть варианты где-то между.
«почти» здесь под довольно большой нагрузкой.
На работе я решаю рабочие задачи, делая то, что нужно работодателю. Нужно переложить ещё несколько жсонов — перекладываю. Нужно поковыряться в махровом легаси — ковыряюсь. Есть какой-то мерзкий неприятный баг — чиню. Нужно в 2017-м году работать с C++03, потому что махровая легаси-кодовая база не переехала на свежий компилятор, потому что от этого вылезают мерзкие баги — плююсь, но работаю. Сколько при этом я получаю фана — работодателю совершенно неважно (и чем больше платят, тем это менее важно и мне самому).
Дома я делаю то, что весело мне самому, и с нулевой ответственностью (что, пожалуй, самое главное). Баги хочу — чиню, не хочу — нет. Фичреквесты хочу — делаю, не хочу — нет. Прошлую версию компилятора хочу — поддерживаю, не хочу — нет. Не хочу — не поддерживаю даже текущую, извольте собирать clang HEAD, там же новую вкусняшку завезли! Хочу — вообще забиваю на проект. Хочу — делаю однодневку как proof-of-concept. Хочу — выбираю маргинальные инструменты и зарываюсь в yak shaving так глубоко, как хочу (захотелось сделать монте-карло-оценку разных стратегий инвестиций по историческим данным ⇒ взял идрис, а там генератора случайных чисел нормального нет ⇒ взял разобрался в PCG, начал писать реализацию ⇒ а в идрисе верифицированных битовых операций нет ⇒ пошёл делать ⇒ отвлёкся, забыл, забил, ну и пофиг, фана получил достаточно).
Ну, смысл понятен.
С точки зрения работодателя — делает. Как специалиста — делает.
А абстрактного единого «лучше» нет, есть только «лучше для $X». Вот что лучше — велосипед или самолёт?
На всякий случай — работаю удалённо, в средний будний день часов 6 в день работа съедает, физическая активность — три похода в тренажерку в неделю по два часа каждый, в качестве пет-проектов сейчас в основном зашариваю разный матан, по 3-4 часа в будний день уходит (и в пару раз больше в выходные), плюс просто читаю всякую ерунду — от блогов до статей с arxiv и этак сорокета книг в год. Ну и ещё всякая мелочёвка есть на несколько часов.
Детей и семьи нет (этого я никогда не хотел), и не жалею об этом. Жалею, что в вузовские годы «не нагулялся», факт (и мета-жалею о том, что разрешил себе в этом признаться только совсем недавно), но эти годы уже всё равно не вернёшь, а сейчас контекст не тот. Да и в вузе было жёстче, чем на работе, и после пар всё равно приходилось заниматься самообразованием. Стоило не поддаваться на peer pressure и идти в халявный вуз только ради отмазы от армии, где надо появляться дважды в год на сессии — всё равно толку с этих всех урматов, диффуров и функанов на работе нет, а для меня самого мне сильно интереснее немного другие ветви математики, которых в вузе нет.
Норм?
На 10" мне уже было мелковато (даже с тримом полей), но YMMV, конечно.
Onyx Boox топ. У меня Tab X, хреновина такая на 13 дюймов, читать в альбомном режиме папиры и монографии в pdf по две страницы на экран самое то.
Если сама статья в две колонки, то получается видно четыре сразу, тоже вполне себе норм.
Один из вариантов — таки типобезопасный printf. Вон, плюсисты нетривиально приседают, чтобы в std::fmt (или как его там, не игрался на практике с этой частью новых плюсов) известные в компилтайме строки позволяли проверять типы аргументов. В шланге и gcc добавили проверки (и аннотации для кастомных строк), чтобы проверять соответствие строки формата аргументам у обычного сишного printf. Наверное, это нужно.
Другой вариант из личной практики, когда я по фану делал на идрисе обёртку вокруг постгреса — можно описать структуру таблицы обычным языком термов, и потом обычными функциями
Schema → Typeсоздать что тип, значения которого соответствуют схеме, что все эти обёртки над create table / insert / update / etc.В мейнстримных языках для этого обмазываются какой-нибудь рефлексией, и всё даёт нечитаемые ошибки и разваливается (в рантайме, если рефлексия — рантайм).
Я на всякий случай уточню: вы правда не понимаете, что доказательства могут быть не только про тот диапазон чисел, чем я считаю сдачу в магазине?
Проверка тотальности через прямой перебор состояний не доступна ни для какого полезного на практике в более чем полутора приложениях m.
Зачем вы опровергаете то, что я не говорил и даже не подразумевал?
Карантин нужен для остановки болезни в том числе. Если вы посмотрите статистику по гриппу за 2020-й и 2021-й, особенно в странах с сильными карантинными мерами, то увидите, что гриппа там было очень мало. Почему? Потому, что он не особо распространялся. Потому, что если вы ограничиваете число контактов, то вы снижаете эффективное R болезни, и эпидемия заканчивается быстрее и с меньшим числом заболевших, особенно если болезнь не зоонозная, как большинство штаммов гриппа (в отличие от того же ковида, к слову).
И особенно если болезнь сезонная.
Кстати, да, про зоонозность я забыл — было бы прикольно, если бы тут взяли пример с Дании (где уничтожали норок) и Китая (где уничтожали домашних животных), добавили американского колорита и позволили добровольцам отстреливать невоспитанных тявкающих собак (которые в тявке могут потенциально выделять много вируса, ну и вообще это шумно, а я имею право на тихую и спокойную жизнь без этого гавканья вокруг). Совместить, так сказать, приятное с полезным.
А, то есть, вы и опровергаете не то, что я говорил, и читаете не до конца? Ну это многое объясняет.
Перегрузки госпиталей в разных странах регулярно случаются и от гриппа. Более того, учитывая, что и распространение болезни, и оценка её динамики, и принятие мер имеет некоторый лаг, выглядит разумной мерой предосторожности просто без всяких условий сажаться на карантин в период гриппа.
«За»: сохранение жизни кучи людей.
«Против»: хммм… а что против?
Нет, конечно, никакого «делайте что хотите» даже после того, как перегрузка госпиталей закончилась, в ковидные времена не было. Гоалпосты двигались всё дальше и дальше, two more weeks было всё больше more.
И, кстати, совсем забыл: там ещё доказывается, что ∃ n. n + 1 = 0, что неверно для натуральных чисел. Поэтому, короче, это очень вредная модель.
Считайте это тестом, что
n— действительно обычный терм, а не костыль уровняDataKinds.Так а что у вас SMT-то тогда делает? Большая часть практических применений RT сводится к тому, что для использования { ν : T | ρ } там, где ожидается { ν : T | ρ' }, достаточно проверить ρ ⇒ ρ', а это вполне себе решается солверами в значимой части практически полезных применений.
Да, и я тогда ошибался, что на обычном уровне (социализация не является априори неважной), что на метауровне (потому что это было не настоящим убеждением, а скорее компенсаторной реакцией, хотя извне разница, конечно, невелика).
А у меня
естьбыли знакомые, которые умерли от гриппа, но предложения садиться на карантин на несколько месяцев в грипповый сезон почему-то не находят должного отклика. Почему? Вам не жаль тысяч людей, погибающих от гриппа, в особо тяжёлые годы перегружающих госпитали?Вопрос неироничный, я серьёзно жду ответ.
Ещё у меня были знакомые, которые суициднулись от карантинных мер так или иначе, а вот умерших от ковида знакомых нет. Не знаю, какие из этого выводы делать.
Не столько карантин, сколько цензуру и бан за намёки на то, что вирус мог сбежать из лабы (что сейчас вообще одна из официальных, если не основная, гипотеза). Или что правило 6 футов взято с потолка (потом все, конечно, переобулись Dr. Anthony Fauci, who headed the National Institutes of Allergy and Infectious Diseases during the height of the pandemic, told Congress that the CDC's social distancing rule was “an empiric decision that wasn’t based on data.”). Или что маски для детей взяты с потолка (оттуда же — Dr. Anthony Fauci said in congressional testimony that he reviewed no scientific evidence behind the specific recommendations for masking children or maintaining 6-foot social distancing before advocating these policies during the height of the COVID-19 pandemic.), хотя лично я детей, конечно, не люблю, а с масками им орать тяжелее, поэтому было бы прикольно, чтобы маски на детях остались с нами на всю жизнь, и я уверен, что это предложение не вызовет ни у кого никаких возражений. Или резко негативное отношение к словам о том, что подобный карантин может негативно повлиять на психическое здоровье взрослых, развитие детей, и так далее, и баланс выгоды надо бы обсудить. Или что у вакцин таки есть сайд-эффекты, и баланс рисков для каждой из групп надо бы обсудить. Или что текущие FDA'шные правила pre-trial'ов вакцин (и лекарств в целом) позволяют исключать из экспериментальной группы людей с тяжёлыми сайд-эффектами по причине «перестали следовать протоколу приёма лекарств» (канеш перестали — сайд-эффекты не дают), но не учитывать это в статистике сайд-эффектов. Или что в ряде стран «умерших с ковидом» записывали как «умерших от ковида» некоторое время, и это раздувало статистику смертности. Или всякие такие вещи.
Но все всё уже забыли, конечно. В памяти остался только карантин.
Имея и ложноположительные, и, что хуже, ложноотрицательные срабатывания.
Обычное ℕ. На машинах с конечной памятью (и в тетрадках с конечным числом листов) вы вполне себе можете доказывать вещи про бесконечный ℕ.
И это на самом деле полезно, потому что как-то очень глупо перепроверять все доказательства и ждать 2^100500 времени после того, как вы просто купили железку с памятью чутка побольше.
Тут дело не в IO (считайте, что это sprintf, а не printf), а в том, что в полноценных завтипах вы можете написать функцию вроде
и потом
после чего, скажем, у
printf "Age: %d, weight: %f"будет типInt → Float → StringПлюс движок для работы с refinement'ами, чтобы
Positiveспокойно передавалось в функцию, ожидающуюNonNegative. В этом основной смысл RT — можно сэкономить на доказательствах, которые спокойно дисчарджатся солвером.Можно весь список плз? Потому что мне известно очень мало таких языков — по большому счёту из более-менее готовых к проду это LH и F*.
От других термов.
Зависимость от других типов — это простой параметрический полиморфизм, бастардизированная версия которого есть даже в плюсах.
В нормальных завтипизированных языках это обычный терм.
У вас можно считать
nиз файла (или из сети) в рантайме обычной функциейtoNat . readFile, получить вектор соответствующей длины (считав его тоже из файла, илиreplicate : (n : ℕ) → a → Vect n a) и что-то с ним сделать?Так-то в хаскеле тоже есть
DataKinds, но есть некоторые причины, почему он не завтипизированный.В 2025-м ожидаешь, что это можно контролировать. Например, ИМХО самая доступная статья на тему — https://dl.acm.org/doi/pdf/10.1145/3408973
Ну там в хаскеле что-то шевелится на тему dependent haskell. Может, придём к готовому к проду завтипизированному языку с хорошим компилятором, просто с другой стороны. Пропозалы крутятся, завтипы мутятся.
Правда, учитывая скорость принятия (маленькую) и скоуп (ещё меньше, по пропозалу на каждую пердюшку в синтаксисе), придём туда мы году к 2050-му, не раньше.
Если к системам с конечной памятью относиться не как к реальным реализациям идеализированной бесконечной МТ, то на этих системах даже коммутативность сложения на ℕ не докажешь, потому что непонятно, терм
тотален «потому», что он логически консистентен и действительно выражает известное утверждение о ℕ, или же потому, что на данной конкретной машине просто тупо перебрали все влезающие в память натуральные числа, и утверждение это, соответственно, не о всех натуральных числах, а о числах меньше данного.
Зачем такое нужно, непонятно.
Правда, зачем называть обёртку над SMT прувером и ставить её в один ряд с завтипами, тоже непонятно, но это уже вопрос ОПу. Среди других вопросов ОПу: @cupraer, типобезопасный printf на вашей версии завтипов пишется? Какой положняк по экстенсиональности и всяким другим умным словам?
Слегка оффтоп, но если у вас вдруг завалялся ECS G732 (или любая его брендированная версия), то исключительно из ностальгических соображений будет интересно почитать обзор с хайрес-фоточками и вернуться в свой
2007-й2003-й.Нет. Это, на мой взгляд, наиболее консистентная с некоторыми другими вещами позиция, не зависящая от подгоняемых под ситуацию эмоций и прочих вайбов.
На хабре к комментарию можно написать ответ и спросить «а почему вы за $smth топите?» Кстати, к тому, на что вы сослались изначально, задать такой вопрос тяжелее, что, в принципе, тоже могло бы вам на что-то намекнуть.
Может, конечно. Может оказаться, что я вообще кот и пишу эти комментарии лапками (в перерывах между поеданием выданного государством вискаса, конечно).
Не надо просто слепо слушать буковки в интернете. Буковки в интернете призваны максимум подкинуть вам чуть больше данных и чуть больше возможных цепочек рассуждений, часть которых вы могли упустить, а не заменять вам голову.
Сорри, не распарсил изначально, что именно вас смутило. Подумал, что вы какие-то фактологические нестыковки нашли, потому что несаркастическое восприятие моего коммента в том контексте мне в голову не пришло ни сегодня, ни когда я его писал изначально.
Мне просто интересно — процитированную часть исходного комментария, на который я отвечал, вы тоже восприняли как серьёзное предложение?
Люди иногда действительно сарказмируют. Люди не всегда делают факт сарказма достаточно явным. Моя оценка вероятности не-восприятия сарказма в данном контексте очевидно неверна и занижена.
Сколько-то жалуется, конечно.
Вы можете заметить, что я отвечал на комментарий, где прямо написано, что учёба должна стать смыслом жизни. Следовательно, предлагается устремить долю времени, выделяемого на учёбу, к 100%. «Я жил моментом» — это аналогично бредовый вариант, когда на инвестиции в будущее выделяется стремящаяся к 0% доля времени. Говорят, есть варианты где-то между.