Стендап Сьогодні

Що я зробив, що я хочу зробити, і що це все значить.
Повсякденні здобутки в форматі стендапу.
Детальніше в статті

30.07.2023

Формальна верифікація: найслабкіша передумова

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

Починаємо з післяумови, яка вже повинна бути задана. (До речі, я про це не згадав, але одна додаткова синтаксична функція моєї граматики — оголошення перед- та післяумов у коментарях.) Далі беремо останню команду та перетворюємо післяумову на найслабкішу передумову, яка гарантує справдження післяумови після цієї команди.

Розглянемо найпростіший приклад. Якщо команда — це присвоєння x = y+1, то всі згадки про x у післяумові треба замінити на y+1. Якщо післяумова була x > 0, то найслабкіша передумова - y+1 > 0.

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

Нарешті, отримуємо найслабкішу передумову для всієї програми. Залишається тільки поєднати її з оголошеною передумовою знаком “випливає” (⇒) та теорема про вірність готова!

Мабуть, потрібно подумати про те, що така теорема стверджує. Вона обмежена тим змістом, який вклав програміст; без хорошої перед- та післяумови доведення не буде корисним — або навпаки, не буде можливим. У цьому формальна верифікація схожа на юніт-тести - “правильність” програми все одно залежить від людського розуміння. Різниця в тому, що юніт-тести перевіряють обмежений набір випадків, а формальна верифікація — буквально всі.

Код для цієї частини

29.07.2023

Формальна верифікація: обробка коду та граматики

Будь-яка обробка коду, будь то компіляція, перевірка на вірність, форматування, або формальна верифікація, зазвичай починається з розбору на синтаксичне дерево. Так і тут. Для цього проєкту я обрав генератор парсерів ANTLR. Він видатний зокрема тим, що підтримує декілька мов — проміж них Java та C#. Для реалізації на Clojure я згенерував класи Java, а коли переписував на F# - то підійшла та сама граматика. Також ANTLR офіційно підтримує Golang та TypeScript. Одним словом, рекомендую мати у своєму арсеналі.

Граматику я писав з нуля. Спочатку намагався знайти готову, але це виявилося складно — бо те, що є, не підходило під мою семантичну модель. (Тут допомогла б стандартна модель esast, з системи Unified, але її ще не існувало.) На мою думку, для простих випадків граматику краще писати наново.

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

Правила парсера описують власне синтаксичне дерево. А саме, можливі варіанти того, як токени складаються у вузли дерева. Ну, наприклад: операція присвоєння: <ідентифікатор> <=> <вираз>. Найвищий вузол - програма: <команда>+, тобто програми складається з команд, а команди своєю чергою з виразів, а вирази з ідентифікаторів. Задача парсера — побудувати дерево, що відповідає тексту.

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

Код для цієї частини

28.07.2023

Вступ до формальної верифікації програм

Сьогодні піде мова про мою бакалаврську роботу — яка ставила собою засіб формальної верифікації програм на псевдо-JavaScript. Кінцевий результат реально працює, хоч і для академічно простих прикладів. Робота була написана на Clojure - бо я тоді від неї був в захваті — та стала цікавим досвідом функціонального програмування. Настільки цікавим, що пізніше я переписав її на F#, щоб випробувати й цю мову — до речі, мабуть, перше, що я робив з VSCode.

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

Як можна досягнути такого результату? Насправді концептуально все просто. Раз — побудувати теорему про вірність — тобто, формальний вислів, який гарантує справдження післяумов. Два — довести теорему. Проблема в тому, що теорему довести складно навіть вручну, а автоматично — ще складніше. Детальніше — в наступні дні.

Чи має це все практичний сенс? Та взагалі має. Формальна верифікація остаточно доводить те, що програма працює правильно. Є мова SPARK - вона використовується для систем з високим ризиком — наприклад, авіоніки. Або середовище Coq. На жаль, через складність доведення теорем ваш додаток React навряд чи колись стане формально верифікованим.

27.07.2023

Terraform, його шари та редагування стану

Давно вже хочу написати про це статтю; кожного разу, як доводиться хірургічно виправляти стан. От сьогодні я створив неправильний aws_ecs_task_definition, а потім затупив та видалив його вручну, після чого Terraform навідсіч відмовився працювати. Коли багато працюєш з Terraform, варто мати таку ментальну модель того, як код декларацій Terraform перетворюється на зміни в реальному оточенні.

В центрі цього процесу знаходиться стан Terraform. Стан — це каталог всіх ресурсів, про які Terraform вже знає. З боку коду, ресурсом є кожна декларація resource, а з боку реального світу, до нього привʼязана та сутність, якою Terraform керує. Обовʼязково у кожній сутності є ідентифікатор, який зазвичай зазначається в кінці документації про ресурс. Це важливо тому, що сама сутність нічого про Terraform не знає — саме тому Terraform можна застосувати до будь-якої предметної галузі.

