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

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

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

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

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

Знание языков, позволяющих доказывать корректность формализации, таки поможет.

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

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

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


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

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

Если формализовано понятие «зашифрованный вид», то да.

А оно формализовано?

Так это у разработчика системы надо спрашивать. Я-то пароли в БД вообще не храню, поэтому не знаю.


Впрочем, если это понятие не формализовано, то как вы про него вообще рассуждаете, как вы этот факт проверяете, и так далее?

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

Про это и говорит предыдущий комментатор — формализовать то можно что угодно, только вот толку от этого…

Давайте, чтобы я лучше представлял приемлемый уровень гарантий, обсудим сначала, как в этом убедиться безо всяких идрисов с агдами? Ну там, тесты какие писать будете? Или что вообще делать будете?


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

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

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

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


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

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


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

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

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

Они помогут его, собственно, проверить, и убедиться, что в конкретной реализации нет багов.


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

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

Они помогут его, собственно, проверить, и убедиться, что в конкретной реализации нет багов.

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

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

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

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

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


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


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

Это вариант, и люди так делают не только для паролей и не только в завтипизированных языках. Проблема с этим подходом в том, что у вас нет гарантий, что у вас нигде не дёргается API БД напрямую, чтобы сохранить туда что-нибудь незашифрованное. Более того, нет гарантий, отличных от «ну я эту функцию String → Hashed прочитал, она вроде хеширует», что функция действительно портит входной параметр, что она не ксорит его с 0xff, а делает что-то более сложное, и так далее.


Есть формализмы, позволяющие выражать соответствующие требования на формальных языках (мелкомягкий Project Everest во многом про это), но я понятия не имею, как именно они это делают.


Но, в любом случае, тестами вы это всё равно фиг проверите, поэтому я и спрашивал про бейзлайн.

поэтому я и спрашивал про бейзлайн.

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

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

Тоесть агдрис подходит только для доказательств корректности нового яп?

Ага, а C++ подходит только для написания всякого машинлёрнинга и немного трейдинга, ведь лично я не умею писать на нём игры или там веб-сервисы.

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

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


В чуть более прикладных задачах люди пишут:


We present the first complete, intrinsically typed, executable, formalisation of System Fωμ that we are aware of. The work is motivated by verifying the core language of a smart contract system based on System Fωμ. The paper is a literate Agda script.

И idris 2, например, написан на идрисе.

Решил объединить 2 треда в один, так как вопросы похожи

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

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

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

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

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

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

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

«Проверяемый». Даёт возможность формально, машиной проверять реализацию на соответствие спеке.


Но это делали и до появления агды и идриса.

Так и компьютеры программировали как-то до появления питона, JS и даже C. Но с ними удобнее, быстрее, надёжнее, масштабируемее, етц.


Может, на бумажке доказывали, может какими-то мат.пакетами, или как-то еще.

Ну вот бумажке у меня веры нет.


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

Именно так! Как и любой другой язык программирования.


У вас будет возможность как-то верефицировать, что этот компилятор действительно компилирует программы на вашем языке?

Да.


Такое возможно?

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

У вас будет возможность как-то верефицировать, что этот компилятор действительно компилирует программы на вашем языке?
Да.


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

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

А разве с ЯП не тоже самое? Яп отдельно, компилятор отдельно.
А как это вообще будет выглядеть?

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


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


такие теоремы про сам язык


или


про преобразование


Соответственно, у этого всего либо есть, либо в обозримом будущем будет формальное доказательство в виде кода на всех этих агдах с идрисами.


А разве с ЯП не тоже самое? Яп отдельно, компилятор отдельно.

Компилятор — это реализация ЯП, да. Так и конкретный тайпчекер — это конкретная реализация условного конкретного языка с зависимыми типами.


Ну или я тут вас не понял.

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

А вы думали, что это магия какая-то, типа, написал, что хочешь, а оно там покрутило шестерёнками и выдало «доказано, мамой клянусь!»?

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

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

