Нарешті я переклав вспоміжний матеріал на Lean4 Теренса Тао до його книги Аналіз I.
Для тих хто не знає, це його проект по формалізації його доказів із книги на Lean4. Із одного боку це приклад того як формалізувати існуючу математику для студентів, із іншого там багато спеціально недоведених речей, тому можна буде попрактикуватися в доведенні самостійно. Бо лише практика дає досвід.

Якщо ви помітили що я використовую нестантартну математичну термінологію, я буду дуже вдячний якщо ви вкажете мені на це, щоб я міг це виправити.

Із людськими сторонніми контрібьюторами в Цезіум складно було, але роботи вирішили що ми гідні того щоб мати із нами справу, і сами прийшли до нас https://github.com/ForNeVeR/Cesium/pull/964
Навіть не знаю що із цього вийде

Зробив переклад OWASP Cornucopia українською. якщо хтось може подивитися і дати рекомендації/коментарі, буду вдячний https://github.com/OWASP/cornucopia/pull/2494

Мені не зрозумілий весь меседж який ФСФ хоче донести до людей але виглядає що вони роблять приховану погрозу Антропіку

https://www.fsf.org/blogs/licensing/2026-anthropic-settlement

Все почалося із обговорення такого простого куска кейсу щодо холістичного використання ШІ у середі проджектів серед казахстанського комьюніті ПМ-ів.

При запуску проекту – pre-mortem за 3 години замість 12. На тому ERP-проекті ІІ знайшов ризик, який би команда не придумала: касири в магазинах саботуватимуть нову систему, бо звикли до старої за 8 років. Без цього інсайту проблема спливла б лише за пілота.

Я спочатку був дуже здивований що як так, це доволі простий і відомий ризик. І у чому тут користь від ШІ. Але потім в ході діскусії сам згадав що не так то багато вже команд десь в ентерпрайзі то і знають про типові ризики впроваждення. Ну і там було багато обговорювань.
Але що мені здалося цікавим, що виходить що ШІ зараз через довіру багатьох людей до нього вчить людей доволі відомим речам. Вони звісно могли вчитися самостійно, могли повірити вже досвідченим членам команди які сказали би про ці ризики, але через довіру до ШІ, люди отримують стандартне знання у делікатних речах, які вони можливо би пропустили через суто людяну упередженість.
Багато прикладів коли навіть якщо є в компанії люди які можуть розповісти про ризики, то їх думки можуть бути поглинуті начальством або почути не їх думки, а думки консультантів.
І тут мабуть дійсно ШІ вчить людей вже зараз в таких не оптимальних компаніяї. Це навчання працює через те що люди довіряють ШІ прямо зараз. Так, це дати людям рибу а не вудочку, але якщо люди не хотять рибачити. то це все одне краще ніж не допомогати людям.

О! Я два дні тому дізнався що CrowdIn це платформа для менеджменту локалізацій зроблена українцями!

На мою персональну думку це дуже професіональний інструмент для широкого кола команд, від 1 людини і до великих груп людей. Від мобілок, сайтів, статей і до книг. Дуже широкий спектр. Але що найгарніше це те що вони
- підтримують переклад із редактурою як процес
- мають автоматичну синхронізацію вихідного коду
- підтримують відкритий код

Якось так трапилося що мені вони дуже подобаються. Рекомендую!

Пройшла епоха

https://github.com/TechEmpower/FrameworkBenchmarks/issues/10932

З вибаченнями до Борхеса, я вважаю, що все дослідницьке програмне забезпечення можна класифікувати так:

1. Те, що працює на ноутбуці початкового автора.
2. Те, єдина документація якого — постер з конференції 2009 року.
3. Те, що залежить від бібліотеки, яка залежить від бібліотеки, яка залежить від Python 2.
4. Те, що включене до цієї класифікації.
5. Те, у якого номер версії «final_FINAL_v3_revised_corrected» є коректним.
6. Те, що дає ледь помітно різні результати на Debian і Ubuntu з причин, які ніхто не досліджував.
7. Те, що написане на Fortran і тому є найнадійнішим з усіх.
8. Те, що працює правильно лише тоді, коли вхідний файл містить парну кількість рядків.
9. Те, яке при запуску видає одне число, що цитується у сімнадцяти статтях.
10. Те, яке швидше переписати, ніж зрозуміти.
11. Те, яке переписували чотири рази і воно все ще не завершене.
12. Те, чиї юніт-тести всі проходять, бо тести були написані під наявний результат.
13. Те, чий результат настільки правдоподібний, що його автори не ставили під сумнів його правильність.
14. Те, яке здалеку виглядає підтримуваним.

дякувати тут - https://third-bit.com/2026/03/26/classifying-research-software/

Абстрактні зобовʼязання - кому воно треба.

Зазвичай це те, що прописано в кодексах етичної та професійної поведінки.
Мовляв, так-так-так, це само собою зрозуміло все, перейдімо до прагматичних результатів - скільки це мені принесе клієнтів, на скільки відсотків зростуть мої доходи і т.п.

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

І тут стає особливо помітно, наскільки мало перекладачів усвідомлюють ці начебто абстрактні поняття.

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

"...act in good faith and respect the dignity of the profession..."

Коли усвідомлювати, що не лише права качати можна, а й треба свідомо брати на себе обовʼязки (як от поважати професію) - то і професія щедро тобі віддячить.

Якщо ні, то тоді не варта нарікати, що ти не пройшов через дедалі дрібніше сито реальності.

#insidetheinterpreting #interpretingisneverboring #conferenceinterpreting #професійнаспільнота