Але також саме тому важливо не створювати та не видаляти ресурси з Terraform власноруч. Взагалі, краще не міняти, але зі змінами Terraform впорається, а от коли розходяться уявлення про існування ресурсів — ручних виправлень не уникнути. Для того є команди state rm та import. Причому імпортувати можна будь-що, тільки треба буде вручну визначити ідентифікатор. Але на хмарному сервісі з імпортуванням складно, бо треба оголосити локально всі наявні змінні, що дратує. Є третя команда - taint - яка просить Terraform видалити ресурс та створити наново. Це інколи єдиний спосіб виправити помилки. (Але в моєму випадку за сьогодні допомогло видалення зі стану командою state rm.)

А поки набір реальних сутностей в стані не змінюється, все інше поміняти набагато легше. Вся структура коду служить тому, щоб побудувати список ресурсів — тому створення нових локальних змінних для рефакторингу взагалі ніяк не вплине на стан. Якщо ж ресурси перейменувати або перемістити в модуль, однак залишити за ними привʼязку до світу, то з сучасним Terraform це робиться на рівні конфігурації — блоком moved. Раніше треба було вживати команду state mv, що робило перейменування окремою процедурою. Блок moved застосовується водночас з рештою конфігурації, що розвʼязує руки для рефакторингу в будь-який зручний момент.

26.07.2023

На Cloud Ops не заощадиш

Коментар до вчорашнього посту нагадав мені про мою профдеформацію — а саме, останні роки я працюю в оточенні, де AWS є даним. Тому коли я порівнював Lambda, то в першу чергу порівнював з ECS.

Проте якщо починати з вільного вибору, то брати AWS для розгортування вебдодатка це безглуздя. Заощадження у коштах вийдуть неадекватними витратами часу та зусиль. Навіть якщо мати досвід AWS - все одно має сенс зупинитись на простішому хостингу - Fly.io, Heroku і так далі. “Сантехнікою” варто займатись, тільки коли є потреба.

На жаль, я не знаю середньої альтернативи між контейнеризованим хостингом та повним хмарним. Допомагає принаймні вести облік в Terraform та за можливістю рефакторити. Насправді є багато різних модулів для Terraform - для створення того ж сервісу ECS, наприклад. Але за моїм досвідом між сервісами залишається достатньо різниці, щоб такий підхід був непрактичним — абстракція “тече” (як сантехніка). Можливо, також Kubernetes в чомусь допомагає, але мені він не зайшов через власну складність.

До речі, ми як раз шукаємо DevOps інженера — чесно, не планував рекламувати вакансію, але був би дуже радий мати поруч досвідченого спеціаліста.

25.07.2023

Cloud ops - сантехніка інтернету

Коли я порівнював запуск Rails на AWS Lambda та AWS ECS, я нічого не сказав про складність розгортування. Хоча, було бажання написати, що ECS це просто, а Lambda потребує більше налаштувань. Проте от в чому справа — мені здавалося, що різниця обʼєктивна, а субʼєктивна, бо з ECS в мене набагато більше досвіду.

Сьогодні довелося створювати новий сервіс на ECS, та ця підозра підтвердилась. Так, сам сервіс являє собою скупчення контейнерів Docker, це ніби зрозуміло, та нагадує Heroku або мій улюблений Fly.io. Але скільки всього потрібно створити навколо сервісу, щоб він запрацював! Роль IAM - зрозуміло. Група безпеки — для цього сервісу та ще не забути оновити всі його залежності. Балансувальник навантаження — без нього сервіси ECS не працюють. Ресурси журналу (та дозволи на них.) А далі, ще налаштувати CodeDeploy. Підготувати параметри Parameter Store. І далі, і далі.

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

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

24.07.2023

Remark та Unified

Дізнався про екосистему обробки синтаксичних дерев, від якої я абсолютно в захваті. Це екосистема Unified для TypeScript (та JavaScript.) Я натрапив на неї при пошуку бібліотеки для розбору Markdown - та виявив, що бібліотека Remark побудована саме на основі Unified.

З чого взагалі складається Unified? В першу чергу, це стандартна обʼєктна модель синтаксичного дерева (ну, може, не стільки обʼєктна, стільки структурна — бо не використовує класів.) Навколо цієї моделі побудоване скупчення функцій, що її обробляють. Як базовий приклад — пакет unist-util-visit. Цією функцією можна знайти в дереві потрібні вузли — наприклад, задачі в документі Markdown.

На такій базовій системі побудовані інструменти для різних мов та задач. Кожна мова має свою специфікацію дерева — наприклад, mdast для Markdown. Але, як я був здивований дізнатись, Prettier теж використовує Unified - для форматування JavaScript!

