Как стать автором
Обновить

Комментарии 142

Автор не усвоил самый тяжелый урок нашего дела:
«Если ты превращаешь реальный мир в матрицы, тензоры, векторы и прочие формализмы, то позаботься о корректности своей формализации. Если ты ошибся в формализации, то тебе не поможет ничего, ни доскональное знание сотни языков, ни детальное знание тысяч библиотек, ни самая навороченная архитектура»
#8
Не, речь не про абстракции языка.
Вот пример, исследуете или рассчитываете что-то на балансах предприятий. И вдруг балансы превращаются в вектора чисел. Но именно вот тут вы и выбрасываете суть и ставите палку себе в колесо — цифры баланса это или долг ваш или долг вам, но долга самому себе не бывает. А в ваших векторах это законная конструкция )) — долг самому себе.
Вот именно про это мой пост.
Я расценил это как абстракцию в целом, не обязательно в языке или каких-то технических подходах. Абстрагироваться ведь можно на разных уровнях.
но долга самому себе не бывает

У меня бывает :) Долг физлица долгу ФОП (аналог российского ИП), если вывел все деньги с расчётного счёта, а тут "внезапно" надо налоги платить...

НЛО прилетело и опубликовало эту надпись здесь
НЛО прилетело и опубликовало эту надпись здесь
любая модель — абстракция, базирующаяся на убеждениях в данный момент постмодернистской философии. Так что доказать что либо из убеждений себе — означает мастурбацию личных убеждений. Как часы которые не показывают время, а измеряют сами себя

Корректность формализации неверной модели очень легко доказуема и ничемушеньки не противоречит. И любой агдрис (отличное имя для скандинавского божества, кстати: «Агдрис на Слейпнире, с Мьёльниром в руке джейсон ковыряет на скрипто́вом языке», — простите, вырвалось) радостно прохавает такую формализацию и подтвердит ее корректность.

НЛО прилетело и опубликовало эту надпись здесь
Можно ли в рамках этой модели доказать, что например, пароли в бд хранятся в зашифрованном виде?
НЛО прилетело и опубликовало эту надпись здесь
А оно формализовано?
НЛО прилетело и опубликовало эту надпись здесь
Ну а делать то в итоге что?
Очевидно, что пароли в базе в незашифрованном виде хранить нельзя. Как в этом помогут идрис с агдой?

Про это и говорит предыдущий комментатор — формализовать то можно что угодно, только вот толку от этого…
НЛО прилетело и опубликовало эту надпись здесь
Ну я и думал, что у вас есть ответ на этот вопрос.
Как я понимаю (хотя я даже не начинал читать), этот диссер исследует крипто-протоколы. Но проверить с его помощью факт, что пароли хранятся в базе как надо по прежднему нельзя.

Нет, можно конечно изобрести какой-нибудь протокол, при взаимодействии с пользователем, чтобы посредством пользователя проверялось, что пароли лежат как надо. Какое-нибудь доказательство с нулевым разглашением или типо того. Но во-первых, для этого нужно править код пользователя, во-вторых, это спокойно можно сделать на любом ЯП
НЛО прилетело и опубликовало эту надпись здесь
Он позволяет проверить, что алгоритм шифрования на самом деле шифрует, а не дописывает к паролю единичку (тем самым, удовлетворяя требованию «строка внутри никогда не совпадает со строкой снаружи»).


Ну понятно, что любой алгоритм шифрования как-то проверяется перед выкаткой его в продакшн (по крайней мере все на это надеются). Вопрос в том, что делать, когда он уже проверен. Чем в этом помогут сверхсильнотипизированные языки против обычного class CryptoAlgorithm?

В принципе, на уровне типов можно даже выразить, что нигде не используется конкретный API низкоуровневой библиотеки для работы с БД, чтобы убедиться, что нигде ничего не кладётся в базу в обход этих проверенных функций.

Это более интересно. Будет ли это чем-то отличаться от функции, которая принимает только аргументы типа EncryptedData?
НЛО прилетело и опубликовало эту надпись здесь
Они помогут его, собственно, проверить, и убедиться, что в конкретной реализации нет багов.

Конкретная реализация — это как правило библиотека. Там уже нечего проверять. Или вы не о том?

Да: вы можете гарантировать, что у вас нет функций, которые пишут в БД в эту таблицу и принимает вместо пароля обычную строку.

Это более интересно
НЛО прилетело и опубликовало эту надпись здесь

Предыдущий комментатор говорит не совсем про это, и предыдущий комментатор в толк не может взять, с чем именно у 0xd34df00d тут заминка (есть гипотеза, что ни с чем). Тут никакой идрис не нужен, банальной джавы хватит.


Нечистоплотная функция, принимающая данные извне, сразу возвращает тип Hashed, с единственным конструктором, который портит входной параметр. В рамках проекта на строго-типизированном языке — (без внезапных вызовов машинного кода по адресу на ровном месте) — до кода, не только до базы, — просто не сможет докатиться исходная строка.


