Расстроен ли я? Что вы, я нет! Ну слегка...

Видимо, выхлоп бредогенераторов в разы превосходит всё что, что делает AndreyKl (учитывая его верования в ФВ, неудивительно), ну а то что не все такие как он - он не догадался.

ай ты умничка. маме покажи свой пост, она тебя похвалит тоже.

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

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

просто для уточнения, клод же последний? просто у меня фабл делает аж прям глаза радуются. причём всё, от презентаций до общения с заказчиком. не без участия человека, да. но штука в том что я тебе говорю что «программист как профессия закончился», а ты мне «а общение с заказчиком», а это дело не программиста, а системного аналитика/тимлида. но и тут клод в разы ускоряет решение.

Люди будут делать дольше, но задачи им ставить проще.

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

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

главное найти куда

В смысле, кто-то до сих пор работает программистом? Зачем? Что вы там программируете? Всё, что нужно было написать, уже давно написано.

ты вероятно шутишь...

Иишки довольно хорошо пишут програмсы, сильно быстрее человеков. Топовые делают это нормально порядка года. Какие новые заметные программные продукты появились за год? Не густо, я только 0-day эксплойты могу вспомнить. Остальной эффект от ИИ - мелкие улучшения или клонирования. И не потому что они не могут. А потому что сколько-нибудь широких нужных ТЗ, под которые нет программы - никто не придумал. Всё на что придумано нормальное ТЗ - написано. А новые ТЗ придумываются довольно медленно

Карпатый говорил

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

Аргумент, конечно. Но я попробую поспорить: сколь-нибудь широких нужных ТЗ под которые нет программы никто не придумывает лет 10-20 как, но программисты начали терять работу только в «эпоху ИИ», т.е. пару лет как. Соотвественно они были нужны и сейчас эту работу делают программисты + ИИ. Так вот я утверждаю что в течение пары лет из этой связки программисты выпадут совсем (в статистическом смысле, конечно).

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

А какие 5 лет назад до ИИ? Рынок давно перенасыщен, никаких вау фотошопов больше никогда не будет, время стремительного роста прикладного софта осталось в девяностых и начале нулевых.

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

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

За каждой LLM стоит человек, который дает ей задачи? А почему бы не рассмотреть альтернативный сценарий: Может быть вместо замены программиста на LLM мы получим замену на связку программист+LLM? Производительность труда многократно возрастет, а планка качества программ поднимется на порядок.

потому что LLM дешевле и работает в сотни раз быстрее программиста. Там где было 100 программистов, будет пара программистов + LLM. просто потому что столько программистов не будет нужно.

потому что LLM дешевле и работает в сотни раз быстрее программиста. Там где было 100 программистов, будет пара программистов + LLM. просто потому что столько программистов не будет нужно.

Так работа программиста чаще всего не в написании кода, а в выдаче «решения». Как он его получил никого не волновало и раньше. Огромными частями работы было понять что вообще требуется и что ещё сломается и с кем надо говориться, чтобы что-то перепроверить или куда-то задеплоить.

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

хорошая аналогия, но два аргумента:

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

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

Так работа программиста чаще всего не в написании кода, а в выдаче «решения». Как он его получил никого не волновало и раньше.

не скажи. это лишь в некотором смысле - не интересовало. на деле платить ЗП надо. И если один программист может теперь делать то что делали 10-100, то 9-99 уволят. это так работало и работать будет во всех сферах. не вижу почему программирование должно стать исключением из этого правила.

Основной скилл программиста в эпоху LLM является код-ревью.

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

просто потому что столько программистов не будет нужно.

Значит остальные 98 программистов совместно с LLM создадут другой продукт в другом месте. У нас разве вся работа в мире переделана?

Значит остальные 98 программистов совместно с LLM создадут другой продукт в другом месте. У нас разве вся работа в мире переделана?

не вся конечно переделана... вон на СВО ждут желающих.

Если серьёзно, загляни в магазины игр - там тучи игр и плагинов висят. весьма неплохих, но никому не нужных, слишком много их понаделали с ИИ.

