В N+1-й раз напишу вам, что ФП не отрицает мутабельность. ФП отрицает неуказание эффектов в типах.
Так как я пишу это в N+1-й раз для сильно ненулевого N, то позволю себе спросить: зачем вы из треда в тред ходите с похожими мифами и тезисами, и как только вам указывают на неконсистентность или некорректность ваших высказываний, вы из треда пропадаете, чтобы через какое-то время снова появиться в другом треде с тем же самым?
Советуете почитать конкретно с точки зрения честности изложения?
Я не нашёл существенных изъянов и биасов, особенно в первой из книг. «The Vision», конечно, биаснута, потому что показывает ментальную акробатику соответствующих людей, но каких-то серьёзных косяков и там не заметил (хотя, опять же, не со всем согласен).
У Соуэла в Basic Economics - просто постоянно biased примеры.
Basic Economics у него я не читал, а, кстати, интересно!
(ну условно сравнил мат-ожидание "парвильной страны" с медианой "неправильной страны")
Для некоторых распределений это норм, кстати. И чем более равномерное распределение (если говорить о доходах, например, к этому вроде даже стремятся), тем ближе матожидание к медиане.
Это я бы сказал «ну вообще в чём проблема с поиском работы, что вы всё переживаете и дрючите литкод, посмотрите вообще каких клоунов нанимают, и у меня никаких проблем с этим никогда не было, я просто не парюсь».
А потом надо искать фиксированную точку. Например, простой итерацией. Или двух фазным вычислением как в NSpice (первая фаза грубая, вторая - Ньютон-Рафсон).
Ой всё. Я лучше уволюсь, чем буду формализовывать вот эти все вычислительные методы.
Это всё проще в SMT загнать, сформулировать ограничения в терминах допусков, и пусть оно там проверяет.
То есть, получается, что типы простые, без полиморфизма, без функций высших порядков (можно их добавить, но это только усложнит инструмент без пользы). С другой стороны, ограничения явно есть, но не очень понятно пока, какие именно.
Ну как всегда — попробуй накидать примеры программ, какие ограничения хотелось бы навесить, а там уже можно будет делать выводы, наверное.
Опять же, я, к сожалению, предметную область дальше курса общефиза не знаю (и общефиз был давно), поэтому интуиции здесь у меня нет.
Но они же получаются связаны через функцию! То есть, для определения точного типа b нужно знать a.
Да, RT — это подвид зависимых типов. С некоторыми оговорками можно воспринимать их как сигма-типы (где, как я теперь знаю, второй аргумент стёрт aka рантайм-иррелевантен).
Там есть теоремы, с какими наборами подобных условий можно работать?
В общем виде — нет (и что-то окологёделевское говорит нам, что алгоритма, разрешающего разрешимость теории, не существует). Но в твоём случае вроде как достаточно стандартного SMT, и это хорошо: не надо заморачиваться.
Хотя в случае небольших количеств переменных (до десятков тысяч), с условно паскалевской изначальной системой типов, должно позволять добавление вот этих ограничений из твоего примера легко, верно?
Более-менее лёгкую арифметику — да.
И даже Z3 не надо - можно для таких размеров (до 10к переменных) всё сделать самостоятельно, да?
Если тебе охота поиграться с самодельным солвером, я бы делал это как отдельный проект :]
SMT очень нетривиальные, с кучей крайних случаев, и они могут подыхать даже на довольно малых наборах констрейнтов. Десятки тысяч переменных — это уже дофига. Лучше дёргать какой-нибудь z3 (haskell-z3 норм байндинги) или за вечер наваять парсер/генератор smtlib-секспров и не париться. Мы для верификации смарт-контрактов именно так и делали (хотя у нас были отдельные пассы для всяких предметно-специфичных вещей до солвера, но это отдельная и не очень релевантная история).
Меня всегда забавляет¹, как люди по сути требуют от других продемонстрировать их регалии перед тем, как хотя бы даже попытаться воспринять их слова по существу, хотя сами не делают ничего: не демонстрируют собственных достижений (что необходимо в их логике), да и даже не говорят ничего по существу, вместо этого размахивая вокруг вялым адхомом.
¹ вру, раньше расстраивало, а забавляет только последние пару лет
В данном случае, правда, границы чисто синтаксические: вы просто сэмплите не только случайных противников из толпы, но и случайные дисциплины. Свойства категории множеств позволяют переобозначить пары ⟨ противник , дисциплина ⟩ как противник', а соревнование с данным противником в данной дисциплине как игру в шахматы'.
Вы-то говорите, что если этот Вася выигрывает, то и другой Вася выиграет, потому, что оба - Васи.
В данном случае Вася — это определённая кульутра и научная школа. В бинаризованном случае у вас есть ненулевая вероятность, что Вася тот же (научная школа и культура сохранились), и прошлые исходы (косвенно) дают информацию о будущих, и есть ненулевая вероятность, что Васю подменили, и тогда прошлые исходы не дают никакой информации. Легко видеть, что при ненулевой вероятности сохранения Васи при прочих равных (или в отсутствие любой другой информации) наиболее эффективное решение совпадает с тем, как если бы вы считали, что Вася сохранился и остался тем же.
Понятно, что на самом деле там не бинарная вероятность, а вещественный спектр, но идея остаётся та же, просто сумма заменяется интегралом.
Надо просто мыслить вероятностными пространствами, а не скалярами, и всё будет нормально.
Я всё о своих схемах думаю — там именно появляются ограничения, и естественным образом это превращается в типы. С другой стороны, поскольку задача ещё не до конца сформулирована, я в некотором смысле «рисую цель там, куда могу попасть». Но мне нужно знать примерный ландшафт.
Я, к сожалению, про cad знаю слишком мало, чтобы вообще что-то по делу тут предлагать. Нутром чую, что RT тут не сильно помогут, но буду рад ошибиться.
Это работа с Ричадом?
Да.
Но тогда это тип функции, верно?
Это тип одного из аргументов, который торчит в типе функции. Весь тип функции выглядит где-то как
{ a : ℝ | True } → { b : ℝ | a ≥ b } → { r : ℝ | r × r = a - b }
(refinement на r можно ослабить, понятное дело)
То есть, из предметной области вытаскиваем язык (алгебру в терминах ADD)
В таком виде у этого языка не нужна предметно-специфичная система типов. Все нужные ограничения выражаются завтипами на сами элементы алгебры.
Так что вот оно — «настоящее программирование», а не «перекладывание JSON'ов».
Нет, это не ошибка горячей руки, потому что здесь нет случайного события (да и в большинстве случаев применения термина «ошибка горячей руки» искомые события тоже не были совсем случайными — у когнитивного искажения, сводящегося к некорректному применению лейблов других когнитивных искажений, наверняка тоже есть какое-нибудь название).
Если Вася систематически выигрывает в шахматы у рандомно взятого из толпы человека, то это повышает шансы, что он выиграет и у следующего рандомно взятого из толпы человека просто потому, что наблюдаемые данные («Вася выигрывает») повышают вероятность того, что мы живём в мире, где Вася действительно хороший шахматист на фоне среднего человека.
Конечно, процитированную вами фразу вашего исходного собеседника надо исправить на «и скорее всего так будет с Китаем», но на практике при человеческом языке отсылка к вероятностному мышлению опускается.
Как это происходит у меня: работодатель за меня отчисляет соответствующий процент. Работодателю можно сказать «two or more jobs», и он будет отчислять больший процент, как если бы я работал на двух работах с примерно одинаковой зарплатой. Кроме того, работодателя можно попросить отчислять больше (а потом переплату получить при налоговом возврате).
Что будет, если я недоплачу в течение года и окажусь должен при оформлении налогового возврата (не зря он называется возвратом)? Естественно, налоговая попросит доплатить. Кроме того, налоговая (или turbotax, хз) скажет, сколько мне платить заранее дополнительно к работодательским вычетам в следующем году примерно раз в квартал. Если я не буду платить эту сумму и задолжаю налоговой и в следующем году, то мне будет штраф. Если буду и задолжаю — вероятно, не будет.
Пистолет не сильно сложно носить так, чтобы его не было видно. Как применять эту статью без обшманывания людей на ровном месте (что запрещено Четвёртой поправкой)? Для шмона нужен reasonable suspicion, а «идёт какой-то чувак в худи и руки в карманах» так себе reasonable suspicion.
Тем более, какое за неё наказание? В тюрьму посадят? Так обсуждаемым лицам от этого ни холодно, ни жарко. От этого плохо только законопослушным гражданам с работой, условно, которые и так никого грабить не собираются.
Плюс, объясните, пожалуйста, почему в Чикаго (где одни из самых серьёзных оружейных ограничений во всей стране) всё так плохо с перестрелками, бандами и смертностью от этого всего?
Для пистолетов с глушителем разрешение получить невозможно, а наказания там серьезные.
Зачем вам глушитель? Я систематически бываю в местах, где в радиусе километра от меня нет никого, и глушитель потенциальному злодею тут совсем не нужен, чтобы сделать мне бо-бо в вашей парадигме.
А полиция нужна, чтобы преследовать нарушителей неопределенно долго.
Бедный голодный бандит прошёл с пистолетом на дело, но не прокатило, не было жертвы. Как тут преследовать неопределённо долго?
Но так какой-то же процент все-таки раскрывается!
А какой-то процент самозащищается, и?
Не думаю, что корреляция здесь из-за самих регуляций.
Нет, конечно, регуляции тут не являются причиной, наоборот: более серьёзные ограничения, казалось бы, должны бы упростить работу полиции, а мы этого не наблюдаем.
Я тоже считаю, что разрешение на владение/ношение/применение оружия это одно из необходимейших условий для создания гармоничного общества.
Вопрос в том, какие у этого разрешения должны быть условия. С одной стороны есть constitutional carry (когда лицензий не нужно, покупай пукалку с магазином любой ёмкости, любой рукоятью, любым калибром, и так далее, и носи), а с другой — «объясните, зачем вам, подождите 15 дней, покажите ваши социальные сети, и тогда мы, может быть, выпишем разрешение на покупку, но винтовку с магазином больше чем на 5 патронов или пистолетной рукоятью, или пистолет на 10, вы всё равно не купите».
Неправильное расходование налогов, как и их полное отсутствие, не приносит каких-то значимых плюсов для общества в целом.
Я склонен считать, что государственное вмешательство и регуляции интегрально делают хуже.
Вы и ваши коллеги не в том перцентиле находитесь, чтобы ощущать преимущества системы налогообложения.
Во-первых, я говорил не про это, а про то, что работодатели впрягаются и без государственной палки.
Во-вторых, да, и?
В-третьих, этот перцентиль больше, чем вам кажется.
Да, эффективность госаппарата это сложный вопрос. Есть разные подходы к его решению.
Ни одно из которых не работает, потому что у государства никогда не будет стимулов быть эффективным (исключая всякие сценарии из ненаучной фантастики типа ошейников со взрывчаткой на чиновниках).
Вы почему-то считаете, что если бы налогов не было, то работодатель давал бы вам всю эту сумму на руки, и поэтому проводите аналогии с воровством.
Эта сумма была бы другой, но её покупательная способность была бы эквивалентной, поэтому на эту разницу (сводящуюся к курсу конвертации между сегодняшним тугриком и безналоговым тугриком) можно забить и считать всё в сегодняшних тугриках.
Почему эквивалентной? Потому, что если работодатель под меня выделяет 187 тысяч на ФОТ, значит, я ему приношу пользы на ≥187 тысяч. Есть, конечно, нерыночные инструменты влияния государства на рынок труда вроде ввода определённых квот, например, но ни под одну из этих квот я не попадаю, а проблемы бездельников меня не очень интересуют. И, кстати, если снизить число бездельников в штате, то количество свободных денег у работодателя повысится — снова мне профит!
Если вы получаете 2000 на руки и 1000 налогов, значит вы согласились получать 2000, и если бы налогов не было, работодатель бы вам платил те же 2000, а 1000 оставлял себе.
В текущем рынке.
В безналоговом рынке у соседнего работодателя есть стимул меня переманить, предложив оплату чуть больше (потому что он может потратить часть этих 1000), и так далее итеративно до тех пор, пока моя зарплата не придёт к плюс-минус такому же балансу полезности для работодателя.
А если бы не было социальных институтов типа полиции, как вы предлагаете, на которые идут эти налоги, он бы нанимал себе охрану и платил 2000 им, потому что в таких условиях они просто так рисковать не будут, а вам бы оставалась та же 1000.
Как хорошо эти институты работают, я мог наблюдать всё своё время в Нью-Йорке, и особенно ярко — в 2020-м, когда менты вставали на колено и занимались прочей показухой, а агенство сдачи недвиги в доме, где я жил, и так наняло ЧОПовцев в районе начала июня, и так и продолжало их кормить до где-то сентября-октября, задолго после того, как я оттуда съехал.
Защита полиции — это миф. Полиция защищает не вас, а государственную систему.
Общего у моего вопроса и вашего ответа только слово в синтаксическом смысле «рассуждать». Даже семантика у него разная в этих случаях: я говорю о том, что «смотрю на кусок кода и пытаюсь понять, что он делает и чего он не делает», вы говорите о том, как бы сделать компиляцию всего проекта побыстрее, если он компилируется слишком долго.
А можете пояснить, как именно распараллелится код Мартина? Мне этот код тяжело читать (оптимизатору проще будет, конечно), но там, похоже, зависимость следующей итерации от результата предыдущей.
Под refinement types разные люди понимают разное, поэтому на него нет единого ответа, и вопрос вроде «какие ограничения подходят для системы типов», я бы сказал, даже не особо имеет смысла. Вопрос скорее в задачах.
В самом общем виде это типы вида { ν : T | P(ν) }, где P может быть достаточно произвольным (включая что-нибудь очевидно неразрешимое вида «ν-ая машина Тьюринга останавливается на входе ν»). Дальше в зависимости от твоих целей можно начинать ограничивать эти P. Хочешь лёгкость программирования, и чтобы машина всё сама решала, а ты о пруфтермах не думал? Ограничиваешься разрешимым подмножеством, или хотя бы тем, что какие-нибудь там SMT-солверы жрут в среднем нормально. Хочешь, чтобы язык был выразительным и позволял любые инварианты в типах? Разрешаешь весь term language там, но получаешь алгоритмическую неразрешимость proof finding'а и требование от машины ей помочь найти доказательства.
Собсна, если я правильно помню соответствующий папир, классические liquid types из liquid haskell — это именно ограничение предикатов на SMT-разрешимое подмножество языка, и чтобы машина там всё сама доказывала (или конструктивно опровергала).
Я же в третьем пункте из предыдущего комментария пытался совместить удобоваримый для продакшен-программирования и SMT-разрешимый язык RT с полноценными завтипизированными DT, но уткнулся в отсутствие прямой симуляции refinement types зависимыми типами (что мешало даже сформулировать правильные теоремы о том, что трансляция RT → DT «имеет смысл» и «сохраняет операционную семантику»), потому что тогда не знал про разные возможности выражать термы как вычислительно неважные на уровне метатеории, но это совсем другая история.
И вопрос по связи ограничений - если у меня есть функцияshifted_sqrt a b = sqrt (a - b), в которой есть ограничение a > b, то это тоже случай refinement types?
Да, если это ограничение выражено в понятной для RT-тайпчекера форме (но лучше таки a ≥ b).
Это так происходит пока законопослушные граждане ходят без калашей. А если они будут с оружием (и без полиции), то сначала в них будут стрелять из пистолетов с глушителями, а потом уже грабить. На все про все уйдет секунд 10-20. И, если рядом никого не будет, то шансов на выживание у жертвы никаких.
Плохие парни де-факто могут обзавестись пистолетом с глушителем уже сейчас. Какая именно магическая пыль каких именно государственных феечек гарантирует безопасность законопослушного жителя сегодня (когда мы платим налоги) в таких ситуациях без людей вокруг и без полиции?
Напомню, что в Штатах (не)раскрываемость убийств — в районе 50%, а в отдельных местах, например, в городах Калифорнии (что дико зарегулированной по оружию, где глушитель или fully semiautomatic military-style mass-shooting-capacity magazine assault rifle хрен купишь легально, что имеющей одни из самых высоких налогов), самая низкая раскрываемость в 36%.
Кроме того, в Техасе, где оружие везде и для его получения и ношения даже лицензии не надо, существенно безопаснее, чем в Нью-Йорке (городе), где с ним как в худших локациях Калифорнии. Если бы у меня была девушка, я бы едва ли отпустил её гулять после заката солнца по Манхеттену (особенно по Централ Парку какому, хотя там людей порядком, или ездить по метро) или, тем более, Бронксу, а здесь, вне метрополий — да спокойно. В Централ Парке мне самому было несколько стрёмно, а здесь я спокойно могу гулять по безлюдным местам в 11 вечера (и именно потому, что за поясом у меня S&W, и проходящий мимо человек знает, что у меня оно может быть, и рисковать ради кредитной карточки… ну такое).
Я уж не говорю о том, что даже если бы arguendo вы были правы, то платить овер 100 тысяч в год за возможность погулять там, где никого нет… хз.
Мне кажется, вы проецируете нынешние паттерны поведения, которые зависят от нынешнего законодательства, на совершенно другую среду.
Текущее законодательство штрафует законопослушных людей и стоит на стороне преступников.
С их достижениями уже все свыклись
А какие достижения? Сокращение рабочего дня выбили не они, если что, а началось всё с Форда и ко, которые заметили, что люди так просто эффективнее (капиталисты клятые).
Я в США работаю, и работаю на компании, дающие сильно больше гибкости, свобод и ништяков, чем требуется (околонулевым по меркам других стран) трудовым законодательством (в чём тут завоевания социал-демократов?). И этот опыт сильно лучше опыта работы на европейцев.
я и за налоговую систему (с хорошей полицией)
Полиция никогда не будет защищать вас, потому что не вы конкретный ей платите деньги. От того, что она профукает вашу защиту, полиции ничего не будет. Поэтому у нас будут дела вроде Warren v. DC (прямо кодифицирующие, что полиция не обязана вас защищать), либо будет Увальде, когда несколько десятков ссыкунов, устроившихся в полицию только ради государственной пенсии и прочих ништяков, не будут ничего делать полтора часа и будут не давать родителям (вооружённым, ага) что-то сделать.
Основная цель полиции — создать иллюзию защищённости в среднем, чтобы у электората (опять же, в среднем) не было вопросов к государству. Что при этом происходит на самом деле, совершенно неважно, пока есть эта иллюзия.
В N+1-й раз напишу вам, что ФП не отрицает мутабельность. ФП отрицает неуказание эффектов в типах.
Так как я пишу это в N+1-й раз для сильно ненулевого N, то позволю себе спросить: зачем вы из треда в тред ходите с похожими мифами и тезисами, и как только вам указывают на неконсистентность или некорректность ваших высказываний, вы из треда пропадаете, чтобы через какое-то время снова появиться в другом треде с тем же самым?
Я не нашёл существенных изъянов и биасов, особенно в первой из книг. «The Vision», конечно, биаснута, потому что показывает ментальную акробатику соответствующих людей, но каких-то серьёзных косяков и там не заметил (хотя, опять же, не со всем согласен).
Basic Economics у него я не читал, а, кстати, интересно!
Для некоторых распределений это норм, кстати. И чем более равномерное распределение (если говорить о доходах, например, к этому вроде даже стремятся), тем ближе матожидание к медиане.
Ну и славно: тогда точно не позвонят в три часа ночи, что в продакшене что-то упало.
Это я бы сказал «ну вообще в чём проблема с поиском работы, что вы всё переживаете и дрючите литкод, посмотрите вообще каких клоунов нанимают, и у меня никаких проблем с этим никогда не было, я просто не парюсь».
Ложное обобщение.
Ой всё. Я лучше уволюсь, чем буду формализовывать вот эти все вычислительные методы.
Это всё проще в SMT загнать, сформулировать ограничения в терминах допусков, и пусть оно там проверяет.
Ну как всегда — попробуй накидать примеры программ, какие ограничения хотелось бы навесить, а там уже можно будет делать выводы, наверное.
Опять же, я, к сожалению, предметную область дальше курса общефиза не знаю (и общефиз был давно), поэтому интуиции здесь у меня нет.
Да, RT — это подвид зависимых типов. С некоторыми оговорками можно воспринимать их как сигма-типы (где, как я теперь знаю, второй аргумент стёрт aka рантайм-иррелевантен).
В общем виде — нет (и что-то окологёделевское говорит нам, что алгоритма, разрешающего разрешимость теории, не существует). Но в твоём случае вроде как достаточно стандартного SMT, и это хорошо: не надо заморачиваться.
Более-менее лёгкую арифметику — да.
Если тебе охота поиграться с самодельным солвером, я бы делал это как отдельный проект :]
SMT очень нетривиальные, с кучей крайних случаев, и они могут подыхать даже на довольно малых наборах констрейнтов. Десятки тысяч переменных — это уже дофига. Лучше дёргать какой-нибудь z3 (haskell-z3 норм байндинги) или за вечер наваять парсер/генератор smtlib-секспров и не париться. Мы для верификации смарт-контрактов именно так и делали (хотя у нас были отдельные пассы для всяких предметно-специфичных вещей до солвера, но это отдельная и не очень релевантная история).
Конечно. Всё самое интересное случается в комплитайме.
Меня всегда забавляет¹, как люди по сути требуют от других продемонстрировать их регалии перед тем, как хотя бы даже попытаться воспринять их слова по существу, хотя сами не делают ничего: не демонстрируют собственных достижений (что необходимо в их логике), да и даже не говорят ничего по существу, вместо этого размахивая вокруг вялым адхомом.
¹ вру, раньше расстраивало, а забавляет только последние пару лет
У каждой аналогии свои границы применимости.
В данном случае, правда, границы чисто синтаксические: вы просто сэмплите не только случайных противников из толпы, но и случайные дисциплины. Свойства категории множеств позволяют переобозначить пары ⟨ противник , дисциплина ⟩ как противник', а соревнование с данным противником в данной дисциплине как игру в шахматы'.
В данном случае Вася — это определённая кульутра и научная школа. В бинаризованном случае у вас есть ненулевая вероятность, что Вася тот же (научная школа и культура сохранились), и прошлые исходы (косвенно) дают информацию о будущих, и есть ненулевая вероятность, что Васю подменили, и тогда прошлые исходы не дают никакой информации. Легко видеть, что при ненулевой вероятности сохранения Васи при прочих равных (или в отсутствие любой другой информации) наиболее эффективное решение совпадает с тем, как если бы вы считали, что Вася сохранился и остался тем же.
Понятно, что на самом деле там не бинарная вероятность, а вещественный спектр, но идея остаётся та же, просто сумма заменяется интегралом.
Надо просто мыслить вероятностными пространствами, а не скалярами, и всё будет нормально.
Я, к сожалению, про cad знаю слишком мало, чтобы вообще что-то по делу тут предлагать. Нутром чую, что RT тут не сильно помогут, но буду рад ошибиться.
Да.
Это тип одного из аргументов, который торчит в типе функции. Весь тип функции выглядит где-то как
(refinement на r можно ослабить, понятное дело)
В таком виде у этого языка не нужна предметно-специфичная система типов. Все нужные ограничения выражаются завтипами на сами элементы алгебры.
Только не нужно никому, и бабок не платят, увы.
Нет, это не ошибка горячей руки, потому что здесь нет случайного события (да и в большинстве случаев применения термина «ошибка горячей руки» искомые события тоже не были совсем случайными — у когнитивного искажения, сводящегося к некорректному применению лейблов других когнитивных искажений, наверняка тоже есть какое-нибудь название).
Если Вася систематически выигрывает в шахматы у рандомно взятого из толпы человека, то это повышает шансы, что он выиграет и у следующего рандомно взятого из толпы человека просто потому, что наблюдаемые данные («Вася выигрывает») повышают вероятность того, что мы живём в мире, где Вася действительно хороший шахматист на фоне среднего человека.
Конечно, процитированную вами фразу вашего исходного собеседника надо исправить на «и скорее всего так будет с Китаем», но на практике при человеческом языке отсылка к вероятностному мышлению опускается.
Как это происходит у меня: работодатель за меня отчисляет соответствующий процент. Работодателю можно сказать «two or more jobs», и он будет отчислять больший процент, как если бы я работал на двух работах с примерно одинаковой зарплатой. Кроме того, работодателя можно попросить отчислять больше (а потом переплату получить при налоговом возврате).
Что будет, если я недоплачу в течение года и окажусь должен при оформлении налогового возврата (не зря он называется возвратом)? Естественно, налоговая попросит доплатить. Кроме того, налоговая (или turbotax, хз) скажет, сколько мне платить заранее дополнительно к работодательским вычетам в следующем году примерно раз в квартал. Если я не буду платить эту сумму и задолжаю налоговой и в следующем году, то мне будет штраф. Если буду и задолжаю — вероятно, не будет.
Как тут говорят, unenforceable.
Пистолет не сильно сложно носить так, чтобы его не было видно. Как применять эту статью без обшманывания людей на ровном месте (что запрещено Четвёртой поправкой)? Для шмона нужен reasonable suspicion, а «идёт какой-то чувак в худи и руки в карманах» так себе reasonable suspicion.
Тем более, какое за неё наказание? В тюрьму посадят? Так обсуждаемым лицам от этого ни холодно, ни жарко. От этого плохо только законопослушным гражданам с работой, условно, которые и так никого грабить не собираются.
Плюс, объясните, пожалуйста, почему в Чикаго (где одни из самых серьёзных оружейных ограничений во всей стране) всё так плохо с перестрелками, бандами и смертностью от этого всего?
Зачем вам глушитель? Я систематически бываю в местах, где в радиусе километра от меня нет никого, и глушитель потенциальному злодею тут совсем не нужен, чтобы сделать мне бо-бо в вашей парадигме.
Бедный голодный бандит прошёл с пистолетом на дело, но не прокатило, не было жертвы. Как тут преследовать неопределённо долго?
А какой-то процент самозащищается, и?
Нет, конечно, регуляции тут не являются причиной, наоборот: более серьёзные ограничения, казалось бы, должны бы упростить работу полиции, а мы этого не наблюдаем.
Вопрос в том, какие у этого разрешения должны быть условия. С одной стороны есть constitutional carry (когда лицензий не нужно, покупай пукалку с магазином любой ёмкости, любой рукоятью, любым калибром, и так далее, и носи), а с другой — «объясните, зачем вам, подождите 15 дней, покажите ваши социальные сети, и тогда мы, может быть, выпишем разрешение на покупку, но винтовку с магазином больше чем на 5 патронов или пистолетной рукоятью, или пистолет на 10, вы всё равно не купите».
Я склонен считать, что государственное вмешательство и регуляции интегрально делают хуже.
Во-первых, я говорил не про это, а про то, что работодатели впрягаются и без государственной палки.
Во-вторых, да, и?
В-третьих, этот перцентиль больше, чем вам кажется.
Ни одно из которых не работает, потому что у государства никогда не будет стимулов быть эффективным (исключая всякие сценарии из ненаучной фантастики типа ошейников со взрывчаткой на чиновниках).
Эта сумма была бы другой, но её покупательная способность была бы эквивалентной, поэтому на эту разницу (сводящуюся к курсу конвертации между сегодняшним тугриком и безналоговым тугриком) можно забить и считать всё в сегодняшних тугриках.
Почему эквивалентной? Потому, что если работодатель под меня выделяет 187 тысяч на ФОТ, значит, я ему приношу пользы на ≥187 тысяч. Есть, конечно, нерыночные инструменты влияния государства на рынок труда вроде ввода определённых квот, например, но ни под одну из этих квот я не попадаю, а проблемы бездельников меня не очень интересуют. И, кстати, если снизить число бездельников в штате, то количество свободных денег у работодателя повысится — снова мне профит!
В текущем рынке.
В безналоговом рынке у соседнего работодателя есть стимул меня переманить, предложив оплату чуть больше (потому что он может потратить часть этих 1000), и так далее итеративно до тех пор, пока моя зарплата не придёт к плюс-минус такому же балансу полезности для работодателя.
Как хорошо эти институты работают, я мог наблюдать всё своё время в Нью-Йорке, и особенно ярко — в 2020-м, когда менты вставали на колено и занимались прочей показухой, а агенство сдачи недвиги в доме, где я жил, и так наняло ЧОПовцев в районе начала июня, и так и продолжало их кормить до где-то сентября-октября, задолго после того, как я оттуда съехал.
Защита полиции — это миф. Полиция защищает не вас, а государственную систему.
Общего у моего вопроса и вашего ответа только слово в синтаксическом смысле «рассуждать». Даже семантика у него разная в этих случаях: я говорю о том, что «смотрю на кусок кода и пытаюсь понять, что он делает и чего он не делает», вы говорите о том, как бы сделать компиляцию всего проекта побыстрее, если он компилируется слишком долго.
А можете пояснить, как именно распараллелится код Мартина? Мне этот код тяжело читать (оптимизатору проще будет, конечно), но там, похоже, зависимость следующей итерации от результата предыдущей.
Под refinement types разные люди понимают разное, поэтому на него нет единого ответа, и вопрос вроде «какие ограничения подходят для системы типов», я бы сказал, даже не особо имеет смысла. Вопрос скорее в задачах.
В самом общем виде это типы вида
{ ν : T | P(ν) }, где P может быть достаточно произвольным (включая что-нибудь очевидно неразрешимое вида «ν-ая машина Тьюринга останавливается на входе ν»). Дальше в зависимости от твоих целей можно начинать ограничивать эти P. Хочешь лёгкость программирования, и чтобы машина всё сама решала, а ты о пруфтермах не думал? Ограничиваешься разрешимым подмножеством, или хотя бы тем, что какие-нибудь там SMT-солверы жрут в среднем нормально. Хочешь, чтобы язык был выразительным и позволял любые инварианты в типах? Разрешаешь весь term language там, но получаешь алгоритмическую неразрешимость proof finding'а и требование от машины ей помочь найти доказательства.Собсна, если я правильно помню соответствующий папир, классические liquid types из liquid haskell — это именно ограничение предикатов на SMT-разрешимое подмножество языка, и чтобы машина там всё сама доказывала (или конструктивно опровергала).
Я же в третьем пункте из предыдущего комментария пытался совместить удобоваримый для продакшен-программирования и SMT-разрешимый язык RT с полноценными завтипизированными DT, но уткнулся в отсутствие прямой симуляции refinement types зависимыми типами (что мешало даже сформулировать правильные теоремы о том, что трансляция RT → DT «имеет смысл» и «сохраняет операционную семантику»), потому что тогда не знал про разные возможности выражать термы как вычислительно неважные на уровне метатеории, но это совсем другая история.
Да, если это ограничение выражено в понятной для RT-тайпчекера форме (но лучше таки
a ≥ b).Угу.
Аналитическое взятие производных на шаблонах C++.
Физзбазз (серьёзно, физзбазз) на идрисе.
Незаконченная формализация исследовательской системы типов на агде.
В среднем ничего из этого не интересно, и уж тем более на это нет спроса.
Плохие парни де-факто могут обзавестись пистолетом с глушителем уже сейчас. Какая именно магическая пыль каких именно государственных феечек гарантирует безопасность законопослушного жителя сегодня (когда мы платим налоги) в таких ситуациях без людей вокруг и без полиции?
Напомню, что в Штатах (не)раскрываемость убийств — в районе 50%, а в отдельных местах, например, в городах Калифорнии (что дико зарегулированной по оружию, где глушитель или fully semiautomatic military-style mass-shooting-capacity magazine assault rifle хрен купишь легально, что имеющей одни из самых высоких налогов), самая низкая раскрываемость в 36%.
Кроме того, в Техасе, где оружие везде и для его получения и ношения даже лицензии не надо, существенно безопаснее, чем в Нью-Йорке (городе), где с ним как в худших локациях Калифорнии. Если бы у меня была девушка, я бы едва ли отпустил её гулять после заката солнца по Манхеттену (особенно по Централ Парку какому, хотя там людей порядком, или ездить по метро) или, тем более, Бронксу, а здесь, вне метрополий — да спокойно. В Централ Парке мне самому было несколько стрёмно, а здесь я спокойно могу гулять по безлюдным местам в 11 вечера (и именно потому, что за поясом у меня S&W, и проходящий мимо человек знает, что у меня оно может быть, и рисковать ради кредитной карточки… ну такое).
Я уж не говорю о том, что даже если бы arguendo вы были правы, то платить овер 100 тысяч в год за возможность погулять там, где никого нет… хз.
Текущее законодательство штрафует законопослушных людей и стоит на стороне преступников.
А какие достижения? Сокращение рабочего дня выбили не они, если что, а началось всё с Форда и ко, которые заметили, что люди так просто эффективнее (капиталисты клятые).
Я в США работаю, и работаю на компании, дающие сильно больше гибкости, свобод и ништяков, чем требуется (околонулевым по меркам других стран) трудовым законодательством (в чём тут завоевания социал-демократов?). И этот опыт сильно лучше опыта работы на европейцев.
Полиция никогда не будет защищать вас, потому что не вы конкретный ей платите деньги. От того, что она профукает вашу защиту, полиции ничего не будет. Поэтому у нас будут дела вроде Warren v. DC (прямо кодифицирующие, что полиция не обязана вас защищать), либо будет Увальде, когда несколько десятков ссыкунов, устроившихся в полицию только ради государственной пенсии и прочих ништяков, не будут ничего делать полтора часа и будут не давать родителям (вооружённым, ага) что-то сделать.
Основная цель полиции — создать иллюзию защищённости в среднем, чтобы у электората (опять же, в среднем) не было вопросов к государству. Что при этом происходит на самом деле, совершенно неважно, пока есть эта иллюзия.
Либо гендерное равенство, либо распространённо сидящие дома жёны. Определиться бы как-то.
А причём тут дети из соседнего комментария — непонятно. Они от одного заведения постоянной подружки не появляются.