Если надо на идрисе — можно доказать, что при проникновении строки внутрь защищенного кода она никогда не совпадает с исходной строкой снаружи.

НЛО прилетело и опубликовало эту надпись здесь
поэтому я и спрашивал про бейзлайн.

Ну вот вас, как глубокого эксперта в формальных доказательствах, приглашают в компанию улучшить (или разработать с нуля) систему хранения пользовательских паролей. Что вы будете делать?
НЛО прилетело и опубликовало эту надпись здесь
Тоесть агдрис подходит только для доказательств корректности нового яп?
НЛО прилетело и опубликовало эту надпись здесь
А вы используете идрис только для доказательств чего-то о языке, или для написания компиляторов?
НЛО прилетело и опубликовало эту надпись здесь
Решил объединить 2 треда в один, так как вопросы похожи

А что дает «проверенный» язык по сравнению с «непроверенным»?

Я как раз о написании библиотеки. И постулат о том, что там проверять нечего, и поэтому язык её написания неважен, мне неочевиден.

Тут вопрос в том, что ок, проверить корректность какого-то криптопримитива можно. Но это делали и до появления агды и идриса. Может, на бумажке доказывали, может какими-то мат.пакетами, или как-то еще. Но както справлялись.
Получается, что идрис в данном случае — это лишь инструмент, один из инструментов для доказательства утверждений, может в чем-то лучше, может хуже каких-то альтернативных инструментов.

А можно ли сделать его больше чем просто инструментом?

Например, вот разработаете вы какой-то новый ЯП. Покажете его кому-то. Этот человек захочет написать компилятор (или интерпретатор) этого языка на javascript. У вас будет возможность как-то верефицировать, что этот компилятор действительно компилирует программы на вашем языке?

Или например, вы приходите к какому-то работодателю и он просит вас улучшить безопасность передачи сообщений по ненадежному каналу. Вы выясняете нужные требования и пишете на идрисе программу по типу:
Дано: Алиса и Боб, которые хотят отправить друг другу сообщение.
Доказать: Кэрол не сможет перехватить и расшифровать сообщение.

Вы пишете такую программу, получаете миллиард долларов и уходите. А дальше, лаборанты за 20000р в месяц доказывают на идрисе все нужные теоремы для используемых протоколов. Нужен протокол TLS — они доказывают ваши утверждения для протокола TLS. Нужен какой-то другой протокол, они пишут доказательство для этого другого протокола. И дальше, любое сообщение, отправленное через такую программу будет отправленно заведомо надежным образом, со всеми прошедшими валидациями.
Такое возможно?
НЛО прилетело и опубликовало эту надпись здесь
У вас будет возможность как-то верефицировать, что этот компилятор действительно компилирует программы на вашем языке?
Да.


А как это вообще будет выглядеть?

Не уверен, что возможно именно такое разделение труда, но вот чтобы написать программу вместе с теоремами, и доказать, что для программы выполняются эти теоремы — это можно.

А разве с ЯП не тоже самое? Яп отдельно, компилятор отдельно.
НЛО прилетело и опубликовало эту надпись здесь
а, ну тоесть для каждого компилятора придется отдельно доказать, что он удовлетворяет тому, что надо? Ну так не пойдет, я думаю.
Ну например, если я подсуну вам компилятор C#-па, как быстро вы поймете, что он не компилирует ваш язык?
НЛО прилетело и опубликовало эту надпись здесь
Ну я на это и надеялся, на самом деле. В ином случае не вижу смысла во всем этом. Ну тоесть я на самом деле подозревал, что примерно так и есть, но на чудо надеялся

Ну хорошо, а если упростить задачу, и скажем пусть компилятор будет написан также на идрисе (но без оглядки на ваши доказательства, только по спецификации), сможете ли вы в этом случае с минимальными усилиями верифицировать компилятор?
НЛО прилетело и опубликовало эту надпись здесь
А в чем тогда смысл комментария
«Проверяемый». Даёт возможность формально, машиной проверять реализацию на соответствие спеке.

Если все настолько сложно?

И какое всеже выходит преимущество у такого языка?
НЛО прилетело и опубликовало эту надпись здесь
Ну смотрите. Давайте еще раз. Вот есть 2 сущности: семантика языка, написанная и проверенная на агде, и компилятор непосредственно этого языка, написанный тоже на агде (но без оглядки на первую реализацию). Можно ли между этими 2 сущностями построить третью сущность (не меняя первые 2, или меняя чисто косметически, правда что такое «косметически», придется договариваться отдельно), чтобы она доказывала, что первая сущность соответствовала второй сущности? И как в этом случае проверить, что эта промежуточная сущность действительно проверяет что нужно, а не возвращает всегда true или random(2)?
НЛО прилетело и опубликовало эту надпись здесь
Ну я примерно это и имел в виду.
А если, например, вот вы построили доказательство, что реализация конкретного компилятора соответствует вашему языку, и тут вам приносят еще один компилятор, как сложно будет адаптировать текущее доказательство под него?
НЛО прилетело и опубликовало эту надпись здесь
Нет, язык то тот же самый. Компилятор другой.

