Хроники Попокалипсиса

[vit_r]

Angeline 2025

Правильность и Адекватность

[ itSotWC::CoD ]

Из всех грустных и беспросветных тем моего богатого общения с представителями племени кнопкодавов-программистов самая прискорбная и до безнадёжности каменной стены непробиваемая была тема верификации и валидации. (Verification and Validation)

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

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

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

С этим у дрессировщиков лул, яв, питонов, рубей, скал и хаскелей проблем нет.

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

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

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

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

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

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

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

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

Всё нормально: быстрое распространение, массовое заражение, тяжёлые случаи вплоть до реанимации.

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

Беня, кстати, доехал до суда -- судьи взяли самоотвод и смыслись -- и мимоходом сообщил собравшимся журналистам -- не отпускать же с пустыми руками --, что на Миндича в Израиле было совершено покушение, но преступники ломились не в тот дом и ранена чужая домработница.

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

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

Закончим зачётной новостью, пусть и на уровне слухов.

https://t.me/crescentscroissants/7777 (Война и мир на Ближнем Востоке, Дина Лиснянская, 2025-12-11):

Reuters: Белый дом рассматривает возможность объявления БАПОР (UNRWA) иностранной террористической организацией и наложения персональных санкций на его руководство.

Знаете, я могу сказать только одно: Если Вам не нравится Трамп, Вы на неправильной стороне.

Comments

[straktor]

> Бредогенераторы и люд чат-гопотящий пришли в нашу жизнь не просто так.
> Это всё было подготовлено десятилетиями развития культуры правильности на уровне "так сойдёт"

а причём тут вступление про кнопкодавов, которым не дали спеку на ГУИ и потом удивляются, что сделано без спеки

ЛЛМы принципиально не реализуют аристотелевский/математический логический вывод, а выполняют припоминание и рассуждения "накуренного альцгеймерника" по образцу
иногда результат получается хорошим
как минимум, не таскается грамматический аппарат, а падежи-рода-склонения болван очень складно пишет
имхо это уже достижение

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

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

и такого фуфла (про того же сотону трампа) люди генерят мегабайтами ежедневно

[vit_r]

> а причём тут вступление про кнопкодавов

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

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

(frozen)

[straktor]

> Задача сочинения "Ленин и Музы" -- не прославить Ленина, а помочь детям освоить работу с терминами.

"садись, Иванов, двойка!" :)
ну какие в 8 лет термины
смысл был ритуальный, насадить основанное на страхе почитание фигуры божества, разместить в центре внимания
писали мы откровенное фуфло, нескладухи и выдумки, и получали свои четвёрки за лояльность
тётка была реально чокнутой на коммунизме

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

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

есть встречное предложение по виноватым -- журналисты, политики, чиновники, бизнес, учителя
люди сталкиваются с ними в материальном и нематериальном мире примерно 90% случаев
2% за программистов я вполне допускаю

вот мы прямо сейчас пользуемся продуктом программистов -- браузером, сайтом, ОС
работает же, общаемся

[moneo1337]

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

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

[vit_r]

У программистов всегда много свежих идей. А когда они иссякают, программисты начинают менять имена переменных и с языка на язык переписывать.

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

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

[straktor]

> времена, когда доказательное программирование еще было свежей идеей

Барбара Лисков с языком https://en.wikipedia.org/wiki/CLU_(programming_language) это 1975 год
и там логический вывод ЕМНИП "вперёд"
Бертран Мейер с https://en.wikipedia.org/wiki/Eiffel_(programming_language) тем же ходом
видел я ещё МГУ-мехмат статью с ... рапирой? Ершол?, у них дедукция назад шла

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

в какой-то степени что-то принимается в индустрию: https://en.wikipedia.org/wiki/Design_by_contract
люди этого не любят, не хотят знать и сопротивляются -- например Java checked exception миллениалсы обосрали "херня непонятная, бумеры с ума сошли"

как минимум, "в поле" никто сейчас не пишет "контрактов" по причинам экономическим, потому что пока напишешь, 10 раз сменится руководство, бизнес, договора и организация
каждые 2 года меняют "платформу" бизнеса, каждые 5 лет -- технологическую/поставщиков
думали, ну будет оракл и сап, лет на 20 хватит
информатика -- отчеты
потом обнаруживается, что они каждый хотят по миллиону евро в год, а можно то же иметь за 50К
сейчас даже юнит тесты: сегодня написал, через год вся система выключается -- зачем было мозг сушить

вот компиляторы и ОС да, там контрактам место

[chaource]

Послѣ 1980 года наша цивилизацiя перестала генерировать новыя идеи. Не было никакихъ новыхъ изобрѣтенiй или продвиженiя впередъ, до сихъ поръ пережевываемъ все, придуманное тогда.

Лисковъ, Мейеръ - зря потратили время. Продвигали ООП, не понимая, что это такое и не руководствуясь теорiей типовъ. (Теорiя типовъ тоже уже была придумана въ 70-е годы.)

Напримѣръ, "принципъ подстановки Лисковъ" это просто плохо сформулированная, расплывчатая мура, которой никто не пользуется и не понимаетъ, потому что этотъ "принципъ" нельзя понять. Если попытаться его сформулировать четко, получится либо тавтологiя ("значенiя типа Т должны обладать всѣми свойствами, присущими значенiямъ типа Т"), либо явно невѣрное утвержденiе ("результаты программы останутся безъ измѣненiй, если въ любомъ мѣстѣ вмѣсто какой-либо перемѣнной подставить какую-либо другую перемѣнную того же типа").

