Статті

  • Шаблони використання LLM - Шаблон нескінченної генерації

    Це сьома стаття стаття із серії яка описує шаблони будування запитів до LLM систем. Інші статті в серії

    Шаблон нескінченної генерації

    Намір і контекст

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

    Мотивація

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

  • Шаблони використання LLM - Шаблон список фактів для перевірки

    Це сьома стаття стаття із серії яка описує шаблони будування запитів до LLM систем. Інші статті в серії

    Шаблон список фактів для перевірки

    Намір і контекст

    Намір цього шаблону полягає в тому, щоб гарантувати, що велика мовна модель (LLM) виводить список фактів, які присутні у відповіді та становлять важливу частину тверджень у ній. Цей список фактів допомагає користувачу зрозуміти, на яких фактах бо припущеннях ґрунтується відповідь. Користувач може потім провести відповідну перевірку цих фактів або припущень, щоб підтвердити достовірність відповіді.

    Мотивація

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

  • Що працює (а що ні) при продажу формальних методів!

    Орігінальна стаття Майка Додса від 8 травня 2025 року про те що допомогає продавати формальні методи для мене дуже інтимна, так як вона говорить про дуже делікатні і важливі речі - як розмовляти про важливість формальних методів. Тому питання - перекладати, чи не перекладати для мене взагалі не стояло.

    Ця стаття розпочала своє життя як доповідь, яку я провів наприкінці 2024 року.

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

  • Побрехенькі про авіацію у які вірять програмісти

    Це переклад статті з 2025 року про неявні припущення які робили програмісти при праці в авіації.

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

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

  • Побрехенькі про імена у які вірять програмісти

    Це переклад доволі старої і дуже відомої статті з 2010 року про неявні припущення які роблять програмісти при праці із іменами.

    Сьогодні Джон Ґрем-Каммінґ написав статтю, в якій поскаржився на те, що комп’ютерна система, з якою він працював, визначила його прізвище як таке, що містить неприпустимі символи. Звісно, це не так - адже будь-що, що людина називає своїм іменем, за визначенням є правильним способом її ідентифікації. Ця ситуація закономірно обурила Джона, і він має на це повне право, бо імена - це основа нашої ідентичності, майже за визначенням.

  • Шаблони використання LLM - Шаблон когнітивного верифікатора

    Це сьома стаття стаття із серії яка описує шаблони будування запитів до LLM систем. Інші статті в серії

    Шаблон альтернативні підходи

    Намір і контекст

    Дослідниками описано, що LLM часто можуть думати краще, якщо питання розділено на додаткові запитання, які дають відповіді, об’єднані в загальну відповідь на початкове запитання. Намір шаблону полягає в тому, щоб змусити LLM завжди ділити питання на додаткові запитання, які можна використовувати для надання кращої відповіді на вихідне запитання.

    Мотивація

    У шаблону когнітивного верифікатора є подвійна мотивація:

    • Люди можуть спочатку ставити запитання занадто високого рівня, щоб дати конкретну відповідь, без залучення додаткових уточнювань, через незнайомість користувача із доменом, лінь у швидкому введенні або невпевненість у правильному формулюванні запитання.
    • Дослідження показали, що LLM часто можуть працювати краще, якщо використовувати запитання, яке підрозділяється на окремі питання.
  • Simple use case for property based testing

    Here we go property-based testing. It’s usually topic which does not have too much discussion on the Internet, and when it is discussed there not much practical aspects to it. It’s relatively well known that you should wrote your invariants and test agains them. This is all fine, but does not give you idea about what exactly these properties of your models are.

    So here our problem. The path normalization. This is art of conversion of paths road/path/../to/hell/ to road/to/hell, or skip/me/./if/you/can to skip/me/if/you/can, or ../../../only/forward/no/backwards. Basically simplification of paths. That can be very tricky business. For example, ././test is just test, or /../some/ is really wrong path, but we have to leave it as is because it appear as absolute path.

  • Думки про безпеку аплікацій

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

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

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

  • Шаблони використання LLM - Шаблон альтернативні підходи

    Це шоста стаття стаття із серії яка описує шаблони будування запитів до LLM систем. Інші статті в серії

    Шаблон альтернативні підходи

    Намір і контекст

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

    Мотивація

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

  • OpenWebIndex - Европейський індекс вебу

    У вересні 2022 року партнери розпочали реалізацію проєкту ЄС OpenWebSearch.eu — першого проєкту, який ЄС профінансував для запуску незалежного веб-пошуку.

    Проєкт виник як відповідь на занепокоєння ЕС щодо дисбалансу на ринку пошукових систем. Веб-пошук є основою цифрової економіки, але він перебуває під контролем обмеженої кількох гравців, таких як Google, Microsoft, Baidu або Yandex, які всі знаходяться за межами ЕС. Таким чином, інформація як суспільне благо, з вільним, неупередженим і прозорим доступом, більше не знаходиться під контролем европейского суспільства. Цей дисбаланс становить загрозу для демократії в межах ЕС та обмежує інноваційний потенціал дослідницького простору та економіки самого ЕС. Через це ЕС вирішив проінвестувати в розвиток незалежної, більш децентралізованої інфраструктури для пошуку в мережі Інтернет.

  • Мексика үкіметінде ашық кодты қолдану тәжірибесі

    Бұл мақаланың аудармасы LWN.NET сайтынан.

    Ашық бастапқы кодты бағдарламалық қамтамасыз етуді, үкіметтің бағдарламаны қабылдағаны әртүрлі жетістіктер мен сәтсіздіктерге ұшырады. Ашық код айқын таңдау сияқты көрінгенімен, үкіметтер түрлі себептермен еркін және ашық бастапқы кодты бағдарламалық қамтамасыз етуді (FOSS) қабылдауға күтпеген қарсылық көрсетуі мүмкін. Федерико Гонсалес Уэйт SCALE 22x шарасында Open Government конференциясында өзінің Мексика үкіметімен жұмыс тәжірибесін баяндады. Ол бірнеше жобаларды басқарды, олардың мақсаты меншік құқығындағы, жиі қанаушылық сипаттағы бағдарламалық компаниялардан көшу болатын, кейбір табыстармен және сәтсіздіктермен.

    Гонсалес Уэйт өзінің мексикалық/киви екенін айтты ("біздей адамдар көп емес", деді ол ұялып), және Мексика үкіметінде тоғыз немесе он жыл жоғары лауазымдарда жұмыс істегенін айтты, "ашық кодты енгізуді ілгерілеткен". Ол, басқалармен қатар, Сыртқы істер министрлігінің CTO-сы болды; "Бүгінде мексикалықтардың электронды төлқұжаттары бар болса, бұл менің жұмысымның арқасы". Бұл оның басқарған жобаларының бірі болды, және оның бір бөлігі ашық бастапқы кодты бағдарламалық қамтамасыз етумен жасалды, бұл көпшілікті таң қалдырғанын айтты. Ол сондай-ақ президент Андрес Мануэль Лопес Обрадор кезіндегі ұлттық стратегия офисінде жұмыс істеді және кейінірек Мексиканың Ұлттық зерттеулер мен инновациялар орталығының бас директоры болды.

    Барлық қызметтерінде ол үкіметте ашық кодты қолдануды қолдады; осындай ауқымда өзгеріс енгізу әрқашан оңай емес, деп атап өтті ол. Жақында президент ауысқаннан кейін (Клаудия Шейнбаумға) ол үкіметтен кетті және қазір "адамдарға өздерінің ашық кодқа көшуін жүзеге асыруға көмектеседі", әрі жаңа негізгі тенденцияларды бақылап отыр. Ол сұрақтарға соңында жауап беретінін айтты, бірақ кейбір сұрақтарға құпиялық міндеттемелері себебінен жауап бере алмауы мүмкін, дегенмен "ол мемлекеттік қызметкер болмағандықтан, еркін сөйлеу мүмкіндігі көбірек" екенін атап өтті.

  • MagicMapper: The fork of AutoMapper

    Recent changes in the AutoMapper license, and the waves which this send across .NET chats and subreddits make me think. Why even look for alternatives to AutoMapper? I really have erratic feelings about that and it rubs me wrong way. AutoMapper was free and useful software for a long time. Jimmy really do great job maintainig it, and even coming out as guy who want a bit more money was done in very professional way.

    So why not even create a fork given that AutoMapper have MIT license?

    Is across whole .NET community not enough developers who have two things, a bit of free time, and a bit of charitable character to maintain things. Why send ripples across bunch of products and perform meaningless rewrites? If you think about it, if you want replace AutoMapper with Mapperly you somehow should justify it. Prefereably as business developers say, that should have business impact. Some fearmongering that “maybe” something happens is not really a justification, because obviosuly Mapperly after sometime may go out of OSS business. Maybe not, but we don’t know. Is rewriting to anything else, not nescessary Mapperly obviously, a reasonable investment, or you can just fork existing working product, with excellent maintainance infrastructure and call it a day.

    But just forking is not maintaining!

    Yes, sure. But how often you expect anything new from AutoMapper as was super happy with new release? From what I know Jimmy don’t really cooperate much with outsiders. That’s his project, cannot blame him on choosing safe way to engage with users. What kind of improvements do you really expect? If you have one, and want spend cycles discussing how you can improve something, let me know.

    Now to maintaining. I really don’t see this as high maintainaince project. You can really go very far with allowing people contribute and submit PR + tests. Existing tests very solid. Just adopt policy to never change existing tests and never break them. That’s easy. Improving would be harder, but you know, who cares… That’s maintainance and we in .NET and not in JavaScript where Mark’s Zuckerberg shouting ‘Move fast and break everything’ from every corner.

    I want improvements!

    So do I. My personal wish for AutoMapper is to be able use it in NativeAOT. Honesly given it’s very liberal use of reflection, I did not try to do that on my NativeAOT fixing spree. I thinking that Jimmy would not want to re-engeneer library to make it support NativeAOT. Maybe I was wrong, but given that I have perception that it would not answer I do not even try. Probably this is golden opportunity. Maybe that allow me to make NativeAOT more friendly to corporate codebases. I know that NativeAOT is painful, and the more libraries will support it in some fashion, the better for everybody. I never understand some decisions which Microsoft developers did back then, and now I painfully realize that this is proper decisions, even if NativeAOT is not that extreme and agressive as it can be. Kudos for caring about community THAT much.

    So in short, expect some source generator experiments. I know that support everything would be impossible, but let’s try to poke that. That would be in separate branch probably.

    Statement

    I create fork, and call it MagicMapper, it’s on Nuget, I do not fully migrate on it my projects, but I will.

    I at minimum plan to maintain this fork for an year. Most likely more. I’m much more liberal to transferring ownership to the project to other, so in case I would be missing or unable to, I think it would be possible to continue work on the project for anybody else, without disruption by other.

    I do try my best to have spirit of OSS running on this project. I want that fork to be solution for independent developers. For somebody to remember, I hope it can be revitalization of Alt.Net movement.

    Personally I more dislike AutoMapper then like it. The only reason why I dislike it, is that it breaks tooling and if using without moderatin it’s easy to make things worse. That don’t reason to abandon library in my opinion, we should preserve too. What I learn during my years in software development is that rewriting is always worst decision then evolution.

    What about other projects?

    In addition to AutoMapper there MediatR and MassTransit. Honesly I never think about forking them, but jokes from my friends that I fork everything what can be forked sometimes make sense. I think I have limited time to maintain, and cannot do that alone, so if somebody think that’s worth it, I may reconsider my involvement. AutoMapper can live on life support, but MediatR is next level, and MassTransit is definitely even more harder.

    Acknoledgment

    I fully aknowledge hard work which Jimmy Bogard did on AutoMapper. I would like to thank you him! I personally don’t envision how my fork can endanger his future business or AutoMapper as commercial thing. I think there can be space for both options in the .NET ecosystem.

    Call for help

    I still not done transferring documentation to some other location, and make sure that all links point to proper location, and other housekeeping things. If you want help, go to Github and start hacking.

  • Шаблони використання LLM - Шаблон уточнення питання

    Це п’ята стаття стаття із серії яка описує шаблони будування запитів до LLM систем. Інші статті в серії

    Шаблон уточнення питання

    Намір і контекст

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

    Мотивація

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

  • Досвід із використання відкритого коду в уряді Мексики

    Це переклад статті із LWN.NET

    Прийняття урядами програмного забезпечення з відкритим вихідним кодом мало як злети, так і падіння. Хоча відкритий код здається очевидним вибором, виявляється, що уряди можуть бути дивно опірними до використання вільного ПЗ з відкритим кодом (FOSS) з різних причин. Федеріко Гонсалес Уейт виступив на конференції Open Government на SCALE 22x у Пасадені, Каліфорнія, щоб згадати свій досвід роботи із та на мексиканський уряд. Він очолював декілька проєктів, що передбачали перехід від пропріетарних, часто хижацьких, програмних компаній, з певним успіхом і також невдачами.

    Гонсалес Уейт почав з того, що він є мексиканцем/ківі ("не так много таких як ми", сказав він зашарівшись), який провів дев’ять або десять років на високих посадах у мексиканському уряді, «просуваючи впровадження відкритого коду». Серед іншого він був CTO у Міністерстві закордонних справ; «Я фактично відповідаю за те, що сьогодні мексиканці мають електронні паспорти». Це був один з проєктів, яким він керував, і частина його була виконана за допомогою ПЗ з відкритим кодом, що люди вважають дивовижним, за словами Гонсалеса Уейта. Він працював в офісі національної стратегії при президенті Андресі Мануелі Лопесі Обрадорі, а згодом став генеральним директором Національного центру досліджень і інновацій Мексики.

    У всіх своїх ролях він виступав за використання відкритого коду в уряді; бути «змінювачем» такого масштабу завжди нелегко, зазначив він. Він залишив уряд після недавньої зміни президента (на Клаудію Шейнбаум) і зараз працює «допомогаючи людям здійснювати власні трансформації» до відкритого коду, водночас слідкує за наступними великими тенденціями. Він зазначив, що відповість на запитання в кінці, але можливо не зможе відповісти на всі через конфіденційні зобов’язання, проте він «вже не є публічним посадовцем, тому це дає мені більше свободи говорити відкрито».

  • Шаблони використання LLM - Шаблон персона

    Це четверта стаття стаття із серії яка описує шаблони будування запитів до LLM систем. Інші статті в серії

    Шаблон персона

    Намір і контекст

    У багатьох випадках користувачі бажають, щоб результат LLM завжди мав певну точку зору або перспективу. Наприклад, може бути корисно провести перевірку коду так, ніби LLM є експертом з безпеки. Намір цього шаблону полягає в тому, щоб надати LLM «особистість», яка допомагає вибирати які типи результатів генерувати та на яких деталях зосереджуватися.

    Мотивація

    Користувачі можуть не знати, на яких видах результатів або дрібницях важливо зосередитися LLM для досягнення поставленого завдання. Однак вони можуть знати роль або тип людини, яку вони зазвичай просять допомогти з цими речами. Шаблон Персона дозволяє користувачам висловлювати, з чим їм потрібна допомога, не знаючи подробиць очікуваних результатів.

  • Шаблони використання LLM - Перевернута взаємодія

    Це третя стаття стаття із серії яка описує шаблони будування запитів до LLM систем. Інші статті в серії

    Перевернута взаємодія

    Намір і контекст

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

    Мотивація

    Замість того, щоб користувач керував бесідою, LLM часто має знання, які може використовувати для більш точного отримання інформації від користувача. Мета шаблону Flipped Interaction полягає в тому, щоб перевернути потік взаємодії, щоб LLM ставив користувачеві запитання для досягнення бажаної мети. LLM часто може краще вибрати формат, кількість і зміст взаємодій, щоб забезпечити досягнення мети швидше, точніше та/або використовуючи знання, якими користувач може (спочатку) не володіти.

  • Шаблони використання LLM - Автоматизатор виводу

    Це друга стаття стаття із серії яка описує шаблони будування запитів до LLM систем. Інші статті в серії

    Автоматизатор виводу

    Намір і контекст

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

    Мотивація

    Результатом LLM часто є послідовність кроків, які користувач повинен виконати. Наприклад, прохаючи LLM створити конфігураційний скріпт на Python, LLM може запропонувати кілька файлів які треба модифікувати та зміни, які слід застосувати до кожного файлу. Однак змушувати користувачів постійно виконувати кроки вручну, продиктовані результатом LLM, це дуже виснажливо і цей процес буде схильним до помилок.

  • Шаблони використання LLM - Шаблон створення сленгу

    Це перша стаття із серії яка описує шаблони будування запитів до LLM систем. Інші статті в серії

    Шаблон створення сленгу

    Намір і контекст

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

    Мотивація

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

  • Італійській опенсурс

    Шлях Італії до відкритого коду

    Історія використання відкритого коду в Італії серед держустанов починається із публікації змін до DECRETO-LEGGE 22 giugno 2012, n. 83. Ці зміни явно прописали можливість використовування програмного забезпечення із відкритим кодом. Ці зміни не декларували потребу використовувати саме відкритий код, але вимагали проводити оцінку ефективності використання відкритого коду у порівнянні із пропрієтарними рішеннями. Пізніше, після публкації цього закону, у листопаді 2012 Агенція Цифрової Італії (L’Agenzia per l’Italia Digitale) почала закликати усіх зацікавлених прийняти участь у процесі будування рекомендацій для виконування данних змін. На той час, в Італії вже було правило що вимагало різні держустанови ділитися між собою розробленими для них, чи куплене їм програмне забезпечення. Це правило дуже схоже до юрідичних правил ліцензування відкритого коду, де будь які зміни становляться публічними для інших.

  • Reflection on Evaluating Human Factors beyond likes of code.

    I’m very glad that more articles like this come out of academia. If you haven’t read it yet, please do, as my thoughts are based on this article.

    Personally as industry worker I suffered a lot from perceived misinterpretation of some usability and easy-of-use metrics for programming languages. Also blanket ignoring that some of my friends and coworkers have problem with understanding of some PL concepts. Also even if I totally agree with message, my perception is that message of article would pass by intended audience and things become “business as usual”. I writing this post, to probably fuel some discussion.

  • Сертіфікований перевіряльник типів

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

    Зауваження: цей приклад базується на прикладі із книги Certified Programming with Dependent Types Адама Чіліпала і прикладу із репозіторію Lean4.

  • Вартість програмного забезпечення з відкритим кодом

    Це переклад статті від Гарвадської школи бізнеса. Орігінал тут

    Зміст

  • Порівняння перевірки запозичень Rust із аналогом у C#

    Це переклад орігінальної статті із англійської. Усі дяки туди!

    Хвилинку! C# має засіб перевірки запозичень?

    Дивіться: класичний приклад безкоштовної безпеки пам’яті у Rust…

    // error[E0597]: `shortlived` does not live long enough
    
    let longlived = 12;
    let mut plonglived = &longlived;
    {
    	let shortlived = 13;
    	plonglived = &shortlived;
    }
    
    *plonglived;
    

    …портуючи на C#:

    // error CS8374: Cannot ref-assign 'shortlived' to 'plonglived' because
    // 'shortlived' has a narrower escape scope than 'plonglived'
    
    var longlived = 12;
    ref var plonglived = ref longlived;
    {
    	var shortlived = 13;
    	plonglived = ref shortlived;
    }
    
    _ = plonglived;
    
  • Learning programming by immersion

    This is translation of post in Ukrainian

    I just read article about Stephen Krashen’s theory on second language acquisition and it struck me with similarities which I see in the learning how we build software. Maybe that can be said about any skill acquisition, but given that programming languages and natural languages have some similarities I would try to speculate a bit.

  • Вивчення програмування через занурення

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

  • Швейцарский закон: Открытый исходный код по умолчанию

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

    Открытый исходный код и открытые правительственные данные

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

  • Ашық код ретінде қабылданған: бұл швейцариялық заң.

    Бұл мақала украин тілінен аударылған. Сонымен қатар, орыс тілінде аудармасы бар.

    Ашық бастапқы код және ашық үкіметтік деректер

    Интернетте швейцариялық үкіметтің енді барлық бағдарламалық өнімдерді ашық код лицензиясымен жариялау керектігі туралы жаңалық тарады. Бұл маған өте қызықты болды, бірақ Швейцария ағылшын тілді ел болмағандықтан, нақты не істелгені туралы ақпарат өте аз болды. Белгілі болғандай, заңдардың талдауы жаңалықтарда жарияланатын нәрсе емес. Заңдардың өзін оқу керек, аудармасында болса да, және өздігінен қорытынды жасауға тырысу керек. Сонымен қатар, кез келген әзірлеушіге тек заңдар ғана емес, код та қызықты. Сол сиқырлы ашық код. Сондықтан мен оқуға да, тексеруге де жеткілікті ақпарат табуға тырыстым.

  • Tokens in different languages

    How different languages define tokens?

    One guy ask in the chat, “how should I define tokens? should I combine token information with position in file?”. That’s simple question, and coming from C#, for me answer was obviously yes. But, I was curios how other languages define different tokens.

  • Відкритий код як усталено: це швейцарський закон

    Відкритий вихідний код і відкриті урядові дані

    Через увесь інтернет пролетіла новина що швейцарський уряд тепер повинен викладати усі програмні продукти, під ліцензіями відкритого коду. Це дуже мене зацікавило, але через те що Швейцарія не англомовна країна, то інформація про те що саме було зроблено, було дуже мало. А як відомо, аналіз законів це не про те що публікують у новинах. Треба читати самі закони, хай і у перекладі, та намагатися самостійно зробити висновки. Також будь якому розробнику звісно цікаві не тільки закони, а і код. Дей цей магічний відкритий код. Тому я спробував знайти достатньо інформації щоб було і що почитати і що потицяти.

  • Безкоштовні датасети із супутників!

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

    Найбільш часто використовувані безкоштовні багатоспектральні супутникові зображення:

    • Sentinel 2
    • Landsat-8
  • Придумана складність у програмуванні!

    Студентам та джунам-фрілансерам присвячується.

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

    — Нещодавно я написав чудову, корисну, дуже складну програму

    Де ці епітети – чудовий, корисний та дуже складний стояли в один ряд і мали означати якісь виключно цінні якості цього твору. Щодо слів чудовий, корисний, то в цьому немає сумніву, але те, що слова дуже складний в цьому ряду – це, звичайно, нісенітниця.

  • MSBuid як мова програмування!

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

subscribe via RSS