И предвосхищая следующий ответ (чтоб 2 раза не ходить), в чем же тогда преимущество вашего разрабатываемого яп, если для него не построить нормальный стандартификатор (хз, как это назвать, в общем, программа которая проверяет соответствие компилятора на стандарт)

(Почемуто на почту уведомление об ответе пришло только через сутки)
(хз, как это назвать, в общем, программа которая проверяет соответствие компилятора на стандарт)

Валидатор, например solidsands.com/supertest
НЛО прилетело и опубликовало эту надпись здесь
Каков язык, таков и валидатор. Доказательство корректности компилятора C++ — задача для Deep Thought, не меньше.
Ну дак предложите не тесты. Хотябы для своего языка. О чем и прошу уже не один комментарий
НЛО прилетело и опубликовало эту надпись здесь
Я все никак не могу понять, что вы проверяете — язык или компилятор? Это разные вещи
НЛО прилетело и опубликовало эту надпись здесь
Ну я то спрашивал как раз про компиляторы. Вам вот не нравится, что верификация компиляторов C++ проводится тестами. Вот я и спрашиваю, можно ли написать такой язык, верификация компиляторов которого будет проводится не тестами. (естественно, я понимаю, что для каждого компилятора в отдельности можно написать свое огромное доказательство, вопрос то тут как раз в постановке верификации «на поток»). И почемуто ответ я до сих пор не могу получить

А какому современному языку требуется несколько компиляторов и зачем?


Времена закрытых компиляторов, породивших открытые аналоги, вроде далеко в прошлом.

А почему бы и нет? По крайней мере, это единственное применение, которое я вижу для формализованного языка
НЛО прилетело и опубликовало эту надпись здесь
Разве языки, позволяющие формализовывать разные вещи, не должны сами быть формализованы? Разве реализациям этих языков не требуется формальное доказательство корректности?

Если вы многократно замечали дефекты в чужих языках, то как вы принимаете на веру, что используемый вами в вашей работе тайпчекер никогда не принимает неверные доказательства за верные?
НЛО прилетело и опубликовало эту надпись здесь
Если, по-вашему, компиляторы C++ далеко в прошлом, то можете сосчитать, сколько сейчас есть (открытых) компиляторов JavaScript или Python.
Вот я и спрашиваю, можно ли написать такой язык, верификация компиляторов которого будет проводится не тестами [...]

Я почему-то думал, что JS и питон уже написаны, а что такое компилятор интерпретируемого языка — я вообще не очень понимаю.


как вы принимаете на веру, что используемый вами в вашей работе тайпчекер никогда не принимает неверные доказательства за верные?

Ну идрис вот написан на идрисе, он умеет проверить самое себя, в принципе.

Я почему-то думал, что JS и питон уже написаны,

По-вашему, это последние в истории языки, для которых активно разрабатываются конкурирующие компиляторы?

что такое компилятор интерпретируемого языка — я вообще не очень понимаю.

Обычно JIT, но существуют Cython, github.com/eddid/jslang и т.д.

Ну идрис вот написан на идрисе, он умеет проверить самое себя, в принципе.

Т.е. корректность идриса полагается на корректность идриса?
НЛО прилетело и опубликовало эту надпись здесь

Можно, ту сам экстент.


На самом деле инвариантность преобразований доказывать почти всегда гораздо проще, чем оригинальный пучок лемм.

НЛО прилетело и опубликовало эту надпись здесь
Ну пока все равно не понял, насколько проще. Судя по всему, мы опять о разном.

То есть что в итоге я хочу вытянуть. Есть 2 разных типа задач

1) Есть яп, разработанный для конкретной цели (удобная верификация) на конкретном языке (идрис). К нему независимые разработчики, пользуясь только спецификацией языка, пишут компилятор (тоже на идрисе, так как на других языках все равно не проверить). Можете ли вы относительно безболезненно верифицировать представленный компиляторы на этот конкретный яп?

2) Предположим, вам дали задачу повысить безопасность (в криптографическом плане) передачи данных между двумя клиентами. Вы приходите, выслушиваете требования заказчика (например, требование, что «человек посередине» не сможет перехватить и расшифровать передачу), выписываете эти требования в виде заголовков теорем и уходите. Дальше, лаборанты начинают встраивать существующие (или новые) криптопротоколы в ваши теоремы, чтобы они стали им удовлетворять. Здесь сложность встраивания уже не играет роли, основное требование это то, чтобы любое сообщение, посланное через такую программу, всегда удовлетворяло обговоренным требованием безопасности (чтобы например разработчики не смогли просто подменить библиотеку, и остаться вообще без шифрования, и этого никто бы не заметил). Насколько возможно это?
Предположим, вам дали задачу повысить безопасность (в криптографическом плане) передачи данных между двумя клиентами...

