TFTDS / Лекция 10 / Спецификация распределённой системы. TLA+

00:00:00 - Дизайн-документ CocroachDB 00:07:00 - Дизайн-документ exactly-once и транзакций в Kafka 00:12:15 - Необходимость формальной спецификации 00:20:05 - TLA+ 00:28:49 - TLA+-спецификация, граф конфигураций 00:39:51 - Логика первого порядка 00:45:40 - Линейная темпоральная логика 01:00:00 - Примеры темпоральных формул 01:07:15 - Описание графа состояний темпоральными формулами 01:11:30 - Спецификация алгоритма Евклида 01:16:58 - Спецификация к "Die Hard" 01:24:51 - Спецификация Paxos 01:47:20 - Спецификация RAFT 01:57:08 - PlusCal, трансляция в TLA+ 02:10:17 - Rust. Loom. Library level model checking 02:13:47 - Jepsen. Blackbox fault injection 02:18:30 - Library level fault injection 02:23:21 - Выбор языка. Учет ссылок, типизация со временем жизни 02:28:49 - Kotlin и null safety 02:30:15 - Type state safety 02:39:19 - Chaos engineering Дата лекции: 30 октября 2021 Лектор: Роман Липовский Съёмка и монтаж: Дмитрий Купцов Плейлист с лекциями:    • TFTDS (лекции, 3 курс, осень 2021) - Липов...   Плейлист с семинарами:    • TFTDS (семинары, 3 курс, осень 2021) - Лип...