В этом выпуске: мы, не успев погрустить о том, что новый интересный спонсор не смог случиться, совершим глубокое погружение в мир формальных методов верификации. Какие подходы считать формальными методами? Кто это применяет и где? Как начать верифицировать свой софт и на что это похоже? Где искать свойства для проверки? Как читать и рефакторить формальные спецификации?
На закуску мы традиционно побурчим на SaaS’ы и починим валерин HDMI.
- [00:05:31] Наш новый спонсор, которого не случилось
- [00:06:59] Вместо рекламы
- [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] Что мы узнали на этой неделе
- [02:08:46] [Одной строкой, SaaSZen] Disqus продолжает охреневать
- [02:11:05] [Одной строкой, SaaSZen] Mail.ru запугивает пользователей
- [02:12:11] Летняя школа по верификации Лялямбда-2021
- [02:17:31] Я у мамы спикер-гофер или GopherConRussia 2021
- [02:18:45] Кажется починил HDMI
Лог чата: https://t.me/devzen_live/1191
Голоса выпуска: Света, Валера, Ваня, Саша, а также гости Антон и Василий.
Фоновая музыка: Plastic3 — Corporate Rock Motivation Loop 4
КДПВ отсюда.
Подкаст: Скачать (81.1MB)