←back to thread

Systems Correctness Practices at AWS: Leveraging Formal and Semi-Formal Methods

(queue.acm.org)
167 points yarapavan | 5 comments | 01 Apr 25 14:59 UTC | HN request time: 0.213s | source
Show context
jlcases ◴[01 Apr 25 17:38 UTC] No.43549529[source]▶
I've noticed that the formalization of methods described by AWS parallels what we need in technical documentation. Complex systems require not just formal verification but also structured documentation following MECE principles (Mutually Exclusive, Collectively Exhaustive).

In my experience, the interfaces between components (where most errors occur) are exactly where fragmented documentation fails. I implemented a hierarchical documentation system for my team that organizes knowledge as a conceptual tree, and the accuracy of code generation with AI assistants improved notably.

Formal verification tools and structured documentation are complementary: verification ensures algorithmic correctness while MECE documentation guarantees conceptual and contextual correctness. I wonder if AWS has experimented with structured documentation systems specifically for AI, or if this remains an area to explore.

replies(5): >>43549557 #>>43549622 #>>43550862 #>>43553797 #>>43554253 #
1. jkaptur ◴[01 Apr 25 17:49 UTC] No.43549622[source]▶
I'm interested in learning more about the benefits of MECE - I've never heard that before. In particular, it seems radically different from Divio's system [0], which presents the same information in many different ways.

0: https://docs.divio.com/documentation-system/

replies(3): >>43549705 #>>43551410 #>>43553800 #
2. zhengyi13 ◴[01 Apr 25 17:58 UTC] No.43549705[source]▶
Is this not https://diataxis.fr/ ?

(I'm engaged somewhat in trying to get our team to write any documentation; once I've got that, I'll start trying to organize along exactly these principles)

replies(1): >>43553832 #
3. ◴[01 Apr 25 21:12 UTC] No.43551410[source]▶
4. jlcases ◴[02 Apr 25 05:01 UTC] No.43553800[source]▶
Great question about MECE vs Divio's system! They actually complement each other rather than conflict.

MECE (Mutually Exclusive, Collectively Exhaustive) comes from management consulting and focuses on organizing concepts without overlap or gaps. Divio's system focuses on documentation types (tutorials, how-to, reference, explanation).

In the AI era, your question raises a fascinating point: if AI can dynamically adapt content to the user's needs, do we still need multiple presentation formats? I believe we do, but with a shift in approach.

With AI tools, we can maintain a single MECE-structured knowledge base (optimized for conceptual clarity and AI consumption) and then use AI to dynamically generate Divio-style presentations based on user needs. Rather than manually creating four different document types, we can have AI generate the appropriate format on demand.

In my experiments, I've found that a well-structured MECE knowledge base allows AI to generate much more accurate tutorials, how-tos, references, or explanations on demand. The AI adapts the presentation while drawing from a single source of truth.

This hybrid approach gives us the best of both worlds: conceptual clarity for AI consumption, and appropriate presentation for human needs - all while reducing the maintenance burden of multiple document versions.

5. jlcases ◴[02 Apr 25 05:11 UTC] No.43553832[source]▶
Yes, that's Diataxis (formerly Divio). I faced similar challenges and found that combining it with MECE principles in my PAELLADOC framework made documentation much easier, especially with AI tools. Good luck getting your team started