1. Дело не в фичах, а в количестве бизнесов. Программисты не создавали никогда в последнее время новые фичи, они доводили до рабочего состояния какие-то продукты. Число нужных программистов определялось только числом стартапов-бизнесов. Ну например поисковиков до гугла было не один. А до телеграма мессенджеров было тоже. И после телеграма создавали мессенджеры. Принципиально новых гениальных фич там особо никто не изобретал. Точнее так: степень оригинальности фичи определялась не прорывным мозгом программиста, а целями которые ставил стартап/бизнес/владелец ну и ещё определялось характером собранной команды разработчиков. Программистов сейчас надо меньше просто потому, что деньги в мире свободные кончаются грубо говоря. Кредиты везде дорогие, стартапы пилят меньше. Хвост от бума доткомов и бума стартапов уже завершается: идеи исчерпываются, приложения примерно для всего чего можно было - написали. Первый айфон вышел сравнительно недавно, лет 20 назад, вот за 20 лет эту тему более-менее и «освоили», да и то ещё немного есть потенциала. Программисты не стали не нужны совсем, спрос на хардкорных чуваков понимающих как работает внутри микросхема или HFT-трейдинг-робот или там планировщик ядра всегда будет, потому что на этих системах мир держится. Как это всё работает и нейронка понимает, но у неё есть неприятная для бизнеса черта: ей вообще пофиг на жизнь, то есть пока ты ей явно в промпте не напишешь на что ещё неявно влияет твой код, то она может и не догадаться, она какбэ не работает и не живёт в данном банке и его бизнес-процессах и может не до конца осознавать конкретные риски каких-нибудь изменений.

2. Код писался достаточно высокоуровневый, программисты уже редко понимали что там в реальном железе происходило. Дошло уже до того, как мы знаем, что .apk - файл с приложением ссаного небольшого банка весило 200 мегабайт: то есть они уже настолько ничего не понимали что пишут, что жесть. Так это же ничем от промптов не отличается вообще. Любой там C++20 с шаблонами, фабриками комбинаторов абстракторов-аттракторов-итераторов - это такой язык промптов в компилятор по-сути. Вы же знаете сколько C++ софтина компилируется? Так это ж вообще жесть, всё как с нейронкой: промпт написал и оно там думает о чём-то, оптимизирует. Это было в десятки-сотни раз быстрее чем клепать как деды на ассемблере или даже иногда на сишечке (например шаблоны С++ позволяют пейсать обобщённый код для любых типов, что на сишечке чуть менее чем достижимо в принципе). Да, теперь LLM полностью пишут код. Но это вообще ничего не меняет: этот код надо куда-то ещё деплоить, проектировать как он там с чем будет взаимодействовать: стыка с живыми людьми, определяющими спрос на этот код сколько было, столько и осталось. Я и раньше никогда в жизни код по 8 часов в день непрерывно не пейсал, всё больше ходил титьки мял вокруг него. Так и сейчас всё точно так же. Только теперь я могу код качественнее высирать через LLM и больше тестов писать. Безопасность и качество вырастет. Ну и говнокода наплодят в 1000 раз больше чем раньше, .APK будут весить по 4 гигабайта в некоторых случаях. У меня сейчас кода столько же получается, просто багов поменьше и тестов побольше генерится и больше времени ютуб на работке посмотреть с кофейком. Важно: код, который высрала нейронка и который никто не понял из программистов - никуда не едет всё равно. В код-ревью всё упирается как и раньше. Посадить 10 гениальных агентов на ревью и доверить всё им никто не собирается в серьёзных местах: в больших поисковиках, соцсетях, видеохостингах и банках…

Если серьёзно, загляни в магазины игр - там тучи игр и плагинов висят. весьма неплохих, но никому не нужных, слишком много их понаделали с ИИ.

Если программисты из-за LLM настолько не знают, чем себя занять, пусть они сделают нечто уровня GTA VI максимально применив всевозможные достижений нейросетей. Наделали то в основном нейро-мусор и очередную «три в ряд».

не скажи. это лишь в некотором смысле - не интересовало. на деле платить ЗП надо. И если один программист может теперь делать то что делали 10-100, то 9-99 уволят. это так работало и работать будет во всех сферах. не вижу почему программирование должно стать исключением из этого правила.

Так всё от экономики просто зависит. Сейчас ЗП не платят и увольняют не потому, что можно найти одного эффективного программиста вместо 10 старых, а потому что производить этот самый продукт уже никому не нужно. Бизнесов нет, стартапов нет, везде пессимистические настроения и ожидания мировых войн. Если бы было всё хорошо в экономике мировой, то все программисты бы остались, просто были бы снабжены нейроночками и продуктов плодили бы в 10 раз больше.

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

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

Программисты не стали не нужны совсем, спрос на хардкорных чуваков понимающих как работает внутри микросхема или HFT-трейдинг-робот или там планировщик ядра всегда будет, потому что на этих системах мир держится.

именно поэтому я и говорю «статистически». или «практически».

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

писать будут в основном «тёмные фабрики», это уже вырисовывается.

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

да, останутся, но сколько? 1 из 100? можно ли это назвать «останутся»?

ну, это то что могут «программисты» на короткой дистанции. чтобы делать что то уровня ГТА нужны деньги. да и ГТА уже есть.