Втім, мені нічого, окрім Markdown, не потрібно. Навіть в такому випадку наявність стандартизованого дерева спрощує створення доповнень, яких для Remark є чимало.

23.07.2023

Створення доповнення для Obsidian

…Виявилося простою та приємною справою. Підготовка оточення потрібна мінімальна — доповнення це звичайний проєкт на TypeScript. Документація чудова. Декларації типів теж. Так званий зразок доповнення насправді містить всі потрібні налаштування - yarn, tsc, esbuild - та також приклади по більшості можливостей розширення. Оновлення наживу можливе.

Робота з інтерфейсом відбувається через HTML/CSS. Тобто ніякої інтерфейсної бібліотеки вивчати не треба. Навпаки, можна використати React або іншу бібліотеку.

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

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

Але простіше за все, то є точка розширення registerMarkdownCodeBlockProcessor(). Вона дозволяє замінити блок коду (три лапки) з визначеною “мовою” на результат виклику функції, тобто довільний HTML. Це працює в обох режимах. Так, фактично, можна вкраплювати в документи справжні додатки — що я й спробую зробити.

22.07.2023

Markdown як структурна мова

…Роздивився вихідний код Obsidian Tasks. Зрозумів, чому вони не підтримують вкладені задачі. Виявляється, що вони обрали найпростіший підхід до розбору документів — рядки з задачами шукають регулярними виразами. Ніякого звʼязку між рядками немає, тому немає й вкладеності. За словами самих розробників, без серйозного рефакторингу її не зробити.

При цьому, документ Markdown наділений цілком реальною структурою. Попри відсутність розмітки, а точніше, навіть завдяки їй — бо на відміну від HTML, Markdown дійсно є мовою “what you see is what you get”.

Колись я вже робив менеджер задач на основі Markdown, тільки на React Native. Ідея була в тому, що редагувати текст на телефоні незручно, тому можна перетворити текст на список (в сенсі UI) - наприклад, елементом списку могла бути задача, яку можна було легко закрити, або ж відредагувати текст, пересунути на інше місце, і так далі. Всі ці зміни перетворювались назад у Markdown.

Як це працювало: я брав дерево AST, створене у markdown-it. Далі перетворював це дерево на семантичне, тобто таке, де елементи мають сенс в моєму контексті: параграфи, списки, задачі, і таке інше. Потім це дерево розрізав на елементи списку. Елементи списку вирушали в React Native.

При змінах зі списку наново будується весь документ. Відтворити оригінальний документ теж простіше, ніж з HTML, бо у розмітці Markdown менше варіації. Наприклад, тег HTML може містити довільні пробіли, а у Markdown таких нюансів майже немає — хіба що список можна створити з * або - та інші дрібниці.

21.07.2023

Доповнення Obsidian Tasks

Виявилось, що в Obsidian вже є чарівне доповнення Tasks, яке вирішує 90% моїх потреб. (Більш за те, решту можна доробити, про що пізніше.)

Сам по собі синтаксис задач - [ ] в Obsidian є стандартно. Доповнення Tasks робить дві речі. Додає розширений синтаксис для оздоблення задачі метаданими — це різні дати та пріоритет. Для цього синтаксису є навіть окремий модальний редактор, але ніхто не заважає написати його руками (з автодоповненням!), бо метадані зберігаються у звичайному тексті: - [ ] надіслати звіт 🔺 📅 2023-08-10. Мою ідею про автоматичне занотовування дати початку Tasks вже реалізував.

Та друга функція Tasks - це можливість побудувати список задач з результатів пошуку. Пошук можна робити як по всій колекції, так і по одному документу, а також фільтрувати по статусах, датах, і так далі. Це відразу вирішило мою потребу бачити список поточних задач: path includes next projects / status.type is in_progress / group by filename.

Чого Tasks не вміє категорично, це розрізняти вкладені задачі. Тобто будь-який елемент, розмічений як задача, має рівний порядок. Хотілося б все ж таки щоб в переліку задач не зʼявлялися ті, що мають вкладені. Або — ті, що заблоковані попередніми задачами. Можливо, як раз тут я можу додати функціоналу власним плагіном, якщо буду назначати відповідні статуси. (До речі, окрім класичних “зроблено”/“не зроблено” Tasks дозволяє створювати довільні статуси та багато з них вже мають підтримку тем.)

Стає ясною концептуальна різниця між Obsidian та іншими системами ведення нотаток. Зазвичай системи діляться на “чисто текстові” та “розширені та розумні” - вибір між простотою та користю. Натомість підхід Obsidian - витягати з простого тексту більше структурованої інформації. Це залишає можливість обробляти цей текст потужними засобами — ручними та автоматичними. Наприклад, щоб перетворити свій список задач в правильні анотації Tasks, я просто скопіював його в VSCode та швидко це зробив мультикурсорами.

Раніше

Пізніше