Итак, что удалось достигнуть на практике. Проект в области IoT, который разрабатывался двумя командами на протяжении 8 лет.
Было принято решение написать проект с нуля по SDD с объемом функциональности кратно (я бы даже сказал на порядок) превосходящим функциональность legacy системы посредством LLM.
Предварительно были проведены эксперименты по исследованию возможностей LLM по написанию кода на языках с развитой системой типов и формальной верификацией. В качестве предметки для эксперимента была выбрана алгоритмическая торговля на фондовом рынке как одна из наиболее сложных. Об этих экспериментах я писал здесь:
- https://t.me/emacsway_log/1751
- https://t.me/emacsway_log/1755
- https://t.me/emacsway_log/1759
По результатам эксперимента было принято решение писать проект на Rust, который имеет такую же развитую систему типов, как и OCaml, и необычайно развитую экосистему формальной верификации. Забегая наперёд скажу, что с OCaml Claude работает легче. Раза четыре даже возникало желание сменить Rust на OCaml.
SDD framework был разработан свой. Он содержит:
1. Обзор возможностей передовых конкурирующих продуктов.
2. Требования:
- Capabilities
- FR
- NFR
- BDD / Gherkin acceptance scenarios
3. Архитектура:
- ADRs
- C4 Model Structurizr DSL diagrams
- Mermaid Event Storming diagrams
- Canvas Domain Model
- Research документы
- Specifications:
- API:
- proto files
- OpenApi
- AsyncApi
- Cedar policy schema
- Config profiles
- SKOS онтология (SHACL/ShEx, валидация на Python с помощью rdflib и pyshacl)
- TLA+ доказательство (валидация на TLC)
- Alloy доказательство
4. Tools (больше 40 инструментов для самоконтроля LLM, трассировки и верификации реализации)
5. Собственно, сама реализация с формальной верификацией доменных моделей в Creusot/WhyML/Why3. MSA (15 сервисов), CQRS, DDD по всем канонам в FP парадигме + Railway Oriented Programming by Scott Wlaschin, Hexagonal/Clean Architecture, DSL Rule Engine, Transactional Outbox & Inbox по схеме Message Bridge, местами Event Sourcing, Unit of Work, Multitenancy, шифрование KMS/KEK/DEK, Specification Pattern, SAGA, Task-based UI (React). Хотел затащить ещё Reason/Rescript на фронт, но воздержался. Envoy gateway, ingress/egress. Полная пирамида тестирования.
В рамках проекта портировал и доработал свои DDD-библиотеки на Rust (до этого были реализации на Python, Golang, OCaml):
https://github.com/krew-solutions/ascetic-ddd-rust
Самая существенная часть работы - это первый микросервис. Последующие микросервисы LLM создаёт как семечки, копируя внутреннюю архитектуру первого как референсную. Вместе с первым сервисом создавалось и описание внутренней архитектуры сервиса в виде набора инструкций и ограничений для LLM.
В общей сложности работа над подготовкой требований заняла около 2-х человеко-месяцев, над реализацией - около 3-х человеко-месяцев. Но это не точно. На текущий момент готовность проекта около 80%. Ни строчки ручного кода.
Возникают мысли обощить абстрактую часть проекта в Open Source Framewofk, если получится изыскать время. Может быть даже попробовать применить этот подход в другой предметке. А то вы постоянно спрашивали про консалтинг. Не мог я раньше.
Post #1918
700
- 🔥 22
- 👍 11
- ❤ 4