←back to thread

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

(queue.acm.org)
167 points yarapavan | 2 comments | 01 Apr 25 14:59 UTC | HN request time: 0s | 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. csbartus ◴[01 Apr 25 20:13 UTC] No.43550862[source]▶
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...

replies(1): >>43553776 #
2. jlcases ◴[02 Apr 25 04:55 UTC] No.43553776[source]▶
Thank you for introducing me to ologs - they're fascinating. I'm intrigued by the distinction you make between formal methods and semi-formal approaches.

I'd love to explore how your "likely-correct model for writing" might complement the MECE-based documentation system I've been developing. Since you're building a model focused on writing correctness, perhaps there's an opportunity to collaborate?

My approach addresses the organizational structure of documentation, while your work seems to focus on ensuring correctness at the content level. Together, these could potentially create a more comprehensive solution that combines hierarchical organization with formal correctness principles.

Would you be interested in discussing further? I'm curious to learn more about your model.