This one from @ilyasergey's course on Programming with Proofs, as a reference reading .. (link to the course: 👇) .. I just skimmed through the contents and here's my 1000 ft view of it .. looking forward to a deep dive read very soon, looks like a great way into the combination of FP, proof systems and Lean .. The course page also refers to work-in-progress class “Practical Verifications of Data structures and Algorithms” (aka PraVDA) - it would be interesting to get some insights into it as well .. The Hitchhiker’s Guide to Logical Verification (2025 Desktop Edition) is a textbook-style guide to interactive theorem proving using the Lean 4 proof assistant. • It introduces the logical foundations of Lean, starting from simple type theory and gradually moving to dependent types, inductive definitions, and structured proofs, treating Lean as a vehicle for learning rigorous reasoning rather than an end in itself. • The book then develops functional and effectful programming in Lean (with inductive types, type classes, monads, etc.) and shows how to prove properties of programs using techniques like induction and rule-based reasoning. (This is the part that looked very interesting to me) • In later chapters it covers program semantics -operational, Hoare and denotational, and connects them to machine-checked proofs, including the use of proof automation and metaprogramming in Lean. • Throughout, the goal is to equip readers with enough practical and theoretical background to tackle real verification projects and move comfortably between Lean and other modern proof assistants.

This is a great thought raising a “mechanical sympathy” point that’s often missing from day-to-day DDD conversations - the in-memory layout of your data and the access patterns of your hot paths matter a lot for performance. In regular designs of domain models we tend to focus more on the conceptual model of the problem domain. Eric Evans’ DDD also talks about modelling the ubiquitous language and capturing domain invariants and not about specifying memory layouts. Treating "domain model" as a prescription for in-memory representation confuses conceptual model with data structure choice. Despite the original domain modelling literature not considering the aspects of mechanical sympathy, the following are real concerns when the tyre hits the road: 1. Access patterns dominate performance. If a workload touches one field of millions of objects in tight loops, a Struct of Arrays (SoA) can massively reduce cache misses and help prefetchers do their job. This is standard data-oriented design (DOD) guidance. 2. False sharing is real. Co-located hot fields updated by different threads can thrash a shared cache line and nuke scalability. Padding, alignment, and data partitioning are sometimes required. However at the same time AoS vs SoA is context-dependent. If your operations usually need several fields from the same entity at once, AoS can be faster (fewer loads, better spatial locality for that use case). There isn’t a one-size-fits-all rule. Some of my thoughts on addressing this .. Think "clean domain model at the edges, data-oriented core for hot loops" .. 1. Model for the business first (standard DDD) Keep entities, value objects, and domain services intention-revealing and faithful to the problem space. This is your collaboration/communication surface. 2. Measure before changing layout Profile CPU time, cache misses, branch misses, and lock contention. Optimize measured hotspots only. 3. Introduce a data-oriented “kernel” behind the model - For the tight loop: use SoA buffers that match the access pattern (SIMD-friendly, batchable). - Keep this layout behind a domain service/repository boundary so the rest of the code can stay idiomatic DDD. - Map between entities and buffers at the boundary (cost is paid at well-chosen seams, not everywhere). This is standard DOD practice. 4. Split hot vs cold fields - Extract “hot” mutable counters/state into a separate structure (or shard by thread) to avoid false sharing. Keep “cold” descriptive fields with the entity. - Manual padding can help or use `CachePadded` like padding (as in Rust). In native code, align/pad structures and avoid mixing hot data in the same line. 5. Choose layout based on operation - SoA if you stream through one/few fields across many items (filters, aggregations, vector math). - AoS if most accesses touch many fields of the same item (rich object logic). 6. Exploit read models/projections If you use CQRS or simply maintain projections, it’s natural to keep a domain model for commands/invariants and one or more performance-tuned read models (often SoA-ish indexes or columnar structures) for queries/analytics. This is general DDD/CQRS practice. Evans doesn’t forbid multiple coexisting models. Let me know your thoughts in the replies .. Maybe I should implement something as a PoC for such modelling strategy ..

Accumulate the recipes and materialize at the boundary. Compose the algebra and commit to the implementation as late as possible. A very typical functional programming pattern.