alt Hacker NewsI'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
There is another way formal methods parallel documentation: both are futile unless you can prove that the modelized/documented system matches the actual, live one.
"This is just a matter of discipline" is not very convincing, especially when the discipline involves long unpaid afterhours.
The examples I've seen in this report from AWS are mostly about one-shot events (helping going through important changes). It's good to see formal methods used in these cases of course, but I'd really like to read stories about how sustained use of formal methods helps reclaiming the high costs of the initial investment as the actual system evolves alongside the modelization.
Could you explain how your "hierarchical documentation system" works? Does the tree parallel the code? Is there a particular tool that you use?
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.
MECE seems to be just a mathematical partition, so it seems there is not need of a new term and acronym.
Formalization, correctness is about models. [1]
There are formal methods where the underlying model is mathematically sound. There are semi-formal methods where the underlying model is structured but not proven to be sound.
For example, in your case ("organizes knowledge") a formal method is ologs from category theory. That method assures that the concepts and their relationship in your knowledge base are mathematically correct.
When you want to transfer that knowledge base into a documentation system you might want look for a mathematically sound model, but I'm afraid there is no such model, so what's left is a semi-formal method / a likely-correct model.
Right now I'm building such a likely-correct model for writing, contact me for more info.
[1] https://www.osequi.com/slides/formalism-correctness-cost/for...