Кажется, то, что вы описали — это в точности https://project-everest.github.io/.

Да, похоже на то. Как понимаю, разработка будет вестись на F*. Насколько F* близка к идрису?
НЛО прилетело и опубликовало эту надпись здесь
Если я правильно помню, есть 2 способа проверять формулы: выводом формулы по правилам логики или обычным перебором с оптимизациями. Что используется в F*?
НЛО прилетело и опубликовало эту надпись здесь
НЛО прилетело и опубликовало эту надпись здесь
Относительно безболезненно в мире верификации вообще ничего не происходит.


А есть какаято теоретическая возможность сделать это менее болезненным?
НЛО прилетело и опубликовало эту надпись здесь

Потому что «каждая селедка рыба, но не каждая рыба — селедка», как говаривал один капитан дальнего плавания.


Я никогда не утверждал, что никакую ошибку поймать нельзя. Я сказал, что не все ошибки элиминируются таким незамысловатым образом. Модель, пытающаяся складывать яблоки и апельсины, безусловно, будет отбракована. Модель, превращающая в качестве сложения все фрукты в пюре — пройдет любую валидацию.


Контекст статьи тут вообще ни при чем.

НЛО прилетело и опубликовало эту надпись здесь
Почему не усвоил? Может просто не отметил в статье.
Еще можно добавить то, что надо избегать работать в компании/с людьми, у которых тяп-ляп (и так сойдет, этот код у нас издавна и не надо его трогать) поставлен в систему. MVP — шикарно и нужно, но MVP, превратившийся в легаси- это болото деградации и уныния. Надо быть очень хорошо замотивированным материально, или просто очень голодным программистом, чтобы работать там.
Еще можно добавить то, что надо избегать работать в компании/с людьми, у которых тяп-ляп (и так сойдет, этот код у нас издавна и не надо его трогать) поставлен в систему

… если выплачиваемая вам там зарплата не позволяет закрывать глаза на подобного рода недостатки :)
Thoth777 так и написал в своём последнем предложении.

Так это нигде работать нельзя, выходит?

Ну почему же нельзя? Просто надо принять во внимание пару вещей:
1. Когда контора хантит свежего разработчика, она, как правило, ищет человека, знающего современные фишечки, даже если они ей нафиг не нужны. Просто так принято, что даже в самой отсталой конторе, чел на собеседовании будет вас гонять по всяким DRY / SOLID, паттернам, особеностям новых версий языка программирования, просто потому что это так принято.

2. Когда вы занимаетесь лепкой пулек из какулек, поддерживая легаси и не рефакторя его, вы деградируете как разработчик (или же вам надо самообучаться в свободное от работы время). Я прям точно не знаю как в других языках, но в PHP например, регулярно выходят обновления, а фреймворки развиваются еще стремительнее. 3-4 месяца без изучения нововведений — и все, вы устареваете.

Что проще: эволюционировать вместе с компанией, или отдельно от нее, в нерабочее время?

Я вот полтора годика посидел на проекте на устаревшей версии языка, работа + дорога занимала порядка 11 часов в день. А вечером голова уже не способна воспринимать новую инфу, да и отдохнуть хочется. Когда пришло время менять работу, мне пришлось, как студенту, зубрить это все. А мог бы и так знать, применяй я это все на практике.
Следующая моя работа была: свежая стабильная версия PHP, свежая стабильная версия фреймворка.
Просто так принято, что даже в самой отсталой конторе, чел на собеседовании будет вас гонять по всяким DRY / SOLID, паттернам, особеностям новых версий языка программирования, просто потому что это так принято.

Бывает и противоположное: я однажды на собеседовании упомянул, что моим первым языком программирования был BASICA, после чего CTO компании стал меня экзаменовать по его особенностям %)

У меня так по FORTH было )

С оптимизацией вообще веселая штука. Один раз был такой неоптимальный код, что так и просил его оптимизировать. В итоге через пару часов его удалось ускорить в 10 раз. С 0,1 секунды до 0,01. И выполнялся он на форме ручного ввода данных. Один раз.

Да, но бывает и обратная штука. Когда в коде (обычный фронтэнд, ничего сверхъестественного) центральное и единственное место, которое вообще только может в этом коде тормозить (вывод списка) — написано в виде огромной свалки жестко связанных частей, и, разумеется, безумно тормозящим образом. И без переписывания начисто большей части проекта с этим ничего не сделать. Зачем так делали? "Ну нам надо было быстро MVP" (с)


И после такого — действительно, последние 10% работы занимают 90% времени. Потому что в эти "последние 10 процентов" на самом деле входит "сделать всё по-новой, только на этот раз вменяемо". Я, кстати, из всего своего трудового стажа примерно половину времени именно на этом и специализируюсь — переделываю чужой говнокод, который "главное — работает!" и "на 90 процентов готов, остались сущие пустяки!".