по остальным пунктам не согласен. рынок , похоже, насыщен, соотвественно бизнес вкладывать деньги в разработку софта уже так отчаянно не будет. писать будут в основном «тёмные фабрики», это уже вырисовывается. как токарей не нужно больше чем их есть, так и программистов не нужно больше чем их буде нужно через год два. да, останутся, но сколько? 1 из 100? можно ли это назвать «останутся»?

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

Если бы было всё хорошо в экономике мировой, то все программисты бы остались, просто были бы снабжены нейроночками и продуктов плодили бы в 10 раз больше.

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

вы оптимист.

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

они были крайне дорогими. а нейронки сейчас пишут пруфы в rocq/lean, мне не нейронка сказала - мне нейронка пруф написала, а rocq проверил. это фундаментально.

они были крайне дорогими. а нейронки сейчас пишут пруфы в rocq/lean, мне не нейронка сказала - мне нейронка пруф написала, а rocq проверил. это фундаментально.

Так тебе надо чтобы кто-то ещё верифицировал, что нейронка правильно выразила условный C++ код в условный верификаторный язык.

А у кого-то есть пруфы что программы, которые формально верифицированы они это, те самые которые верифицированы?

они были крайне дорогими. а нейронки сейчас пишут пруфы в rocq/lean, мне не нейронка сказала - мне нейронка пруф написала, а rocq проверил. это фундаментально.

Вообще эти все формальные верификации программ мало где нужны: только в гипервизоре каком-нибудь, в микроядре, где-то в очень узкой области. У всего остального концепция «пускай падает, пускай ломают и хакают - оно контейнеризовано». Я вот чё-то слышал про то, что какой-то там гипервизор в айфоне так верифицирован, чтобы ни одна скотина не смогла получить такого главного рута, который бы мог прошивку модема например поменять и из всех айфонов в мире ботнет сделать, отключив их от apple навсегда. Щас достаточно один раз из linux ядра все баги вычистить, которые отвечают за проламывание namespaces/cgroups и всё, пускай хакеры рута получают - рут там липовый.

Мне кажется, что программисты могли бы доучиться в инженерию и заняться более наукоемкими вещами. В России, например, нет собственных нейростимуляторов. И даже зарубежные далеки от совершенства, причем не только «железячного», но и программного. Работа с оборудованием - это ведь, помимо прочего, и задачи более разнообразные, и LLM пока что далека от тех профессий, где нужно что-то делать физически. Сейчас даже кофеварку без участия программиста не сделать.

Но раз уж тут затронули вопрос экономики. А где сейчас не кризис? Сейчас никому не живется легко.

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

А верификация, на секунду, была в 4-5 раз дороже написания, это минимум.

При чём тут спеки я не понял. Спека - это ж какая-то формальная фигня, а речь вообще не про это. Мы и спеки-то не пишем нифига например. Их никто не читает потому что, как и документацию. Чисто на опыте поцоны. Писать код по спеке - это уныло и скучно, я в таких местах не пытался работать. Раньше таких презрительно называли «кодер» а не гордо «разработчик») Это как «админ» и «девопс» наверное…

А верификация, на секунду, была в 4-5 раз дороже написания, это минимум.

Так она и сейчас дороже. Цена верификации же состоит в составлении спеки и прогоне на этой спеке спец-сертифицированных алгоритмов-доказаторов. И тут два нюанса: доверие к правильности составления спеки и доверие к правильности работы алгоритмов-доказаторов - это уже и есть стык человек-машина. То есть само по себе понятие «доверие» - это деньги, юридические риски, бизнес, бабло, «вывоз в лес в багажнике», просёр полимеров, разборки, войны. Это уже прямо живые люди и ресурсы. Слишком образно выражаюсь, хочу сказать что природа/суть/свойство самого понятия «верификация» жесточайше опирается на «вот эти очкарики в третьем поколении, которые жопу поставили на кон, мамой клянутся, что это верно». Никто не будет верить нейронке, надо чтобы живое мясо подпись поставило, потому что его квартиру потом продавать с торгов будут если он провафлится, а у нейронки взять нечего. Незнаю как точнее выразиться, плохо мозг уже работает.

Так тебе надо чтобы кто-то ещё верифицировал, что нейронка правильно выразила условный C++ код в условный верификаторный язык.

тут две проблемы, я просто не понял о которой ты:

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

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

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

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

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

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

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

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


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

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

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

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

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

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

ему для этого программист нужен.

мысль в том что там где было нужно 100 программистов, теперь будет нужен 1.

Я ещё одну мысль вспомнил: был такой фильм Generation П (ещё книга была, но я тупой для книг, только фильмы смотрю). Так вот, там был такой диалог:

-- вот ты пишешь "коллективное бессознательное", а сам знаешь что это такое?
-- нуууу... на уровне коллективного бессознательного...
-- А не боишься, что есть кто-то, кто энает отчётливо?

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

мысль в том что там где было нужно 100 программистов, теперь будет нужен 1.

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

Мне вот кажется, что частных самолётов через океан летает катастрофически маловато. На подводных лодках в туристических целях тоже мало кто ходит или на своих яхтах. Есть же куда расти явно.

Есть главный п***бол планеты подобного рода - Илон Маск - космический корабль в каждый дом - вот хотелось бы к нему духовно присоединиться в данном посте. Надо что-то придумывать, что надо занести в каждый дом и что нужно каждому, а мы тут титьки мнём. Африка, огромный континент, всё ещё плохо освоен и полит водой, пресной воды мало для этого запилено, атомных реакторов маловато сделано. А зачем тут программисты: а ведь всё это автоматизировать надо, никто не готов уже к тому, что тачка при парковке сама не затормозит.

угу... только это так не работает, см. пример с промышленной революцией.

угу… только это так не работает, см. пример с промышленной революцией.

Ну всё-таки как-то это двигает экономику вперёд? Производство чего-то всё же удешевляется. Ну да, какие-то люди не вписываются в рынок. Так и в 2018 году, когда нейроночки код не писали, тоже была ситуация «IT-шники богачи, элита, завидую им, вот бы тоже вкатиться в IT». То есть и тогда был привелегированный класс, кому повезло в большие деньги зарабатывать на давлении кнопок. Так и с нейроночками - этот 1 из 100 оставшихся будет представлять собой всё ту же ситуацию. Справедливости как не было, так и нет. Я ещё помню было дело, когда flash-аниматоров на мороз массово выкинули. А ещё было дело Delphi-разрабов кикнули. Ещё виндузятников кикали, когда на linux всё переезжало на серверах постоянно и был отказ от MS-серверов и MSSql в 2022 году. Да много раз это уже происходило, всегда будет масса не вписавшихся в рыночек. «Попал в вольчью стаю - не **бёшь так бегай» и «в большое семье не щёлкай клювом» и «кто первый встал, того и тапки» всё ещё рабочие поговорки)

и вот так во всём.

Неделю назад писал нечто для микроконтроллера (хобби) вместе с deepseek, разговаривая с ним в чате. Он мне доказывал что одним таймером для двух разных дел обойтись нельзя. Я его переспорил, ткнув носем в то как это можно сделать. Он признал что был не прав и меня похвалил:) И написал нужный кусок сишного исходника по моим предельно четким указаниям абсолютно правильно. И это мне понравилось. Я теперь думаю о более высоких материях, а не о том какие биты как выставить в регистрах настройки этого таймера. Я ему сказал как должен быть настроен таймер - он написал и биты не перепутал. Сказал ему что должно быть в обработчике прерывания от таймера - и он это написал. Ну и так далее - я указываю что делать, он делает. И чаще всего хорошо делает,хотя и не абсолютно всегда.

формальная верификация позволяет полностью убрать ошибки?

Вопрос только в том, ошибки какого уровня она позволяет убрать. Уверен что не те, которые связаны с взаимонепониманием с заказчиком и тем более с тем что заказчик сам толком не знает чего же он хочет. Про это хорошая серия картинок есть: https://workspace.ru/upload/medialibrary/097/1.png

А так-то да, вон совсем простые синтаксические ошибки ловит даже просто компилятор, без всякого ИИ. Ошибки - они очень разные бывают.

Всё, что нужно было написать, уже давно написано.

Согласен что для десктопа ситуация действительно близка к этому. Нового в таких количествах как раньше уже писать не придется. А вот в микроконтроллерах увы - там почти каждая задача достаточно уникальна потому что МК обычно более плотно взаимодействуют с физической реальностью через датчики и управляемые ими исполнительные механизмы. А реальность - штука сильно сложная и разнообразная в своих вывертах. Да, ИИ безусловно помогает, но не заменяет человека. Когда-то в дискуссиях на форумах, типа этого, программистов делили на собственно программистов и «кодеров», способных только наколотить тривиальный,пусть и объемный, код по готовому подробному техзаданию. Так вот ИИ неплохо заменяет вторых, но не первых. А основная работа программиста - вовсе не в скоростном наборе кода, а в обдумывании что же именно должно быть написано.

столько программистов не будет нужно.

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

Можете не верить, но это из за меня. Я когда то даже гербалайф развалил. Куда я ни приду, скоро это умрет. 3,5 года назад я взялся за программирование. Даже не шибко удивлен.