В качестве, видимо, новогоднего подарка мне, на канале NDC выложили прекрасный доклад Шона Парента:
Locknote: Local Reasoning in C++ - Sean Parent - NDC TechTown 2024 https://youtu.be/bhizxAXQlWc
Ниже мой конспект этого доклада. Разумеется я также рекомендую вам посмотреть и составить собственное мнение, но может быть этот конспект поможет сделать правильные акценты, т.к. доклад сложный и насыщенный.
---
00:00 Failed software projects.
Когда проекты по разработке ПО проваливаются большинство исследователей винят менеджмент и процессы. Некоторые доходят до обвинения инструментов разработки и библиотек. Но очень часто виновато неправильное управление сложностью в разрабатываемой системе. Система может оказаться просто по своему построению слишком сложна, чтобы даже идеальная команда при идеальном менеджменте могла бы её отладить и поддерживать.
10:00 Local reasoning.
Что такое возможность рассуждать о свойствах программы локально? Это возможность убедиться в корректности части кода, независимо от контекста в котором эта часть будет использована. Ключ к такой возможности это корректное использование API на стороне client и его разумное проектирование на стороне implementor.
Также немного о предусловиях: тщательно выписываем предусловия конкретных функций, выносим общие предусловия.
15:56 Mutation
Почему мы вообще хотим использовать модифицируемые переменные? Нищета программирования с иммутабельными структурами на примере замены двигателя. Очень часто именно мутабельные переменные проще для доказательства свойств. Дуализм трансформации и действия.
void a(T& x) { x = t(x); } // a from t
T t(T x) { a(x); return x; } // t from aНо см. ниже, этот дуализм работает не всегда.
18:38 Laws of exclusivity
std::vector a{0, 1, 1, 0};
erase(a, a[0]);
println("{}", a);Не запуская годболт, догадайтесь что будет на экране. Потом посмотрите пример. Удивительно, но это даже не UB.
Далее Парент приводит правила исключения одновременных ссылок для Swift и Rust. Фактически то же правило есть в C++ (если вы не хотите проблем), но убедиться в его соблюдении -- задача разработчика.
29:05 Projections and Objects
Проекция это получение ссылки на часть объекта. Проекции могут быть инвалидированы как итераторы для контейнера или как отображение или как повисшая ссылка и т.д.
Оказывается дуализм между действием и трансформацией, описанный выше работает только для инкапсулированных (contained) объектов, но не для их проекций. Нам нужно чтобы выполнялся equational reasoning -- свободная замена равных подвыражений в выражениях.
Главное при проектировании типа для объектов это отношение часть/целое. Это отношение обладает свойствами связанности, ацикличности, сепарабельности и владения.
Если бы у нас были только отношения части и целого, то проблема, поставленная в начале, была бы решена. Увы, мир сложнее.
45:20 Extrinsic relashionships
Внешними называются все отношения, которые не часть/целое: хранение невладеющего указателя, хранение ключа или индекса на внешний массив, ссылка на глобальную переменную, использование примитивов синхронизации.
Важнейшая лемма, которой суммируется доклад: для возможности рассуждать о программе локально, внешние отношения между классами должны быть инкапсулированы в класс-владелец, хранящий их корректность в качестве своего инварианта.
54:40 Structural complexity
Проблема трёх тел как пример внешних взаимосвязей, приводящих к непредсказуемости системы. Виды структурной зависимости: деревья, полидеревья, DAG, полные графы. Фактически только структурная зависимость в форме деревьев решает поставленную проблему.
01:05:24 Summary
---
От себя добавлю что именно такого рода разматывание внешних связей между сущностями и то, как это привело к гораздо лучшему проектированию генератора llvm-snippy, я показывал на Zero-cost conf прошлого года. Но там от меня это был конкретный пример проектирования, к тому же изрядно перемешанный с деталями предметной области. Здесь же Шон Парент даёт очищенную эссенцию такого подхода, практически с математической точностью формулировок.
#talks