НЛО прилетело и опубликовало эту надпись здесь
Забавно.
Сижу читаю на хабре разные умные мысли, иногда да, а иногда… вот такие.
Сидит пачка «кого либо» и обсуждает свою профессию, что надо, как надо, что мы могучи и т.п. а по факту эти могучи заменяются… любым со двора, и ничего не падает в плане работы, все продолжает отлично работать.
Нет фактора — меня могучего увоилил и все встало.
Почему?
Потому что, все работает не на вас. И проработает с успехом еще долго, даже если взять сотрудника на пол ставки неуча.
Это просто вот так вот работает, как не парадоксально в большнистве своем, а с учетом прихода и ухода, и меняющегося рынка и требований — это скорее норма чем исключение.

А по фатку в статье очивидные вещи — ты никто и звать тебя никак, и учиться надо всегда, и теперь уже не только в ит. Мир говорит надо быть быстрым, а не опытным.
НЛО прилетело и опубликовало эту надпись здесь
Именно, он решил, узнал и пошел познавать зная причину, а не сидел еще 5 лет думая «не… ну я еще не опытный, это не для меня, пусть спецов ищут и так всю жизнь»
Таког ОПЫТА и не будет если ты не имея его не будешь делать то где он нужен.
Вы просто были местом где этот человек решил что научитсья, ну не вышло, научитсья в другой конторе «завтра», а не когда нибудь «потом», когда будет все знать.
Вы просто были местом где этот человек решил что научитсья, ну не вышло

«Мы любим свою работу, но должны понимать, что решаем проблемы»
НЛО прилетело и опубликовало эту надпись здесь
Ит достаточно редко является бутылочным горлышком в компании и что бы довести его до такого состояния надо действительно постараться. Впрочем даже и такие прецеденты известны.
По сути всё верно, а дальше поизвращаю малость:
1. Решая проблемы, не забудьте, чтобы вы своими не оптимизированными кодами их не добавили. Прежде всего, вы работаете во благо цели организации, предприятия, компании…даже если это компания разработчиков и вы хитро ушли от ответственности.
2. Разработчик такой же инструмент и винтик (гвоздь) в механизме бизнеса. Языки хорошо изучать… но может изучить другие бизнес идеи по зарабатыванию?
3. Факт, что если вам не подходит разработчик… то просто меняйте его. Дело не том, что знать алгоритмы, а хотя бы помнить куда копать и где найти, так что как раз это и помогает быстрее решать проблемы. В больших компаниях уже полно готового кода, библиотек кода и там просто шаг влево или вправо уже увольнение.
4. Идите в начальники, там можно абстрактно думать и переливать одно и тоже в разные виды и втирать юзерам, что это такой дизайн и это сейчас модно и тд и тп
5. Цена работы программиста очень большая, так что если самолет летит, то главное чтобы выглядел красиво (как у Макса скафандр и др), а центр тяжести, да двигатели как-то потом доделаем
6. Пройти тест – это важно, оптимальность не главное для большинства случаев, а для передовых компаний нужен и передовой софт, где уже оптимальность будет важнее (забейте об оптимальности, скоро снова ядер компам добавят и как-то это будет работать)
7. Если 10% проекта занимали 90% времени, значит, проектирования и не было. Тут пропущено слово РЕАЛИЗАЦИИ Хорошее проектирование – залог быстрого, четкого и правильного приложения и почти 50% работы. Но вот хорошее проектирование почти не бывает, ну разве что на готовом шаблоне и сказать, что месяц делал :) Ну и чем больше проект, тем БОЛЬШЕ ЖОПА и непредсказуемость того, что наделают кучи программистов. Чем проще – тем надежнее.
8. Абстракция всегда должна быть, просто название приложения уже есть 1 уровень абстракции. Погружаясь дальше, вы все больше и больше опускаетесь в тонкости реализации, до кода, а кто и до ассемблера и до железа доходит.
9. Сторонний проект поможет не сойти с ума…писать тесты каждый день? Пусть этим проектом будет всегда семья и ваши дети.
Языки хорошо изучать… но может изучить другие бизнес идеи по зарабатыванию?

