←back to thread

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

(queue.acm.org)
167 points yarapavan | 1 comments | 01 Apr 25 14:59 UTC | HN request time: 0.001s | source
Show context
csbartus ◴[01 Apr 25 18:08 UTC] No.43549787[source]▶
I've recently created a likely-correct piece of software based on these principles.

https://www.osequi.com/studies/list/list.html

The structure (ontology, taxonomy) is created with ologs, a formal method from category theory. The behavior (choreography) is created with a semi-formal implementation (XState) of a formal method (Finite State Machines)

The user-facing aspect of the software is designed with Concept Design, a semi-formal method from MIT CSAIL.

Creating software with these methods is refreshing and fun. Maybe one day we can reach Tonsky's "Diagrams are code" vision.

https://tonsky.me/blog/diagrams/

replies(1): >>43550342 #
matu3ba ◴[01 Apr 25 19:10 UTC] No.43550342[source]▶
"Diagrams are code" exists as ladder diagrams for PLC, from which Structured Text can be derived, which typically are used by PICs for simple to estimate time behavior in very time-sensitive/critical (real-time) control applications.

Stack + dynamic memory and other system resource modeling would need proper models with especially memory life-time visualization being an open research problem, let alone resource tracking being unsolved (Valgrind offers no flexible API, license restrictions, incomplete and other platforms than Linux are less complete etc).

Reads and writes conditioned on arithmetic have all the issues related to complex arithmetic and I am unaware of (time) models for speculation or instruction re-ordering, let alone applied compiler optimizations.

replies(1): >>43553889 #
1. jlcases ◴[02 Apr 25 05:26 UTC] No.43553889[source]▶
Fascinating approach with ologs and FSMs I've been working on PAELLADOC (https://github.com/jlcases/paelladoc) which applies MECE principles to documentation structure. Similar philosophy but focused on knowledge representation correctness rather than software behavior.

The results align with your experience - structured conceptual foundations make development more intuitive and documentation more valuable for both humans and AI tools.