Все, что они сдѣлали, давно и заслуженно забыто.

[chaource]

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

[anonim_legion]

С нынешними вычислительными мощностями доказывать можно очень многое, только никто этим не занимается.

[uselessextras]

Ну почему же никто. Некоторые для себя открывают: https://aws.amazon.com/blogs/security/an-unexpected-discovery-automated-reasoning-often-makes-systems-more-efficient-and-easier-to-maintain/

[chaource]

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

А программистъ въ современномъ пониманiи - это какъ секретарша, которая возомнила, что можетъ сама сочинять квартальный отчетъ, не понимая, что и для кого тамъ пишется. И для форматированiя отчета и рисованiя рамочекъ придумываетъ какiя-то лекала и формочки изъ пластмассы, думая, что это "инженерная технологiя написанiя отчетовъ".

[vit_r]

С самого начала программирование обслуживало бизнес и бухгалтерию.

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

А потом программистов начали учить программисты и всё превратилось в то, что имеем.

[chaource]

https://www.cs.ox.ac.uk/people/jeremy.gibbons/wg21/meeting58/

Вотъ кстати. Уже въ 2004 году оказалось, что ни математика, ни логика программистамъ не нужна никакая. Университеты исключили этотъ матерiалъ изъ курсовъ информатики.

Some Bachelor programmes in Computer Science for engineering students contain no logic and no mathematics of programming. "No" is not a hyperbole but is to be taken literally. This omission of essential fundamental material is due to the pressure of including more material that is directly job-related as early as possible in the curriculum. Initially, there were promises to compensate for this deficiency in the Masters programmes, but recently approved proposals indicate that these promises will often not materialize. Arguments typically given are that "the mathematics of programming is for pure scientists, not engineers", and that "our engineering students find it too abstract and do not like it".

[straktor]

> секретарша, которая возомнила, что можетъ сама сочинять квартальный отчетъ, не понимая, что и для кого тамъ пишется

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

наверное, вокруг них стоят программисты и бьют палками, когда те пытаются?

[(Anonymous)]

>сообщил, что на Миндича в Израиле было совершено покушение, но преступники ломились не в тот дом и ранена чужая домработница

очень хорошо! я считаю, что всегда нужно так говорить.

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

Ваша критика поверхностна

[(Anonymous)]

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

[vit_r]

В детский сад провели интернет.

Качество нельзя прибавить к имеющемуся продукту. Это фундаментальное ограничение.

Не говоря о том, что остальное тоже к делу не относится.

[(Anonymous)]

Я часто замечал, что многие образованые и умные люди, вдруг в какой-то сфере не могут увидеть проблему "out of the box". Причиной тому обычно является инерция, но иногда бывают и более интересны причины - не буду спекулировать. Кроворукого программиста может исправить строгий менеджер. Ленивого инженера может вылечить пинок под зад. Косяки языковой модели, может исправит другая модель "sufficiently grounded in reality". Я упрощаю - реально работающие схемы несколько сложнее, но это основной принцип.Качество нельзя прибавить к имеющемуся продукту. Но можно добавить его извне.

[anonim_legion]

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

Есть там требования и на цвет, и на форму. Только говно. И проект говно, и заказчик говно, и сама контора говно. Сходите вот в ProcessQ поработать.

[vit_r]

Естественно, и с этим я сталкивался.

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

[anonim_legion]

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

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

И ещё, из больших проектов. Вот скажем, есть некая сущность на стороне одного внешнего сервиса. В сущности имеется 180 полей, они именованные и как-то по-уебански (извините). Чтобы не видеть этого уебанства на стороне бэкенда мы заводим свою сущность с именами и маппинг между внешним сервисом и нашей моделью. Затем мы отдаём эту сущность в UI, на фронтенд, а там имён должно быть два - внутреннее в коде и внешнее в интерфейсе, понятное уже пользователю, максимально не-уебанское.

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

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

Если Вам не нравится Трамп, Вы на неправильной стороне.

[(Anonymous)]

Q-silver

При всем богатстве выбора - стороны всего две: ворюги и кровопийцы. И они обе неправильные.

Правильным может быть место на той или иной стороне.

Вот топить за кровопийц из Швейцарии (или за ворюг - из Канады) - это хорошее, правильное место.

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

[vit_r]

Русачкам не нравится признавать, что живут в дерьме.

Потому постоянно твердят, что кругом дерьмо.

Что дерьмо всегда.

И нет ничего кроме дерьма.

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

[dresden23]

Верификация и валидация присутствуют в современной индустрии, правда в весьма специфических областях. Когда надо сделать контроллер памяти для современного мобильного процессора, то там EAL6+ и никто не отвертится от Thales или подобного сертифицирующего центра. Когда нужно микроядро с предсказуемыми таймингами, то там целый процесс построен от словесной спецификации до формальной модели. Когда нужна проверка формальной спецификации weak memory на GPU, то над этим работают ведущие мировые лаборатории, накручивая сверху дополнительно слои автоматической валидации. Правда стоит это все соответствующих денег, поэтому и редко используется; я сам работаю над валидацией моделей памяти, раньше работал над детерминированным воспроизведением конкурентных программ (deterministic record & replay).

Чатгопота же в умных руках полезный инструмент. Иногда ощущается как переход с ручного фрезерного станка на 7-координатный обрабатывающий центр. Другое дело что надо знать текущие границы применимости этого инструмента.

[vit_r]

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

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

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