Ваше предложение сменить род деятельности звучит не лучше, чем «Языки хорошо изучать… но может выучиться на адвоката или на дантиста, ведь они зарабатывают ещё больше?»
Не ограничивайте себя — говорит автор. Не мыслите узко, так как словосочетание «бизнес идея» может быть и на вашем языке и вашей деятельности. Проверить, что вам надо очень просто: представьте, что выиграли 10000000 баксов… кажись хватит. Так вот, что вы будете делать, изучать языки, приумножать эти деньги, поделитесь с кем-то и тд и тп. Вот тогда ясно будет, для чего человек сидит на работе и ради чего, что ему приносит радость, какова его цель в жизни?
В тенечке под пальмой лежит негр, отдыхает. Идет поблизости белый и говорит негру:
— Чего ты лежишь под деревом, на котором столько бананов? Возьми палку, сшиби
несколько штук, пойди на рынок и продай их…
— Зачем?
— Как зачем? Деньги получишь — наймешь еще десяток негров, которые будут бананы с пальм сшибать, а ты будешь продавать.
— Зачем?
— Потом наймешь сотню негров, посадишь тысячу пальм и будет у тебя огромная банановая плантация.
— А это зачем?
— Будешь богатый. Другие будут работать, а ты будешь только лежать в тенечке под пальмой и отдыхать.
— А сейчас я что делаю?
НЛО прилетело и опубликовало эту надпись здесь
Еще бы добавил.

Каким бы вы круты не были лет через 5-6 вас сократят решением акцинеров, чисто чтобы снизить издержки бизнеса. На моей 20 летней практике кровавого ентерприза — 3 раз по 6 лет. Уйдут или скопом и одним за другим. И каждый раз процесс найма все тяжелее и тяжелее.

Учите оба стека Linux/Windows. C++/C#/Java/Python/SQL. (это мой стек)
У кого-то будет Go/Javascript/…
Со временем эти языки и так будут воспользованы в разных проектах, а в голове будет перманентная каша из синтаксиса.

Поэтому есть 5-6 темплейтов резюме с разными стеками.

Раз в год сдавайте/подтвержадайте сертификат на знание из одного из языков.
Каждые полгода сертификат на новомодное напреавление в технологиях.

Docker/K8/AWS,…

Раз в неделю проходите интервью куда-нибудь на работу. Тем более сейчас все online.

Это должно стать обыденностью. Каждый день решайте задачи на hackerrank и leetcode.

Задачу сабмитте на каждом языке для усвоение материала и поддержания знания языков

Некоторые уже совсем обнаглели и даже перед первым интервью сразу шлют ссылку на

You have been invited to attend the challenge CDN Company Senior Full-Stack Engineer. We wish you all the best!

Дают легкие задачки, но иногда их пишут люди с неродным английским и ужасным описанием.
Если вы не прошли — да и пес ними — звезды на небе не совпали.

Через полгода опять подадите.

Pet проект жалательно иметь. вебсайт с распределенной базой данных, REST сервисами, картой, множеством IoT датчиков и большими обэмами данных.

Некоторые перед интервью спрашивают описать как организована домашняя сеть.
What operating system do you run at home? What does your home computer network look like?

В конце интервью с командой всегда интересуйтесь если девушки среди разработчиков, есть ли музыкальная банда и нет ли спортивной группы типа катания на лыжах или игры в кегли.

От них тоже зависит окончательное решение и должны понять что вы свой.

Раз в год сдавайте/подтвержадайте сертификат на знание из одного из языков.
Каждые полгода сертификат на новомодное напреавление в технологиях.
Docker/K8/AWS,…
Раз в неделю проходите интервью куда-нибудь на работу. Тем более сейчас все online.
Это должно стать обыденностью. Каждый день решайте задачи на hackerrank и leetcode.
Задачу сабмитте на каждом языке для усвоение материала и поддержания знания языков

… или заведите вместо всего этого барахла приятное хобби, и получайте удовольствие от жизни, а не от непрерывного выпахивания на свои скиллы, чтобы потом еще больше пахать на свои скиллы.
НЛО прилетело и опубликовало эту надпись здесь
А почему у него тогда весь пост пропитан болью и страданием? :)
Ну странно в таком случае выставлять хобби как безусловный пункт получения работы. Иначе с тем же успехом он мог написать «Смотреть по 2 серии игры престолов каждый день»
Встречал я такого devops, на момент собеседования у него было около 30 сертификатов. Правда 95% из них от ноунейм сайтов, но его это не смущало. Он считал что чем больше — тем лучше.

P.S.
собеседование он провалил
Хороший годный план спасибо. Остался маленький нюанс уточнить: А работать когда? а проводить время с семьей когда? А время на хобби остается? ну или хотя бы на поспать?

Каждую неделю собесы проходить? Каждый день задачи на hackerrank? А где у вас столько времени?

Видимо, с этим связано
лет через 5-6 вас сократят

:)

Столько времени затрачивать на поддержание своей конкурентоспособности — это перебор. Ну только если это все по фану. Гораздо эффективнее этим заниматься в процессе смены работы. Пару месяцев после увольнения вполне позволят подтянуть навыки до нужного уровня почти в любой смежной области (в том числе и навыки прохождения собеседований). Эти знания будут достаточно актуальны, не успеют еще подзабыться.

Главное что бы от этого кукуха не поехала, а то будешь со всеми этими знаниями всегда улыбаться и ходить под себя.

