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% доля времени. Говорят, есть варианты где-то между.
Я не знаю. Мне кажется, это костыль, который делается ради оптимизации в языках где не осилили stackful корутины.
Я подумал и решил, что ты прав, для языков с нормальными гринтредами раскраска на уровне языка не нужна, да.
Она нужна на уровне библиотек где-то настолько же (если не меньше), насколько нужно в типах выражать, скажем, «эта функция принадлежит слою с БД» — помогает рассуждать о коде, архитектурно полезно, но не критично. Даже «эта функция работает с [не]санитизированным пользовательским вводом» полезнее.
Ещё есть момент с сохранением инвариантов между await-точками, но мой опыт из чистых языков или stackless-корутин в плюсах на это не трансферится, а при попытке подумать про это из первых принципов ни доказать себе, что пофиг на async, ни построить контрпример, чтобы было не пофиг (но было пофиг в IO) я сходу не смог.
Но ведь он не говорит этим миру ничего нового.
На архитектурном уровне говорит, но без этого можно спокойно жить.
Ну и это тебе в хаскеле [почти] не говорит, где уже есть контроль эффектов в IO (и непокрытый им источник латентности — только медленные CPU-bound-функции). В языках, где вообще всё живёт в IO (и в задачах, где CPU-bound-частей по факту нет), таки говорит.
И когда я пишу критичный к перфу код на плюсах, мне бы хотелось, кстати, в типах аннотировать «выделяет память»/«бегает по указателям O(n) от входных данных»/etc. Асинк где-то там рядом.
При этом требует усилий, например, пройтись по стеку вызовов и там тоже в асинки покрасить.
Без какого-нибудь waitAsync : Async a → IO a грустно, да.
Есть, кстати, Cost-Aware Type Theory. Там, судя по абстракту, что-то такое описывается.
О, прикольно, я не встречал. Чё-т там люди хорошо так навернули. Закинул себе в список на чтение, спасибо.
То, что я встречал, было достаточно лайтовыми вариациями на тему, скажем, QTT с более сложной структурой, чем { 0, 1, ω }, для отслеживания сожранной ширины сети в квантовом circuit'е. CATT выглядит более точной системой, да.
Окей, так как вы по-прежнему отказываетесь предоставить своё определение, но здесь согласились, то я буду исходить из определения «концептуальное программирование — это когда есть архитектура и модель данных». Правда, по-прежнему непонятно, что такое «техническое программирование», как и непонятно ваше нежелание прояснять используемые вами термины, но это другая история.
Так вот, с учётом этого всё мной упомянутое в моём первом комментарии — вполне себе концептуальное программирование. Причём архитектуру, модель данных и так далее в том же HFT надо выбирать с существенно большим набором констрейнтов (по перфу, отсутствию багов и отчётности перед SEC, например), чем в упомянутом вами C++/WTL или 1C. В тайпчекерах — гляньте вот и скажите, сколько там техники, а сколько — концепций (я не автор, конечно, но в одном из проектов мы на подобных вещах прямо основывались).
Правда, вы там дальше пишете
Поэтому, для меня концептуальное программирование, когда я имею 100%-ную свободу выбора всего, но и отвечаю тоже, персонально, за результат.
а это совсем другая формулировка, и высшее образование тут точно ни при чём. Видимо, это опять упомянутое вами «и вашим, и нашим». Не знаю, что с этим делать. Для консистентной модели придётся проигнорировать.
Делать то могут все, а вот что получается в результате?
А в результате получается отсутствие корреляции между вузовским образованием и навыками по построению архитектуры. Не, серьёзно, я встречал жутких клоунов с гонором после MIT. Я встречал реально крутых людей, скиллам которых я завидую, которые в вуз и не пробовали поступать.
А последующая боль про 1С — это, ну, как бы это сказать помягче…
Мне уже доказывать как бы поздновато
Вообще это плохой знак, если что. Это не то, чем стоит гордиться.
Однако, как я уже писал, без МГУ, лично я бы, как программист, не состоялся.
Осталось понять, почему. Но дальше становится понятно, почему! Потому, что N десятков лет назад домашний компуктер не у каждого был-то, мягко скажем. Особенно такой, навыки программирования на котором легко обобщались бы на продакшен-системы.
То есть, вышка дала вам доступ к железу для прокачивания навыков. Это вполне валидная причина для программиста ≤80-х. Это валидная причина, не знаю, для врача сегодня (трупы на дом для препарирования и тренировки почему-то не продают). Это не валидная причина для программиста сегодня. Про неё можно писать мемуары (или комменты, как saipr, скажем), но её не надо обобщать на сегодняшних школьников, которые выросли с железкой в кармане и доступом в интернет (а растущие без этого на хабр не зайдут).
Более того, из вашей истории ясно, что формат образования у вас был куда ближе к самообразованию, чем к чему-то системному. Я совсем перестаю понимать, с чем вы спорите и за что топите, кроме как за смешивание «в мои годы с доступом к железу было туго» и «фундаменталка сформировала что-то там».
Если зеркалировать вашу логику на мою историю, то вполне можно сказать, что я бы не состоялся как программист без лазанья по помойкам: первую книжку по программированию я нашёл на свалке рядом с книжным магазином (иронично, что это была книжка по джаваскрипту), да и первую книжку по плюсам получил примерно аналогичным путём. Значит ли это, что старшеклассники, желающие стать программистами, должны тусить с бомжами и получать навык просеивания помоек?
Да, это так! «Здравый смысл, на базе фундаментального образования» реального работает, для меня.
Я бы не стал так радостно это подтверждать, потому что дальше же я пишу, что это нефальсифицируемый тезис и, более того, вы не даёте никакой дополнительной информации, чтобы оценить вероятностное пространство ваших возможных траекторий в окрестности этого здравого смысла.
Автор статьи предлагает свои «советы постороннего», я свои
Я рад, что вы хотя бы в такой форме признали, что даёте советы, а не просто «делитесь впечатлениями о своём опыте». Это самое главное.
Дальше не самое главное:
У нас даже классиков не считают, особо, за авторитеты
От человека с двумя высшими (включая мехмат МГУ) можно было бы ожидать понимания, что дело не в авторитетах, а в содержании высказываний.
Печально, что вы так воспринимаете!
Процитированные мной вещи вроде «Учитесь про запас» — это не просто «вы так воспринимаете». Давайте без этого приёма здесь, пожалуйста.
Все, понемногу, и правы и не правы. Для меня, естественно, воспринимать Мир через призму: «И нашим и вашим!». Это закон жизни, независимо от того, нравится он нам или нет.
Ergo «все претензии по существу к моим комментариям — мелочи и придирки к частностям, и их можно игнорировать». Давайте и без этого тоже.
Тем более, что нет такого закона.
Лучше расскажите про свои взгляды на процесс разработки программ, успехи и неудачи, всяко интересней будет, чем придираться к частностям.
У меня нет универсальных взглядов «в общем». Но если очень хотите что-нибудь о процессах, то можете почитать отличную книгу Algebra-driven design.
Тот комментарий написан 2 месяца назад с глаголами в настоящем времени — «Полностью поддерживаю», «Не рекомендую». При чём здесь «Тогда мне казалось норм, а сейчас вижу, что не норм»?
Исходное процитированное мной утверждение в том комментарии было очевидно саркастичным, и я продолжал эту линию сарказма в контексте исходного обсуждения (что там за контекст был? что-то на уровне «всё ради учёбы!», да?). Временное химическое отрезание писюнов, конечно, лайтовее постоянного физического, но всё равно не является общепринятой (или даже хотя бы морально допустимой) нормой поведения, поэтому в моей модели читатель подумает «ппц упорыш, нафиг так жить, сессии того не стоят», что в итоге усилит его мнение о том, что всё ради учёбы — плохая идея.
Плюс, конечно, нельзя отрицать мой биас в сторону «вы хотите поговорить об этом».
Но я скорректирую свою модель, спасибо.
И поддерживаются тоже сами, с нулевым количеством затрачиваемой энергии
Воспринимаемо — да.
Эта энергия была на уровне как мне сейчас пойти почитать книжку с утра перед работой или погонять в командный шутан. Книжки бывают сложные, требующие поддержания большого контекста и интеграции с имеющимися знаниями, а также поддержания внимательности и придирок к каждому тезису, а в шутане бывают раунды на пару часов, где геймплей подразумевает что необходимость кооперации, продумывания тактики наперёд и так далее, что включение мозгов «локально» на уровне «учесть дистанцию, разность высот и конечную скорость пули при выстреле», и все эти занятия требуют энергию в формальном физическом смысле, но ты не воспринимаешь их как затраты.
Если формализовывать, то я бы говорил о дельте энергии между «до» и «после» сходки (книжки, сессии за игрой).
и при отсутствии конкуренции.
Я ж говорю: в том контексте ты не думаешь о будущем, а живёшь сейчас. Это вы говорите как вы сегодняшняя, с вашим сегодняшним опытом, точно так же как я сегодняшний тоже думаю в терминах каких-то там конкуренций, альтернативных издержек, жизненных целей, sunk costs, долговременных стратегий, энергий и их дельт, и так далее. Но тогда я так не думал. Это всё существовало и было доступно как какие-то абстрактные концепты, но не было частью ежедневного эмоционального словаря.
Поэтому, короче, тебя в 17-20 лет это не парит. Но, может, у вас наивность и беззаботность раньше кончилась, хз.
Во-первых, я, возможно, написал неаккуратно: речь, конечно, не только непосредственно о 17 годах, а о всём промежутке в этак 16-20 лет (с последующим плавным спаданием до 23-25).
Во-вторых, не ожидал, что тред станет настолько биографичным, ну да ладно, ожидать этого стоило.
У меня было некоторое окно в этак 5-6 месяцев между ранней весной 11-го класса (когда стало понятно, что я поступил по олимпиадам, и поступательное давление резко спало, но как раз в 11-м классе я и упарывал Фезам, и слез с него как раз где-то с окончанием олимпиад) и сентябрём в начале 1-го курса. В это окно мне удалось заглянуть и понять, как живут нормальные люди: ну там, съездил отметить сдачу сессии приятеля (тоже физтех, но социальный, и потом вылетел) на год старше, съездил отметить днюху другого приятеля (на пару лет старше, познакомились ещё в физмат-школе). Этого хватило, чтобы засэмплить, как работают социальные графы и прочее описанное мной здесь, даже если я этим пользовался сильно не целиком.
А потом эти графы стали распадаться и стремиться к нулю, сначала медленно, а потом всё быстрее. Да, к концу первого курса их ещё хватало, чтобы с кем-то случайно познакомиться (и чуть не завалить сесссию, где под «чуть» понимается «сдал линал на три, а главный препод по линалу был факер, и на пересдачу идти было стрёмно») — в конце концов, первый семак самый халявный, да и я тогда позволял себе не работать, но к концу этак второго граф уже сдулся, отношения тоже сдулись, а я сделал вывод, что надо себе что-нибудь выключить.
Ну и, конечно, в моменте всё это воспринималось как правильное решение, поэтому ботал я действительно счастливо и эффективно. А сейчас, если смотреть назад на всю историю в целом, то, конечно, уже не так счастливо и эффективно.
Главное, не пытаться, принудительно, «осчастливить» других. Поэтому, просто делимся впечатлениями о своем жизненном опыте и делаем, про себя, выводы, какие считаем нужными.
Сорян, но нет. Когда вы комментируете пост с рекомендациями другим людям, начинаете свой комментарий с
Ребята, не ведитесь! Послушайте, лучше «старого волка».
, внутри комментария регулярно говорите вещи вроде
Имея хорошие знания, вы не пропадете. Учитесь про запас, ибо никогда не знаешь, что именно будет востребовано.
, а также даёте советы вроде как себе (но на самом деле аудитории)
Что бы я посоветовал самому себе, если бы я, сейчас, учился бы в школе, либо поступал бы в ВУЗ?
, и когда в других комментариях вы пишете, скажем,
техническому исполнителю взять неоткуда, не имея хорошего образования за плечами
, то это именно что рассказы другим, что им надо делать, чтобы прийти к успеху. Это настолько близко к принудительному осчастливливанию, насколько комментарии в интернете к нему вообще могут быть близки, и весьма далеко от «просто делимся впечатлениями и делаем выводы про себя».
Через весь ваш комментарий лейтмотивом идёт противопоставление «технического» и «концептуального» программирования. Чтобы я мог предметно ответить, можете как-то более-менее сформулировать (даже не обязательно на уровне строгости мехмата МГУ), что конкретно вы имеете в виду? Желательно не через одни лишь примеры, а то там уже есть один, и он… странный, а через какое-то определение, которым можно было бы оперировать в логических построениях. И, учитывая ваши проекты, которые вы обычно упоминаете в других комментариях, или запомнившийся мне комментарий от вас под статьёй о теоркате в духе «а как теоркат поможет проектировать UI-то?», мне это особенно интересно.
А пока что наиболее вероятная гипотеза ваших определений — что под «концепцией» вы понимаете выбор архитектуры, модели данных и так далее, что в индустрии делают все уровнем чуть выше джуна, и для чего высшее образование не нужно (эмпирически наблюдаемый факт). И, более того, то, о чём я писал — игры с архитектурой и поддерживаемостью в личных пет-проектах, тот же Александреску, да тот же Саттер — это даёт все те же навыки (и больше), о которых вы говорите.
Теперь по частностям.
И потом, говорить, что ВУЗ не нужен, человеку, который закончил ВУЗ, это не вполне логично.
Ну это стандартная уловка-22: если ты окончил вуз, то говорить, что он не нужен, нелогично. Не окончил — тем более, ведь ты просто не знаешь, что упускаешь.
Мне вот не нужны, иностранные языки, которые я учу сейчас, но я это делаю не ради абстрактной нужности, а ради собственного развития, в чем именно вижу и смысл и пользу.
Но вы при этом не говорите, что программистам нужны иностранные языки, так что никаких вопросов. И, кстати, обычно наоборот: нужность конкретная, а вот развитие скорее более неизмеримое и абстрактное.
Можно привести аналогию. «Писать код», это как писать дневник. Типа, сегодня было то, а вчера – сё. Манька сказала «А», а Ванька – «Б». По принципу чукчи: «Что вижу, то и пою».
Очень strawman'истая аналогия, которая не мапится на реальность.
Смог бы ли я их делать без двух ВУЗов? Не уверен! Без МГУ, я бы, как программист, не состоялся бы. Пока, для меня, самым эффективным методом оказался «метод здравого смысла», на базе фундаментального образования.
Это неверный фрейминг и, более того, неверный подход к анализу (что не вполне логично от окончившего мехмат МГУ). Вы рассматриваете альтернативную гипотезу, где вы выкинули ваше образование, но не заменили его ничем — ни пет-проектами в то же время, ни реальной продакшен-работой, ничем подобным. Альтернативные издержки работают не так. И я не сомневаюсь, что если выбирать между «6 лет вуза» и «6 лет лежать на печи», то первое будет лучше. Но обсуждаемый выбор слегка другой.
И ещё один вопрос: почему вы в этом уверены? Почему вы считаете, что без вышки бы вы не состоялись?
Вы же сами пишете, что ничего конкретного не использовалось, математика забыта, всё такое. Остаётся только некий «здравый смысл», который был воспитан в вашей модели именно вузом (и не мог быть воспитан никак иначе). Упрощая, это нефальсфицируемый тезис. Точно так же, как не очень фальсифицируемым тезисом является что-то в духе «армия сделала из меня мужика и воспитала меня, все мои успехи благодаря армии» (что я на самом деле слышал от других людей в слегка других стратах).
хоть с рекомендуемыми вами книгами, хоть без них
Для протокола, я не рекомендовал здесь ни одной книги и не собираюсь этого делать, потому что все мои рекомендации условны по «а что именно вы хотите достичь?», и для разных целей я буду рекомендовать сильно разное.
В итоге, вы игнорируете мои советы, а я – ваши.
Нет, здесь нет симметрии, потому что я на ваши тезисы отвечаю весьма подробно (а не просто их игнорирую) и пытаюсь докопаться до вашей модели мира и того, как вы обобщаете вашу модель.
У меня всего полтора высших, не два: оконченный ФУПМ МФТИ и незаконченная аспирантура на ВЦ РАН по 01.01.09.
Что я могу сказать, по итогу. Я не учился на профессионального программиста, но, де факто, стал им. Очень помогло, конечно, фундаментальное образование, и, хотя, я профессионально, математикой не занимался, но, она помогала мне выживать в трудные времена, которых было не мало.
Что могу сказать по итогу я, раз мы тут делимся личным опытом и его обобщаем?
Вуз для работы (особенно в упоминаемом выше 1C, C++/WTL и так далее) не нужен подавляющему большинству программистов для подавляющего большинства задач. На самом деле вуз не необходим (и не достаточен) даже в тех вещах, которыми занимался я — от прикладного, продуктового машинного обучения до HFT на плюсах, тайпчекеров на хаскеле и формальных методов на агде/коке. Даже там за глаза было достаточно сильной физмат-школы (которая у меня тоже была), и программа которой в вузовском ритме осваивается за полгода, если не за месяц. Либо (в случае формальных методов) было недостаточно вуза, потому что теорию типов на этом «фундаментальном образовании» не дают. И матлог за пределами семестра, по факту, исчисления высказываний не дают.
Вуз уровня МФТИ (и даже, может, МГУ, МИФИ и Бауманки) для программиста — это трата времени студента, это трата бюджетного места, это трата времени лекторов и семинаристов. В подавляющем большинстве задач у подавляющего большинства программистов не нужны уравнения в частных производных, функан, и прочие подобные методы. Не нужен даже условный линал за пределами шпаргалки на одну страницу.
Вуз нужен для человека, который потом свяжет свою жизнь с ресёрчем. Это не случай подавляющего большинства программистов. Как понять, ваш ли это случай? Зажмуриться и представить две картинки:
вы пишете код и деплоите в прод, ходите на митапы по языку X и стеку Y, по вечерам читаете посты в блогах о новом языке Z и либе W.
вы пишете статьи и сабмитите в arxiv, ходите на конференции с какими-то закорючками на слайдах, по вечерам читаете чужие статьи с arxiv.
Что из этого больше привлекает? Что из этого больше привлекает потому, что это ваше (и что вы готовы делать уже сейчас), а не потому, что папка с мамкой сказали, что наука — эта крута, или потому что у учёных такой вот ореол полубожественности, или, для симметрии, потому что программистам дофига платят?
Что нужно для программиста? Писать код. Просто писать код. Обсуждать код с другими людьми. Находить реальные продуктовые подработки. Писать код у меня получалось до вуза. Прочитать Саттера и Александреску у меня получалось до вуза. Находить людей, которые критиковали мой код и давали дельные советы, у меня получалось до вуза, даже в ранних и средних нулевых, когда в интернете было меньше людей.
И главное — долго писать код. Поддерживать свой пет-проект годовой/трёхлетней/пятилетней давности и смотреть, что работает хорошо, а что — превратилось в нечитаемое неподдерживаемое месиво, и делать выводы на практике о том, что такое — поддерживаемый код. Развлекаться с языком, писать всякую ерунду на темплейтах в плюсах или абьюзить систему типов в хаскеле или натравливать vtune на свой код просто потому, что интересно, и прокачивать там свои скиллы. И по итогу предлагают хорошие деньги мне именно за то, что я умею писать всякую ерунду на плюсах и делать её быстрой, и потому, что я на личном опыте знаю, что — поддерживаемо.
А тезис «математика помогает» вообще ничем не отличается от тезиса, не знаю, «вера помогает», ведь «в трудные времена я думал о Боге, и Писание помогло мне их преодолеть». Хотя чего это я, даже это — более конкретное утверждение, чем «математика мне помогла в трудные времена». Как помогла? Чем? Обязательно ли для этой математики было оканчивать МГУ? Непонятно.
Что бы я посоветовал самому себе, если бы я, сейчас, учился бы в школе, либо поступал бы в ВУЗ? Прежде всего, учиться! Учеба должна стать смыслом жизни! Как говорил «Дедушка» Ленин: «Учиться, учиться и еще раз учиться!» «Настоящим образом!».
Я бы посоветовал не слушать всех тех, кто говорит, что без фундаментального образования никуда (ещё как куда). Посоветовал бы учиться в личное время на личных проектах, и не тратить своё и чужое время на вуз.
Потому что с окончания вуза прошло уже 10+ лет, и можно было бы ожидать какой-то отдачи от него, наконец, а её нет (и я теперь понимаю, что и не будет). А затраты и ненулевые альтернативные издержки — есть.
Вплоть, до: «Не хочу жениться, а хочу учиться!».
Про это в таких тредах редко говорят, поэтому я позволю себе сфокусироваться на этом отдельно.
Жениться в 17 действительно несколько рановато, а вот социального контекста, который настолько легко позволяет отношения, не отягощённые мыслями о тикающих часиках, будущем-вместе-или-нет через 10 лет, и так далее, и где вы встречаетесь с кем-то ради вас здесь и сейчас, больше не будет никогда. А если вы немного интроверт, то больше никогда не будет и богатого социального графа сверстников, через которых можно естественно оказываться в одной компании с большим количеством представительниц противоположного пола, имеющих похожий с вами социальный уровень, уровень самоосознания, и так далее, и где знакомства происходят сами, с нулевым количеством затраченной энергии.
Но можно, конечно, всё это променять на урматы.
Имея хорошие знания, вы не пропадете. Учитесь про запас, ибо никогда не знаешь, что именно будет востребовано.
Всё ещё жду, когда мне пригодятся урматы.
Ну и да, условия позднего СССР/ранней РФ и современного мира — это, тащем, два разных мира. Сегодня входным билетом куда лучше работает гитхаб и блог, а когда я диплом последний раз показывал — и не помню. По-моему, его у меня уже даже в резюме нет.
И да,
Читайте книжки, которые мне нравятся
Лучше спокойно прочитать Таненбаума или «Computer Systems: A Programmers Perspective», чем выдрочить себе интроектированным элитизмом мозг до того, что от чтения любых книг, где нет хотя бы одной теоремы с доказательством, ты ощущаешь стыд, потому что мог бы в это время читать что-нибудь про higher topos theory, например.
А свобода слова не означает свободно говорить неприятные для фирм вещи и гадящие стране факты. А свобода совести не означает свободно придерживаться аморальных ценностей и иметь гадящее стране мировоззрение.
Нет, братиш, запутался тут ты, сорян. То, что ты называешь свободой — это не свобода, а тоталитарный загончик, который, как ты почему-то думаешь, обязательно окажется меховой частью в твою сторону.
Проблема в том, что настоящая свобода (а не этот новояз, который ты и такие, как ты, пытаются притащить в дискурс) требует осознания личной ответственности за свою жизнь, а это тяжёлое, сложное осознание.
Нет смысла рассматривать существование «вообще». С подвешенным в вакууме термом x (одиноко стоящая переменная) ничего нельзя сделать, он неинтересен сам по себе.
а не один из трех - только внутри функции.
Формализация этих правил (с системами типов, отношением типизации, и так далее) раздует статью куда сильнее, и, ИМХО, оно того заслуживать не будет.
И что значит Variable(Int)?
ХЗ, в данной кодировке оно напрямую не нужно. Может, автору потом пригодится для его дальнейших замыслов, не знаю, я ж не автор. Пока оно ему нужно, только чтоб красиво печатать λ-термы.
А ML-семейством я не занимался. Может, поэтому и нет его вдохновения.)
Далее, выше сказано, что "функция от переменной", а тут она от терма. Почему несоответствие?
Потому что это на самом деле одно и то же.
Переменная — это то, что видит тело функции. Вы пишете λx. x + 2, и вот эта вот штука справа от точки (то есть, тело функции) видит только переменную x.
Когда вы вызываете эту функцию, то передаёте вы ей полноценный терм, который подставляется на место этой переменной. Просто в данном случае за подстановку отвечает метаязык (мета- — потому, что это язык, на котором описывается язык), и в нём такие функции имеют тип Term → Term.
Ничего непонятно.
ХЗ, я gleam не знаю, но это достаточно распространённый синтаксис в языках, черпающих вдохновение в ML-семействе. При очень беглом взгляде я вообще подумал, что это раст (которого, впрочем, я тоже не знаю).
Не, так не честно, это не настоящая бета-редукция, читерство какое-то.
Не читерство, а higher-order abstract syntax (потом можно обобщить до P(olymorphic)HOAS).
Охренительно удобная штука, на самом деле. Вам бесплатно (из метаязыка) даётся весь набор инструментов для работы с именами и байндингами, и, как следствие, отсутствие геморроя с представлением переменных (символы? de Bruijn? locally nameless? да это всё не нужно, фигачь на метаязыке!), бесплатная α-эквивалентность, процедура подстановки (это просто применение в метаязыке), и, если метаязык достаточно мощный (ну там, coq/agda/etc), то доказательства свойств вашего языка становятся сильно проще.
Плюс движок для работы с 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% доля времени. Говорят, есть варианты где-то между.
Я подумал и решил, что ты прав, для языков с нормальными гринтредами раскраска на уровне языка не нужна, да.
Она нужна на уровне библиотек где-то настолько же (если не меньше), насколько нужно в типах выражать, скажем, «эта функция принадлежит слою с БД» — помогает рассуждать о коде, архитектурно полезно, но не критично. Даже «эта функция работает с [не]санитизированным пользовательским вводом» полезнее.
Ещё есть момент с сохранением инвариантов между await-точками, но мой опыт из чистых языков или stackless-корутин в плюсах на это не трансферится, а при попытке подумать про это из первых принципов ни доказать себе, что пофиг на
async, ни построить контрпример, чтобы было не пофиг (но было пофиг вIO) я сходу не смог.На архитектурном уровне говорит, но без этого можно спокойно жить.
Ну и это тебе в хаскеле [почти] не говорит, где уже есть контроль эффектов в
IO(и непокрытый им источник латентности — только медленные CPU-bound-функции). В языках, где вообще всё живёт вIO(и в задачах, где CPU-bound-частей по факту нет), таки говорит.И когда я пишу критичный к перфу код на плюсах, мне бы хотелось, кстати, в типах аннотировать «выделяет память»/«бегает по указателям O(n) от входных данных»/etc. Асинк где-то там рядом.
Без какого-нибудь
waitAsync : Async a → IO aгрустно, да.О, прикольно, я не встречал. Чё-т там люди хорошо так навернули. Закинул себе в список на чтение, спасибо.
То, что я встречал, было достаточно лайтовыми вариациями на тему, скажем, QTT с более сложной структурой, чем { 0, 1, ω }, для отслеживания сожранной ширины сети в квантовом circuit'е. CATT выглядит более точной системой, да.
Окей, так как вы по-прежнему отказываетесь предоставить своё определение, но здесь согласились, то я буду исходить из определения «концептуальное программирование — это когда есть архитектура и модель данных». Правда, по-прежнему непонятно, что такое «техническое программирование», как и непонятно ваше нежелание прояснять используемые вами термины, но это другая история.
Так вот, с учётом этого всё мной упомянутое в моём первом комментарии — вполне себе концептуальное программирование. Причём архитектуру, модель данных и так далее в том же HFT надо выбирать с существенно большим набором констрейнтов (по перфу, отсутствию багов и отчётности перед SEC, например), чем в упомянутом вами C++/WTL или 1C. В тайпчекерах — гляньте вот и скажите, сколько там техники, а сколько — концепций (я не автор, конечно, но в одном из проектов мы на подобных вещах прямо основывались).
Правда, вы там дальше пишете
а это совсем другая формулировка, и высшее образование тут точно ни при чём. Видимо, это опять упомянутое вами «и вашим, и нашим». Не знаю, что с этим делать. Для консистентной модели придётся проигнорировать.
А в результате получается отсутствие корреляции между вузовским образованием и навыками по построению архитектуры. Не, серьёзно, я встречал жутких клоунов с гонором после MIT. Я встречал реально крутых людей, скиллам которых я завидую, которые в вуз и не пробовали поступать.
А последующая боль про 1С — это, ну, как бы это сказать помягче…
Вообще это плохой знак, если что. Это не то, чем стоит гордиться.
Осталось понять, почему. Но дальше становится понятно, почему! Потому, что N десятков лет назад домашний компуктер не у каждого был-то, мягко скажем. Особенно такой, навыки программирования на котором легко обобщались бы на продакшен-системы.
То есть, вышка дала вам доступ к железу для прокачивания навыков. Это вполне валидная причина для программиста ≤80-х. Это валидная причина, не знаю, для врача сегодня (трупы на дом для препарирования и тренировки почему-то не продают). Это не валидная причина для программиста сегодня. Про неё можно писать мемуары (или комменты, как saipr, скажем), но её не надо обобщать на сегодняшних школьников, которые выросли с железкой в кармане и доступом в интернет (а растущие без этого на хабр не зайдут).
Более того, из вашей истории ясно, что формат образования у вас был куда ближе к самообразованию, чем к чему-то системному. Я совсем перестаю понимать, с чем вы спорите и за что топите, кроме как за смешивание «в мои годы с доступом к железу было туго» и «фундаменталка сформировала что-то там».
Если зеркалировать вашу логику на мою историю, то вполне можно сказать, что я бы не состоялся как программист без лазанья по помойкам: первую книжку по программированию я нашёл на свалке рядом с книжным магазином (иронично, что это была книжка по джаваскрипту), да и первую книжку по плюсам получил примерно аналогичным путём. Значит ли это, что старшеклассники, желающие стать программистами, должны тусить с бомжами и получать навык просеивания помоек?
Я бы не стал так радостно это подтверждать, потому что дальше же я пишу, что это нефальсифицируемый тезис и, более того, вы не даёте никакой дополнительной информации, чтобы оценить вероятностное пространство ваших возможных траекторий в окрестности этого здравого смысла.
Я рад, что вы хотя бы в такой форме признали, что даёте советы, а не просто «делитесь впечатлениями о своём опыте». Это самое главное.
Дальше не самое главное:
От человека с двумя высшими (включая мехмат МГУ) можно было бы ожидать понимания, что дело не в авторитетах, а в содержании высказываний.
Процитированные мной вещи вроде «Учитесь про запас» — это не просто «вы так воспринимаете». Давайте без этого приёма здесь, пожалуйста.
Ergo «все претензии по существу к моим комментариям — мелочи и придирки к частностям, и их можно игнорировать». Давайте и без этого тоже.
Тем более, что нет такого закона.
У меня нет универсальных взглядов «в общем». Но если очень хотите что-нибудь о процессах, то можете почитать отличную книгу Algebra-driven design.
Исходное процитированное мной утверждение в том комментарии было очевидно саркастичным, и я продолжал эту линию сарказма в контексте исходного обсуждения (что там за контекст был? что-то на уровне «всё ради учёбы!», да?). Временное химическое отрезание писюнов, конечно, лайтовее постоянного физического, но всё равно не является общепринятой (или даже хотя бы морально допустимой) нормой поведения, поэтому в моей модели читатель подумает «ппц упорыш, нафиг так жить, сессии того не стоят», что в итоге усилит его мнение о том, что всё ради учёбы — плохая идея.
Плюс, конечно, нельзя отрицать мой биас в сторону «вы хотите поговорить об этом».
Но я скорректирую свою модель, спасибо.
Воспринимаемо — да.
Эта энергия была на уровне как мне сейчас пойти почитать книжку с утра перед работой или погонять в командный шутан. Книжки бывают сложные, требующие поддержания большого контекста и интеграции с имеющимися знаниями, а также поддержания внимательности и придирок к каждому тезису, а в шутане бывают раунды на пару часов, где геймплей подразумевает что необходимость кооперации, продумывания тактики наперёд и так далее, что включение мозгов «локально» на уровне «учесть дистанцию, разность высот и конечную скорость пули при выстреле», и все эти занятия требуют энергию в формальном физическом смысле, но ты не воспринимаешь их как затраты.
Если формализовывать, то я бы говорил о дельте энергии между «до» и «после» сходки (книжки, сессии за игрой).
Я ж говорю: в том контексте ты не думаешь о будущем, а живёшь сейчас. Это вы говорите как вы сегодняшняя, с вашим сегодняшним опытом, точно так же как я сегодняшний тоже думаю в терминах каких-то там конкуренций, альтернативных издержек, жизненных целей, sunk costs, долговременных стратегий, энергий и их дельт, и так далее. Но тогда я так не думал. Это всё существовало и было доступно как какие-то абстрактные концепты, но не было частью ежедневного эмоционального словаря.
Поэтому, короче, тебя в 17-20 лет это не парит. Но, может, у вас наивность и беззаботность раньше кончилась, хз.
Во-первых, я, возможно, написал неаккуратно: речь, конечно, не только непосредственно о 17 годах, а о всём промежутке в этак 16-20 лет (с последующим плавным спаданием до 23-25).
Во-вторых, не ожидал, что тред станет настолько биографичным, ну да ладно, ожидать этого стоило.
У меня было некоторое окно в этак 5-6 месяцев между ранней весной 11-го класса (когда стало понятно, что я поступил по олимпиадам, и поступательное давление резко спало, но как раз в 11-м классе я и упарывал Фезам, и слез с него как раз где-то с окончанием олимпиад) и сентябрём в начале 1-го курса. В это окно мне удалось заглянуть и понять, как живут нормальные люди: ну там, съездил отметить сдачу сессии приятеля (тоже физтех, но социальный, и потом вылетел) на год старше, съездил отметить днюху другого приятеля (на пару лет старше, познакомились ещё в физмат-школе). Этого хватило, чтобы засэмплить, как работают социальные графы и прочее описанное мной здесь, даже если я этим пользовался сильно не целиком.
А потом эти графы стали распадаться и стремиться к нулю, сначала медленно, а потом всё быстрее. Да, к концу первого курса их ещё хватало, чтобы с кем-то случайно познакомиться (и чуть не завалить сесссию, где под «чуть» понимается «сдал линал на три, а главный препод по линалу был факер, и на пересдачу идти было стрёмно») — в конце концов, первый семак самый халявный, да и я тогда позволял себе не работать, но к концу этак второго граф уже сдулся, отношения тоже сдулись, а я сделал вывод, что надо себе что-нибудь выключить.
Ну и, конечно, в моменте всё это воспринималось как правильное решение, поэтому ботал я действительно счастливо и эффективно. А сейчас, если смотреть назад на всю историю в целом, то, конечно, уже не так счастливо и эффективно.
Поэтому здесь как раз всё консистентно, ИМХО.
Сорян, но нет. Когда вы комментируете пост с рекомендациями другим людям, начинаете свой комментарий с
, внутри комментария регулярно говорите вещи вроде
, а также даёте советы вроде как себе (но на самом деле аудитории)
, и когда в других комментариях вы пишете, скажем,
, то это именно что рассказы другим, что им надо делать, чтобы прийти к успеху. Это настолько близко к принудительному осчастливливанию, насколько комментарии в интернете к нему вообще могут быть близки, и весьма далеко от «просто делимся впечатлениями и делаем выводы про себя».
Через весь ваш комментарий лейтмотивом идёт противопоставление «технического» и «концептуального» программирования. Чтобы я мог предметно ответить, можете как-то более-менее сформулировать (даже не обязательно на уровне строгости мехмата МГУ), что конкретно вы имеете в виду? Желательно не через одни лишь примеры, а то там уже есть один, и он… странный, а через какое-то определение, которым можно было бы оперировать в логических построениях. И, учитывая ваши проекты, которые вы обычно упоминаете в других комментариях, или запомнившийся мне комментарий от вас под статьёй о теоркате в духе «а как теоркат поможет проектировать UI-то?», мне это особенно интересно.
А пока что наиболее вероятная гипотеза ваших определений — что под «концепцией» вы понимаете выбор архитектуры, модели данных и так далее, что в индустрии делают все уровнем чуть выше джуна, и для чего высшее образование не нужно (эмпирически наблюдаемый факт). И, более того, то, о чём я писал — игры с архитектурой и поддерживаемостью в личных пет-проектах, тот же Александреску, да тот же Саттер — это даёт все те же навыки (и больше), о которых вы говорите.
Теперь по частностям.
Ну это стандартная уловка-22: если ты окончил вуз, то говорить, что он не нужен, нелогично. Не окончил — тем более, ведь ты просто не знаешь, что упускаешь.
Но вы при этом не говорите, что программистам нужны иностранные языки, так что никаких вопросов. И, кстати, обычно наоборот: нужность конкретная, а вот развитие скорее более неизмеримое и абстрактное.
Очень strawman'истая аналогия, которая не мапится на реальность.
Это неверный фрейминг и, более того, неверный подход к анализу (что не вполне логично от окончившего мехмат МГУ). Вы рассматриваете альтернативную гипотезу, где вы выкинули ваше образование, но не заменили его ничем — ни пет-проектами в то же время, ни реальной продакшен-работой, ничем подобным. Альтернативные издержки работают не так. И я не сомневаюсь, что если выбирать между «6 лет вуза» и «6 лет лежать на печи», то первое будет лучше. Но обсуждаемый выбор слегка другой.
И ещё один вопрос: почему вы в этом уверены? Почему вы считаете, что без вышки бы вы не состоялись?
Вы же сами пишете, что ничего конкретного не использовалось, математика забыта, всё такое. Остаётся только некий «здравый смысл», который был воспитан в вашей модели именно вузом (и не мог быть воспитан никак иначе). Упрощая, это нефальсфицируемый тезис. Точно так же, как не очень фальсифицируемым тезисом является что-то в духе «армия сделала из меня мужика и воспитала меня, все мои успехи благодаря армии» (что я на самом деле слышал от других людей в слегка других стратах).
Для протокола, я не рекомендовал здесь ни одной книги и не собираюсь этого делать, потому что все мои рекомендации условны по «а что именно вы хотите достичь?», и для разных целей я буду рекомендовать сильно разное.
Нет, здесь нет симметрии, потому что я на ваши тезисы отвечаю весьма подробно (а не просто их игнорирую) и пытаюсь докопаться до вашей модели мира и того, как вы обобщаете вашу модель.
У меня всего полтора высших, не два: оконченный ФУПМ МФТИ и незаконченная аспирантура на ВЦ РАН по 01.01.09.
Что могу сказать по итогу я, раз мы тут делимся личным опытом и его обобщаем?
Вуз для работы (особенно в упоминаемом выше 1C, C++/WTL и так далее) не нужен подавляющему большинству программистов для подавляющего большинства задач. На самом деле вуз не необходим (и не достаточен) даже в тех вещах, которыми занимался я — от прикладного, продуктового машинного обучения до HFT на плюсах, тайпчекеров на хаскеле и формальных методов на агде/коке. Даже там за глаза было достаточно сильной физмат-школы (которая у меня тоже была), и программа которой в вузовском ритме осваивается за полгода, если не за месяц. Либо (в случае формальных методов) было недостаточно вуза, потому что теорию типов на этом «фундаментальном образовании» не дают. И матлог за пределами семестра, по факту, исчисления высказываний не дают.
Вуз уровня МФТИ (и даже, может, МГУ, МИФИ и Бауманки) для программиста — это трата времени студента, это трата бюджетного места, это трата времени лекторов и семинаристов. В подавляющем большинстве задач у подавляющего большинства программистов не нужны уравнения в частных производных, функан, и прочие подобные методы. Не нужен даже условный линал за пределами шпаргалки на одну страницу.
Вуз нужен для человека, который потом свяжет свою жизнь с ресёрчем. Это не случай подавляющего большинства программистов. Как понять, ваш ли это случай? Зажмуриться и представить две картинки:
вы пишете код и деплоите в прод, ходите на митапы по языку X и стеку Y, по вечерам читаете посты в блогах о новом языке Z и либе W.
вы пишете статьи и сабмитите в arxiv, ходите на конференции с какими-то закорючками на слайдах, по вечерам читаете чужие статьи с arxiv.
Что из этого больше привлекает? Что из этого больше привлекает потому, что это ваше (и что вы готовы делать уже сейчас), а не потому, что папка с мамкой сказали, что наука — эта крута, или потому что у учёных такой вот ореол полубожественности, или, для симметрии, потому что программистам дофига платят?
Что нужно для программиста? Писать код. Просто писать код. Обсуждать код с другими людьми. Находить реальные продуктовые подработки. Писать код у меня получалось до вуза. Прочитать Саттера и Александреску у меня получалось до вуза. Находить людей, которые критиковали мой код и давали дельные советы, у меня получалось до вуза, даже в ранних и средних нулевых, когда в интернете было меньше людей.
И главное — долго писать код. Поддерживать свой пет-проект годовой/трёхлетней/пятилетней давности и смотреть, что работает хорошо, а что — превратилось в нечитаемое неподдерживаемое месиво, и делать выводы на практике о том, что такое — поддерживаемый код. Развлекаться с языком, писать всякую ерунду на темплейтах в плюсах или абьюзить систему типов в хаскеле или натравливать vtune на свой код просто потому, что интересно, и прокачивать там свои скиллы. И по итогу предлагают хорошие деньги мне именно за то, что я умею писать всякую ерунду на плюсах и делать её быстрой, и потому, что я на личном опыте знаю, что — поддерживаемо.
А тезис «математика помогает» вообще ничем не отличается от тезиса, не знаю, «вера помогает», ведь «в трудные времена я думал о Боге, и Писание помогло мне их преодолеть». Хотя чего это я, даже это — более конкретное утверждение, чем «математика мне помогла в трудные времена». Как помогла? Чем? Обязательно ли для этой математики было оканчивать МГУ? Непонятно.
Я бы посоветовал не слушать всех тех, кто говорит, что без фундаментального образования никуда (ещё как куда). Посоветовал бы учиться в личное время на личных проектах, и не тратить своё и чужое время на вуз.
Потому что с окончания вуза прошло уже 10+ лет, и можно было бы ожидать какой-то отдачи от него, наконец, а её нет (и я теперь понимаю, что и не будет). А затраты и ненулевые альтернативные издержки — есть.
Про это в таких тредах редко говорят, поэтому я позволю себе сфокусироваться на этом отдельно.
Жениться в 17 действительно несколько рановато, а вот социального контекста, который настолько легко позволяет отношения, не отягощённые мыслями о тикающих часиках, будущем-вместе-или-нет через 10 лет, и так далее, и где вы встречаетесь с кем-то ради вас здесь и сейчас, больше не будет никогда. А если вы немного интроверт, то больше никогда не будет и богатого социального графа сверстников, через которых можно естественно оказываться в одной компании с большим количеством представительниц противоположного пола, имеющих похожий с вами социальный уровень, уровень самоосознания, и так далее, и где знакомства происходят сами, с нулевым количеством затраченной энергии.
Но можно, конечно, всё это променять на урматы.
Всё ещё жду, когда мне пригодятся урматы.
Ну и да, условия позднего СССР/ранней РФ и современного мира — это, тащем, два разных мира. Сегодня входным билетом куда лучше работает гитхаб и блог, а когда я диплом последний раз показывал — и не помню. По-моему, его у меня уже даже в резюме нет.
И да,
Лучше спокойно прочитать Таненбаума или «Computer Systems: A Programmers Perspective», чем выдрочить себе интроектированным элитизмом мозг до того, что от чтения любых книг, где нет хотя бы одной теоремы с доказательством, ты ощущаешь стыд, потому что мог бы в это время читать что-нибудь про higher topos theory, например.
А свобода слова не означает свободно говорить неприятные для фирм вещи и гадящие стране факты.
А свобода совести не означает свободно придерживаться аморальных ценностей и иметь гадящее стране мировоззрение.
Нет, братиш, запутался тут ты, сорян. То, что ты называешь свободой — это не свобода, а тоталитарный загончик, который, как ты почему-то думаешь, обязательно окажется меховой частью в твою сторону.
Проблема в том, что настоящая свобода (а не этот новояз, который ты и такие, как ты, пытаются притащить в дискурс) требует осознания личной ответственности за свою жизнь, а это тяжёлое, сложное осознание.
Вы уже во второй раз пытаетесь спорить с утверждением ∀x. P x ⇒ Q x, доказывая ∃x. ¬P x ∧ Q x? И вы при этом математикой занимаетесь, да?
Мне уже второй раз очень тяжело не язвить в ответ на эту тему.
Нет смысла рассматривать существование «вообще». С подвешенным в вакууме термом
x(одиноко стоящая переменная) ничего нельзя сделать, он неинтересен сам по себе.Формализация этих правил (с системами типов, отношением типизации, и так далее) раздует статью куда сильнее, и, ИМХО, оно того заслуживать не будет.
ХЗ, в данной кодировке оно напрямую не нужно. Может, автору потом пригодится для его дальнейших замыслов, не знаю, я ж не автор. Пока оно ему нужно, только чтоб красиво печатать λ-термы.
Это, конечно, упущение!
Потому что это на самом деле одно и то же.
Переменная — это то, что видит тело функции. Вы пишете λx. x + 2, и вот эта вот штука справа от точки (то есть, тело функции) видит только переменную x.
Когда вы вызываете эту функцию, то передаёте вы ей полноценный терм, который подставляется на место этой переменной. Просто в данном случае за подстановку отвечает метаязык (мета- — потому, что это язык, на котором описывается язык), и в нём такие функции имеют тип
Term → Term.ХЗ, я gleam не знаю, но это достаточно распространённый синтаксис в языках, черпающих вдохновение в ML-семействе. При очень беглом взгляде я вообще подумал, что это раст (которого, впрочем, я тоже не знаю).
Не читерство, а higher-order abstract syntax (потом можно обобщить до P(olymorphic)HOAS).
Охренительно удобная штука, на самом деле. Вам бесплатно (из метаязыка) даётся весь набор инструментов для работы с именами и байндингами, и, как следствие, отсутствие геморроя с представлением переменных (символы? de Bruijn? locally nameless? да это всё не нужно, фигачь на метаязыке!), бесплатная α-эквивалентность, процедура подстановки (это просто применение в метаязыке), и, если метаязык достаточно мощный (ну там, coq/agda/etc), то доказательства свойств вашего языка становятся сильно проще.
(P)HOAS — сила.
Разумно. Спасибо за пояснение!