Доброго понедельника!

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

sigops.org — рассматриваются принципы дизайна подобной системы с точки зрения формальной верификации и то какие инструменты используются для этого.

sigops.org — история ядер L4, с концентрацией на технической реализации, реализация IPC, управлением памятью и планировщиком процессов. А так же от каких решений приходилось отказываться и почему.

Не то, чтобы всем приходилось каждый день писать микроядра, но чтение может быть интересным и полезным даже для тех, кто этим не занимается.

а есть возможность модифицировать или запретить markup в сообщениях в телеграм? а то все теги кроме последнего выделяются жирным т.к. телеграм воспринимает * как символ жирности?

А давайте спецолимпиадку по типам? Есть код codegists.com это Freer для стрелок, но с ним проблема, нужно квадратичное число инстансов, так надо определять Category (Freer Category eff), Category (Freer Arrow eff), несмотря на то, что Category => Arrow. Что очевидно очень печально, и хотелось бы это поправить.

У меня получилось такое:

gist.github.com

Есть чуть более простые варианты но с тоже с квадратичным числом инстансов, хоть и более простых. Так же можно запилить вариант на TH который будет сразу генерить полный instance search, но это читерство.

Принимаются варианты и предложения по улучшению гиста.

подлый телеграм все ссылки вида /message превращает в команды и автоматически отправляет при клике, получается не очень хороший UI. Можно сделать чтобы телеграмобот не отправлял сразу сообщения вида /message если это не команда? ну или стандартные ссылки переводить в валидные линки или команды?