Очень верные умозаключения
Только вот система отбора кандидатов у большинства работодателей рассчитана на людей несколько иного склада
На самом деле изучение различных языков очень неплохая тренировка памяти и получение полезных навыков. Но куда важнее разработать свой язык и желательно его реализовать.
Я прочитал книгу Seven Languages in Seven Weeks несколько лет назад, и она открыла мне множество вариантов только потому, что показала способы решения задач, доступные в других языках.

Вот только большинство промышленных задач решаются не языками, а экосистемой библиотек в них. По сути, эффективность разработчика зависит в большей степени от количества и качества готовых решений, предложенных в этих экосистемах, нежели от самих языков. А это пласты знаний посерьезнее "7 языков за 7 недель".

большинство промышленных задач решаются не языками, а экосистемой библиотек в них

Есть три типа задач:


  • проектик для портфолио, когда начал учить новый язык
  • обычная работа на галере
  • что-то новое, интересное и сложное

Так вот множества задач, решаемых экосистемой (②) и задач, которыми заниматься хочется (①, ③) не пересекаются вообще никак. В нормальных задачах ну вот разве что только хранилище данных и брокер сообщений можно взять готовые, да и то придется напильником полировать.

Как же тогда человек, постоянно увлекающийся пунктами 1 и 3, всегда умудряется попасть в пункт 2?
Не соглашусь: например, pandas и NumPy — не часть Питона, но сложно представить датасатанистское исследование класса ③ без использования этих библиотек.

Ну, скажем, Франсуа Коллету пришлось, и правда, затащить пару библиотек в работу класса ③.


Но «датасатанистское исследование» как таковое — это уже давно класс ②.

Хорошие советы. Особенно про эго, в первый раз вижу, что кто то об этом написал. Приятно, что где то есть такие люди.

У разработчиков раздутое эго. Это факт.

Чтобы обобщать подобные вещи, да ещё представлять их как факт — требуется недюженное эго ;-) Так что выучил ли автор урок номер 1 — тот ещё вопрос.

Языки — это инструмент. Вы знаете только молоток? Тогда все проблемы похожи на гвозди

Знаете что я вам скажу… если язык инструмент, то это не язык.
Настоящие языки настолько универсальная штука, что никакого другого не надо. Что русский, что английский, что французский могут все. И эффективно.
«Карл V, римский император, говаривал, что испанским языком с Богом, французским — с друзьями, немецким — с приятелями, итальянским — с женским полом говорить прилично», — писал несколько веков назад Михаил Васильевич Ломоносов, создатель русской научной грамматики.
П.1. Проглотите его и выслушайте то, что другие люди скажут о вашей работе.

В своей деятельности приходится констатировать тот факт, что подавляющее большинство людей не могут сказать что либо связанного даже о своей работе. Даже если у них прописано это в должностных обязанностях. И, поверьте, это не мое раздутое эго, к сожалению, это печальный факт. Попробуйте посидеть пару дней в отделе техподдержки — вы заплачете. Крокодильи слезы будут литься по Вашим щекам о том, что человечество обречено, о том кто же нанял всех этих людей, о судьбах людей не на своих местах и о пути, куда катиться этот мир. И да, вишенкой, Ваши попытки, в основном тщетные, исправить это положение дел будут натыкаться на то, что Вас не будут вообще серьезно воспринимать пока вы не продемонстрируете свое (пусть и полностью дутое) чрезмерное Эго. И вот когда Ваше Эго заставит Вас запросить за час сотню юсд, клиенты подумают — а не пора ли собственно попробовать решить свои проблемы самому, ибо че то дорого стало сваливать все свои проблемы, которые я же и генерю, на этих ИТшников. И только в этот момент их проблемы начнут действительно решаться и мир озарит луч надежды.
Отсюда п.0 — никогда не пренебрегайте диалектикой
Тут гораздо больше решает спрос на высокую квалификацию, иначе откажут, а может ещё и поймут что с подводной лодки всё равно не куда, да и вы сами в эти правила игры начали, кстати стрелочка в одну сторону уже не крутится.
В вашем случае поможет расценки в час сделать меняющимися в зависимости от оказываемых услуг. Но хорошо что это дорого считать))
Один важный пункт не описан. Постоянный поиск баланса. Когда выбрать brute force, чтобы замастырить дырочку, а когда найти время на создание эффективного и элегантного алгоритма. Когда вывалить спагетти ассоциаций по поводу задачи, а когда структурировать потоки и причесать абстракции. Когда решить расширить функциональность сервиса или выбрать рефакторинг кода. Программирование — это искусство возможного. И хождение по канату.
опыт разработки чуть больше наверное будет, и под каждым пунктом подпишусь. все совершенно правильно. как говорится, если ты молод и думаешь по другому, через какое то время ты будешь думать так же.
Очень много правил. Я бы описал все проще и даже безотносительно программистов:
1. Надо любить то, что делаешь.
2. Надо уметь учиться новому.
Все остальное вытекает из этих двух.
Я бы пофиксил первый пункт так:
Надо делать, что любишь.

