В этом выпуске: мы, не успев погрустить о том, что новый интересный спонсор не смог случиться, совершим глубокое погружение в мир формальных методов верификации. Какие подходы считать формальными методами? Кто это применяет и где? Как начать верифицировать свой софт и на что это похоже? Где искать свойства для проверки? Как читать и рефакторить формальные спецификации?
На закуску мы традиционно побурчим на SaaS’ы и починим валерин HDMI.

• [00:05:31] Наш новый спонсор, которого не случилось
• [00:06:59] Вместо рекламы
  • DigitalOcean The developer cloud
  • Установки и настройка OpenVPN в Ubuntu Linux за 5 минут | Записки программиста
  • Поднимаем собственный почтовый сервер на VDS | Записки программиста
• [00:09:40] Интервью с гостем
  • https://twitter.com/falsenov
  • anton-trunov (Anton Trunov) · GitHub
  • Эликсир от даунтайма — Episode 0185 « DevZen Podcast
  • GitHub — ligurio/practical-fm: A gently curated list of companies using verification formal methods in industry
  • Cosette: An Automated SQL Solver
  • GitHub — coq-community/awesome-coq: A curated list of awesome Coq libraries, plugins, tools, verification projects, and resources [maintainers=@anton-trunov,@palmskog]
  • Software Foundations
  • Certified Programming with Dependent Types
  • John Hughes — How to specify it! A guide to writing properties of pure functions | Code Mesh LDN 19 — YouTube
  • The Science of Deep Specification
  • K framework · GitHub
  • Telegram: Contact @practical_fm
• [02:03:18] Что мы узнали на этой неделе
  • International Fixed Calendar — Wikipedia
  • International Fixed Calendar — The Perihelion Effect
  • http://www.public.asu.edu/~checkma/today.html
• [02:08:46] [Одной строкой, SaaSZen] Disqus продолжает охреневать
• [02:11:05] [Одной строкой, SaaSZen] Mail.ru запугивает пользователей
• [02:12:11] Летняя школа по верификации Лялямбда-2021
  • Лялямбда ’21, школа верификации, компиляторов и реверса
  • Логистика Лялямбда ’21
• [02:17:31] Я у мамы спикер-гофер или GopherConRussia 2021
• [02:18:45] Кажется починил HDMI

Лог чата: https://t.me/devzen_live/1191

КДПВ отсюда.

Голоса выпуска: Света, Валера, Ваня, Саша, а также гости Антон и Василий

Фоновая музыка: Plastic3 — Corporate Rock Motivation Loop 4