Давно я не читав нічого цікавого по педагогіці навчання програмуванню. Ця стаття дуже провокує мене спробувати використовувати ролі змінних для навчання. Замість комірки можна казати що бувають різні сорта комірок і це мабуть непогана інтуїція для початку навчання.

Почитайте і скажіть, які ще типи змінних ви бачили в реальних проектах

https://third-bit.com/2026/03/28/e-bike-for-the-mind/

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

https://kant2002.github.io/en/obfuscators/2026/04/02/how-to-build-obfuscator-part-i.html

https://ochagavia.nl/blog/a-real-world-case-of-property-based-verification/

Мені здається це гарна мотиваційна стаття, вона не розказує як конкретно будувати властивості, і виходячи із того що я бачу по коду це скоріш 1 велика властивість, ніж якийсь набір властивостей, але незважаючи на це стаття показує продвинуті методи валідації системи.

Якщо вважати що будь-яка ШІ-побудована система складна, то подібні техніки цікаві. звісно сам проект супер-крутий - міжпланетарні сітьові взаємодії

Нарешті цікаві розробки в компіляторах. Це звісно про локалізації мов програмування. Мова на корейській


Пісочниця на верцелі https://geul-web.vercel.app/playground

GitHub (MIT): https://github.com/wwoosshh/geul-lang

Не знаю куди написати, тому напишу сюди. Це один із варіантів стратегії ЄС щодо ШІ. Це дуже цікаво як мінімум почитати що одна лоббі група думає про напрямок розвитку

https://europe.mistral.ai/

https://flukeout.github.io/

о! це також прикольна штука для тренування знання СSS селекторів. не вистачає підказок, та посилань на матеріали, але сама гра дуже крута

Трішки ігор. Вирішив підглядіти існуючу ігру де треба відгатати фразу яка зашифрована кодом підстановки.

https://kant2002.github.io/aristocrat/

Думаю буде цікаво і дітям і дорослим

Пісочниця для Пітона онлайн. Можна вчити дітей із телефону

https://dou.ua/forums/topic/58908/

Шикарне відео про те як можна вимірювати надійність архітектури щодо змін в майбутньому. В принципі технікі доволі прості, але мають гарне математичне обгрунтування. Більше того, якщо вирахувати 1 дісципліну генерувати неймовірні події, які можуть поламати бізнес це буде надійно працювати. Звісно я розумію що дуже багато команд буде просто не в змозі це вигадати, і будуть роздувати вимоги. Але мабуть навіть там можна будет розділити принципи на
- вимоги
- ризики
- якась кількість фантастичних ризиків.

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

https://www.youtube.com/watch?v=0wcUG2EV-7E

16 квітня в Ірландії після тяжкої, швидкоплинної хвороби пішов із життя Юрій Олексійович Ющенко — доцент, кандидат фізико‑математичних наук Національного університету «Києво‑Могилянська академія». Він продовжив наукову спадщину своєї матері, відомої української науковиці Катерини Логвинівни Ющенко (Рвачової), працюючи в галузях штучного інтелекту, теорії алгоритмів та логічного програмування.
Мав честь бути особисто знайомим із паном Юрієм. Від нього я дізнався багато цінних історичних фактів про розвиток комп’ютерних технологій в Україні. Окрім викладання, він досліджував науковий спадок своєї матері (зокрема Адресну мову програмування) та інших піонерів галузі. Разом ми консультували розробників емулятора ЕОМ «Київ» з УКУ, що сприяло відродженню цього славетного технічного здобутку в програмному коді. Ми також інформували суспільство про досягнення Катерини Ющенко, ім’я якої тепер носять вулиці у Львові та Кременчуці.
Мої щирі співчуття родині пана Юрія. Світла пам’ять.

Хочу записати свої враження від відвідування воркшопу по верифікації програмного забеспечення за допомогою Lean4. Для мене це було доволі яскрава подія, де я просто був вдячний побачити людей які не лише цим цікавляться, а і працюють в цій сфері. Із прагматики що мене вразило - це те що ніхто хто займається формальною верифікацію не ставлять собі задачі що доводити явно. У них є мета і вони скоріш або формалізують конкретну мету, або беруть готові специфікації написані іншими людьми. Принаймні із цієї точки зору мені зрозуміло чому популярізація цього напрямку доволі слабко працює. Якщо взяти цей підхід, то звісно все встає на місця і всі проблеми і інструменти які будуються цілком зрозумілі.

Дуже приємна спільнота, яка дружньо ставиться до сторонніх людей. А мене не можна назвати прямо членом спільноти звісно. Познайомився із Еміліо Аріасом, який займається популярізацією Лін серед людей. Виглядає що я якось можу трансформувати мої спостереження щодо деяких проблем із онбоардінгом нових людей на Lean.

Також був анонс від групи із назвою Бенефіціарне ШІ що вони будуть вести роботу по формалізації Сігналу в Лін. Цей проект називається Signal Shot (до речі вони шукають людей) і буде мати свій канал в Зуліпі де можна познайомитися із людьми і щось допомогти якщо є бажання.

Із цікавого спостереження що багато хто в комьюніті показував конфігурацію коли люди працюють на расті і верифікують код на Lean. Звісно для растерів не новина, але про С ніхто всерйоз не згадує, лише як код який треба переписати і верифікувати.

Виглядало що робота по F* не дуже гарно рухається на відміну від Lean. Тому деякі проекти типу Hax роблять ставку на експорт в багато мов де можна робити верифікацію.

Чим менша залежність від ГітХабу тим краще. Більше децентралізованих сервісів

https://social.treehouse.systems/@whitequark/116454915873481567