Этому чуду не суждено осуществиться как минимум по связанным с Тьюрингом причинам, увы :(


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

Это будет, конечно, проще. Но доказывать вообще довольно трудоёмко. Десяток лемм, которые на бумаге доказываются в основном утверждением «Straightforward induction on $X», на агде у меня заняли порядка тыщи строк и месяца три работы (но при этом я находил дырки в бумажных доказательствах, недостаточно мощные предпосылки, и так далее, и в результате я вот прям вообще уверен).

А в чем тогда смысл комментария
«Проверяемый». Даёт возможность формально, машиной проверять реализацию на соответствие спеке.

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

И какое всеже выходит преимущество у такого языка?

Ну вас же не смущает, что ТЗ может быть на десятке листочков, а реализация — на десяток-сотню тысяч строк? Зачем языки программирования, если всё настолько сложно?


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


А преимущество в том, что когда проверяет машина, то она


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

Да, только доказательство вы сами пишете. Тайпчекер только проверит его корректность.


И как в этом случае проверить, что эта промежуточная сущность действительно проверяет что нужно, а не возвращает всегда true или random(2)?

Посмотреть на тип тех функций, которые представляют доказательства искомых утверждений.


Например, утверждение одной из теорем со скринов выше представляется в коде как


preservation : ε ↝ ε'
             → Γ ⊢ ε ⦂ τ
             → ∃[ τ' ] (Γ ⊢ ε' ⦂ τ')

Оно достаточно мелкое, чтобы было понятно, что это не всегда true, а его доказательство вам неважно — оно там для тайпчекера.


Или, например, если мы вдруг хотим сделать доказуемую функцию сортировки, то мы сначала определяем понятие упорядоченного списка:


data OrderedList : (f : Order a) -> (xs : List a) -> Type where
  EmptyList       : OrderedList f []
  SingleList      : (x : a) -> OrderedList f [x]
  ConsOrderedList : (f : Order a) -> (x0 : a) -> {auto prf : So (x0 `f` x1)} -> (rest : OrderedList f (x1 :: xs)) -> OrderedList f (x0 :: x1 :: xs)

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


Потом мы определяем, что значит, что один список является перестановкой другого:


data (~~) : (xs : List a) -> (pxs : List a) -> Type where
  PNil    : [] ~~ []
  PSwap   : x0 :: x1 :: xs ~~ x1 :: x0 :: xs
  PRest   : (rest : xs ~~ pxs) -> x :: xs ~~ x :: pxs
  PTrans  : (p1 : xs ~~ pxs) -> (p2 : pxs ~~ ppxs) -> xs ~~ ppxs

То есть:


  • пустой список является перестановкой пустого списка,
  • список [x0, x1, xs...] является перестановкой списка [x1, x0, xs...],
  • если два списка — перестановки друг друга, то можно к ним обоим дописать в начало один и тот же элемент,
  • отношение перестановочности транзитивно по определению.

Это уже звучит чуть сложнее, поэтому дальше можно доказать, что если два списка являются перестановками друг друга в смысле этого определения, то они являются перестановками и в смыслах вроде «если элемент встречается в одном списке N раз, то и в другом списке он встречается N раз», но не суть.


А дальше, короче, мы пишем, что список, сортированный согласно отношению f — это перестановка исходного списка, являющаяся упорядоченной:


data Sorted : (f : Order a) -> (orig : List a) -> (sorted : List a) -> Type where
  MkSorted : (permPrf : sorted ~~ orig) -> (ordPrf : OrderedList f sorted) -> Sorted f orig sorted

и говорим, что какая-нибудь функция сортировки, скажем, merge, выдаёт сортированные списки:


mergeSortIsASort : (f : Order a) -> (ftotal : Totality f) -> (xs : List a) -> Sorted f xs (mergeSort f xs)

Доказательство этого занимает строк 100, но на них можно не смотреть, достаточно глазами пробежаться по этому десятку строк, чтобы вообще понять, что мы там делаем и доказываем.

Ну я примерно это и имел в виду.
А если, например, вот вы построили доказательство, что реализация конкретного компилятора соответствует вашему языку, и тут вам приносят еще один компилятор, как сложно будет адаптировать текущее доказательство под него?

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

Нет, язык то тот же самый. Компилятор другой.

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

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

Валидатор, например solidsands.com/supertest

Там же тесты.

Каков язык, таков и валидатор. Доказательство корректности компилятора C++ — задача для Deep Thought, не меньше.
Ну дак предложите не тесты. Хотябы для своего языка. О чем и прошу уже не один комментарий

Для своего языка у меня уже есть (или пишутся) не тесты, и их я тоже упомянул выше.

Я все никак не могу понять, что вы проверяете — язык или компилятор? Это разные вещи

В итоге — и то, и то. Пока занимаюсь только самим языком — вот только пару дней назад про него progress theorem окончательно доказал, сейчас занимаюсь preservation. Потом, когда закончу это, перейду к формализации транслятора.


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

Ну я то спрашивал как раз про компиляторы. Вам вот не нравится, что верификация компиляторов C++ проводится тестами. Вот я и спрашиваю, можно ли написать такой язык, верификация компиляторов которого будет проводится не тестами. (естественно, я понимаю, что для каждого компилятора в отдельности можно написать свое огромное доказательство, вопрос то тут как раз в постановке верификации «на поток»). И почемуто ответ я до сих пор не могу получить

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


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

А почему бы и нет? По крайней мере, это единственное применение, которое я вижу для формализованного языка

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

Разве языки, позволяющие формализовывать разные вещи, не должны сами быть формализованы? Разве реализациям этих языков не требуется формальное доказательство корректности?

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

Гёдель вместе с теоремой о невозможности доказать консистентность арифметики изнутри неё не даёт.


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

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

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


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

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

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

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

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

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

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

Т.е. корректность идриса полагается на корректность идриса?

Я же уже конкретно на этот вопрос (о постановке верификации на поток) ответил раза три — что нет, нельзя.


Правда, похоже, из этого вы делаете вывод, что формальная верификация не полезна и не нужна, и я не могу понять, как вы этот вывод делаете.

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


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

Нет, язык то тот же самый. Компилятор другой.

Ну это проще. У вас уже будет готовая формальная модель языка в таком случае.


в чем же тогда преимущество вашего разрабатываемого яп

У моего ЯП ноль преимуществ, это математическая модель некоторого языка, для которой можно доказать всякие полезные теоремы.


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

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

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

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

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

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

Да, похоже на то. Как понимаю, разработка будет вестись на F*. Насколько F* близка к идрису?
F* чуть хуже, так как там в ядре тайпчекера используется SMT-солвер вместо простой и мелкой системы типов, поэтому доверия ему меньше. Но F* куда ближе к идрису, чем к какой-нибудь джаве.

Там ещё, кстати, активно Lean используют, а это Coq от Microsoft Research.
Если я правильно помню, есть 2 способа проверять формулы: выводом формулы по правилам логики или обычным перебором с оптимизациями. Что используется в F*?

Есть ещё два варианта:


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

Вот в F* как раз используются эти самые эффективные решающие алгоритмы в виде SMT-солвера прям в ядре проверялки типов.


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

Можете ли вы относительно безболезненно верифицировать представленный компиляторы на этот конкретный яп?

Относительно безболезненно в мире верификации вообще ничего не происходит.


Насколько возможно это?

Это возможно. Папир, на который я ссылался где-то выше, ровно про это. Project Everest, на который я ссылался выше, и на который вам дали ссылку снова сейчас, тоже про это.

Относительно безболезненно в мире верификации вообще ничего не происходит.


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

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

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


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


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

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

Не пройдёт валидацию на то, что ноль фруктов является identity.

Почему не усвоил? Может просто не отметил в статье.
Еще можно добавить то, что надо избегать работать в компании/с людьми, у которых тяп-ляп (и так сойдет, этот код у нас издавна и не надо его трогать) поставлен в систему. 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 процентов готов, остались сущие пустяки!".

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

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

Вот у нас тут один такой быстрый (в июне бакалавра по электронике получил) взял Питончик и сказал, что ща быстренько сделает приложение для 3D печати. Итог — потеряли полгода, приложение переписывается с нуля, а быстрый валит из конторы.
Просто у него не было ОПЫТА разработки хоть чего-нибудь большего, чем наколенный скрипт, а он быстро решил, что может всё.
Именно, он решил, узнал и пошел познавать зная причину, а не сидел еще 5 лет думая «не… ну я еще не опытный, это не для меня, пусть спецов ищут и так всю жизнь»
Таког ОПЫТА и не будет если ты не имея его не будешь делать то где он нужен.
Вы просто были местом где этот человек решил что научитсья, ну не вышло, научитсья в другой конторе «завтра», а не когда нибудь «потом», когда будет все знать.
Вы просто были местом где этот человек решил что научитсья, ну не вышло

«Мы любим свою работу, но должны понимать, что решаем проблемы»
У него был шанс научиться делать софт. Он он решил, что уже всё знает.
Да, опыт он получил (надеюсь, хотя бы научился, как не надо делать). Негативный опыт — тоже опыт. Собственно, его проблемы меня не волнуют. Неприятный лживый тип.

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

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

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

У нас как-то с одним товарищем завязалась дискуссия о важности и профите от развития софт-скиллов…


— Ну не знаю, зачем мне софт-скиллы, я вот от ковыряния $hardskill удовольствие получаю и занимаюсь этим добровольно в личное время.
— А мог бы прокачать софт-скиллы и договориться на работе, чтобы $hardskill качать в рабочее время.
— Даже если бы мне разрешили совершенно не относящиеся к работе занятия — зачем это?
— Чтобы в личное время этим не заниматься!

Еще бы добавил.

Каким бы вы круты не были лет через 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. Вы будете учиться всю свою карьеру
этот пункт актуален для всех сфер деятельности
Спорно, чему учится всю жизнь условный продавец в продуктовом магазине или водитель автобуса?
Продавец в условном советском союзе и в пятёрочке в 2020 это две большие разницы.

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

Вежливости, новым, эффективным методам раскладки товара, новым кассовым аппаратам.

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

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