По части абстракций не стоит увлекаться и бросаться в крайности. Немного копипасты лучше, чем огромная зависимость, которая пытается натянуться на всевозможные ситуации в куче разнородных программ, причём, решая их все довольно посредственно. Перед тем, как что-то выносить во внешнюю библиотеку или даже функцию, стоит десять раз себя спросить, настолько ли оно универсально, чтобы надёжно решать эту задачу в будущем? И нужна ли эта универсальность, если решаемая проблема действительно не такая уж и сложная?


Это всё приходит с опытом, конечно. Но часто лучше делать маленькие и функциональные, реиспользуемые блоки, из которых можно собрать решение конкретной задачи (пусть и каждый раз заново!), чем большой, абстрактный и универсальный монолит, который вроде и решает 90% задач, но оставшиеся 10% в него настолько плохо вписываются, что начинаются большие проблемы. Либо копировать и менять под задачу этот монолит (нельзя скопировать лишь кусочек, оно слишком абстрактное для этого), либо продолжать раздувать код для покрытия новых редких случаев, которые в 90% использоваться не будут.


По сути, проблема похожа на композицию и наследование. Первое ты для каждого случая собираешь из частей, зато оно модульное и гибкое, а второе ты получаешь сразу готовым и универсальным, но с сопутствующими головными болями при нестандартных требованиях. Реалии таковы, что требования меняются часто, и конструкторы оказываются более пригодны для решения настоящих задач.

Не делать, но время от времени смотреть сторонние проекты — маст хэв
Если вы собираетесь потратить ещё два дня только на то, чтобы сделать код идеальным, но он может пойти в производство прямо сейчас, то есть шанс, что он должен быть в производстве прямо сейчас.
Оправдание для костылестроения получено.
Ранняя оптимизация является проблемой, потому что в конечном счёте вы тратите много времени и усилий на то, что, возможно, не нуждается в оптимизации.
Так оптимизация не нужна или всё же костыли не нужны?
В начале
5. Работающее лучше идеального
потом
6. Заставьте код работать, затем оптимизируйте
а после внезапно
7. Последние 10 % проекта занимают 90 % времени


В начале делаем тяп-ляп, лишь бы быстрее показать что-то заказчику не вдумываясь в архитектуру и переиспользование элементов
А потом под конец проекта ВНЕЗАПНО его становится очень тяжело поддерживать, добавлять некоторые штуки очень тяжело и вообще скорей бы уже новый, а то этот какое-то г-но

Может быть лучше сразу разрабатывать вдумчиво, пусть и несколько медленнее, за-то сохраняя грамотную структуру?
Мне кажется, здесь не имеется в виду говнокод в угоду скорости. Приведу два примера с текущего проекта:
5 — оплату картой реализовали, а сохранение карты подождет пару недель
6 — заявки пользователя один раз из десяти обрабатываются неверно, пока что можем позволить вместо автоматизации исправления ошибок обойтись мониторингом и ручной правкой в базе
При этом остается время на тесты и на исправление багов по выкаченным ранее фичам.
Вот моё личное правило: если код повторяется в двух местах, он отправляется в функцию (метод, модуль); вы поняли идею.

И, абстрагировав код сразу, вы сразу будете иметь к нему доступ.


Если только в двух местах — ничего не делать. Отпустить и жить с этим дальше.

Если в трёх — сделать пометку чтобы вынести в абстракцию… потом… когда наступит четвёртый раз.

Если в четырёх местах — вот тут уже в кайф делать эту абстракцию, т.к. видешь её уже чуть выше, чуть больше имеешь контекста, меньше шансов сделать неудачную абстракцию которая будет протекать.

Это всё вообще не от количества мест зависит, к слову. А от модели.
Потому что существуют случаи, когда и повторенный 20 раз код ни в коем случае не нужно никуда выносить, потому что корректной доменной абстракции просто не существует (а то, что 20 раз одно и то же — не более, чем редкое совпадение обстоятельств).

4. Вы будете учиться всю свою карьеру
этот пункт актуален для всех сфер деятельности
Спорно, чему учится всю жизнь условный продавец в продуктовом магазине или водитель автобуса?
НЛО прилетело и опубликовало эту надпись здесь

И чему будет учиться всю жизнь продавец из 5ки?

НЛО прилетело и опубликовало эту надпись здесь

Ну такое, притянуто за уши, имхо

Вежливости учатся явно не всю жизнь, а один раз в детстве. Раскладка товара — это не работа продавца супермаркета. Точнее, непосредственно раскладывает-то обычно он, но насчёт «что и куда ставить», его мнение никого в супермаркете не интересует, планограмму выкладки товаров составляют отдел маркетинга и договорной отдел, ну, ещё администратор торгового зала и/или заведующий магазином в этом участвует. И кассовые аппараты — тоже не его дело, да и учиться там, в общем-то, особо нечему.
Зарегистрируйтесь на Хабре, чтобы оставить комментарий