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

Ну незнаю даже, а креативные навыки? Карпатый говорил что LLM не могут решать проблемы, с которыми сталкиваются впервые… Незнаю конечно, с учетом такого огромного увеличивающегося датасета каждый день. Ну вообще, как минимум, все что происходит сейчас демотивируют: одни думают что их обнулили, другие не хотят проф разрабами становиться, ну а третьи херачат какой-то нейрослоп и радуются. Я сам в электрики подумываю перейти, хотя разраб с 10+ лет опыта. Либо какой-то интуитивной сферой, где все очень тяжело формализуется занятся…

Наукой заниматься тоже не ходите - там теперь ИИшка все решает. И на производстве вы тоже не нужны, там роботы заруливают. А нужны будут только белковые генераторы энергии. См. соответствующий эпизод Lexx.

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

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

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

Ну я разраб и как бы тоже с людьми непосредственно работаю, без общения результата нормального не будет, где-то шлифануть, где-то самому исправить после получения обратной связи… Так что не ссать, кто ссыт тот гибнет!)

Ээээ... Смотри, LLM подбирает коэффициенты в твоей системе уравнений. Но порядок системы уравнений выбираешь всё ещё ты.

Не знаю, насчёт творческих, но

причём только в те, которые работают с людьми непосредственно

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

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

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

ну, и как ты «не дашь этот датасет»? у тебя не купят - у другого купят.

я инженер по ФВ. то что ты не понимаешь о чём статья, это понятно. но она об этом. логика такая - если можно верифицировать, то человек (программист) просто не нужен. год назад то что сделали ребята было невозможно по трудозатратам. это годы работы для десятков специалистов по ФВ. ребята сделали за 4 недели командой из 5 человек. заметь, они об этом прямо сказали. с чего бы, да, если статья не об этом?

крупные игроки делают то жже

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

тебе не показалось, мне думается.

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

Ну понятно что хирургия и большой теннис нам не светит. Думаю читательский клуб что-ли организовать…

ну-ну.

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

Вечность пахнет нефтью (c)

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

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

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

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

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

мол все срочно идите в творческие профессии, причём только в те, которые работают с людьми непосредственно, иначе останетесь без работы

С этим и openai 4o справится, этот прекрасный маленький дружелюбный лжец

Ты рассказываешь это человеку который себе на жизнь этой профессией зарабатывает последние лет 10. Я вижу какой ты у мамы умный. Говори ещё.

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

логика такая - если можно верифицировать, то человек (программист) просто не нужен.

и тут же ниже

ребята сделали за 4 недели командой из 5 человек

из 5 человек

Л - логика.

То, что AI позволяет в некоторых случаях очень сильно сократить затраты - да, но это не исключает из процесса человека.

Ну и ладно, я вот мог и не понять, но мой друг claude opus 5.5 тоже, видимо, не понял статью

The article doesn’t support “humans won’t be needed for software development.” It does support a weaker claim, and that weaker claim is the one worth arguing about on LOR.

What the article says

AlphaProof Code is a multi-agent system where AI agents write machine-checked proofs in Lean. It verified the core cryptographic code underlying the Signal protocol, and the proofs go down to the compiled machine code. The headline numbers: the verification took about four weeks, while expert teams historically take years for comparable work, and human reviewers examined about one percent of the codebase. 

Where humans were involved, in DeepMind’s own words

- Deciding what to prove. The article’s own summary is that “human experts work with AI to decide what to prove, and a group of AI agents does it.” Human experts reviewed every specification. 
- Reviewing proofs. The agents flagged areas needing a human second look, and the article says this let experts focus on “where human judgment matters most.” 
- Outside feedback. Signal’s engineers gave feedback on the methodology. 


So DeepMind presents this as human–AI collaboration. It doesn’t claim humans were removed.

Further points against the “no humans” argument

- This was verification, not development. Signal’s code was written by people, along with its security goals and the threat model. The AI proved that existing human-built code meets properties humans chose. That’s a different task from deciding what software should do.
The specification is where the risk is. A proof only shows the code matches its spec. If the spec leaves out an important property, the proof can’t catch that. Writing and approving the specs was exactly the part left to people.
- Only 1% reviewed doesn’t mean only 1% of the trust. The flagged 1% is the hardest part. The rest is checked by Lean, a tool written by humans that the whole result depends on.
- This is a company blog post, not a neutral source. It even contradicts itself on size: the body says over six million lines of Lean, while the meta description and social previews say “over three million lines”. The authors also say scaling the approach “requires continued research.” 
deepmind.google

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

я инженер по ФВ

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

программирование без багов... так говорят ребята в статье

Моя профессия будет только дорожать от таких заблуждений.

просто спроси у своего друга, как ему кажется
1) в чём основная проблема разработки с LLM
2) как ему кажется, если решить основную проблему, то человек в программировании вообще останется нужен? Клод может как то оценить на сколько сократиться участие человека в программировании если LLM будет способен писать без багов

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

Клод тебя просто утешает , это у них по ходу встроенное.

ФВ - формальная верификация в контексте беседы. или я вообще не понимаю о чём ты.

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

Моя профессия будет только дорожать от таких заблуждений.

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

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

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

Ты сам назвался инженером ФВ, кек. Меня не колышет какой тут контекст. Разработка ПО не использует ФВ кроме как в устаревших методологиях.

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

абсолютно точно.

жаль, что нет реакции как кто то крутит у веска..

программирование полностю без багов средствами LLM возможно

Прочитай для начала что такое баг. И чем отличается верификация от валидации.

иди к чёрту.

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

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

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

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

Вот, кстати, почему это НИЧЕГО не значит - ответ по одной бабуйне от свеженького ChatGPT с подпиской:

Да, это моя ошибка. Я предложил синхронный call-process из самого Emacs, который через emacsclient обращается к тому же Emacs. Получилась взаимная блокировка: Emacs ждёт завершения emacsclient, а emacsclient ждёт ответа Emacs.

- и вот так во всём. И нет, не научится.

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

ты пробовал это? или рассуждаешь как слепой о слоне?

Да, гитхабом не надо пользоваться, это сайт микрософта.

У тебя же клод? ты попробуй, запиши что гвоорит заказчик

Ты не поверишь :) Я так и делаю - и кучу времени трачу на то, чтобы получить «понимание» от клода, что действительно нужно и утрясти все детали. И даже во время имплементации он периодически приходит за уточнениями. Т.е. стало лучше и быстрее, но почему-то у меня не получается сидеть, плевать в потолок и нечего не делать. Думать приходится очень много - на самом деле, людям задачу ставить намного проще - это я тебе как лид с 10-летним опытом говорю. Люди будут делать дольше, но задачи им ставить проще.

военка, куда никакой ИИ и близко не подпустят.

В военке его как раз любят. И первая весна ИИ произошла тоже из-за толстых кошельков военки. И эта тоже.

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

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

Формализовать отсутствие ШГ можно?

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

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

ну, не знаю как формализовать, а если ты скормишь клоду пару скриншотов с ШГ, пару без ШГ и объяснишь на что смотреть, то дальше он будет тебе свободно говорить ШГ или не ШГ.

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