5 ms·

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

174 points by yarapavan 2y ago

deleted 2y ago
[deleted]
OhMeadhbh 2y ago
I find this highly unlikely. My first day at Amazon I encountered an engineer puzzling over a perfect sine wave in a graph. After looking at the scale I made the comment "oh. you're using 5 minute metrics." Their response was "how could you figure that out just by looking at the graph?" When I replied "Queuing theory and control theory," their response was "what's that?" Since then, Amazon's hiring practices have only gotten worse. Can you invert a tree? Can you respond "tree" or "hash map" when you're asked what is the best data structure for a specific situation? Can you solve a riddle or code an ill-explained l33tcode problem? Are you sure you can parse HTML with regexes? You're Amazon material. Did you pay attention to the lecture about formal proofs. TLA+ or Coq/Kami? That's great, but it won't help you get a job at Amazon. The idea that formal proofs are used anywhere but the most obscure corners of AWS is laughable. Although... it is a nice paper. Props to Amazon for supporting Ph.D.'s doing pure research that will never impact AWS' systems or processes.
- georgeburdell 2y ago
  A graph of what?
- deleted 2y ago
  [deleted]
- deleted 2y ago
  [deleted]
- scubbo 2y ago
  They specifically mention "the P team at AWS". The two following things are perfectly able to be simultaneously true: * The average Amazon engineer is not expected to have awareness of CS fundamentals that go beyond LeetCode-y challenges * The average Amazon engineer builds using tools which are each developed by a small core team who _are_ expected to know those fundamentals, and who package up those concepts to be usefully usable without full understanding (I did 10 years on CDO, and my experience matches yours when interacting with my peers, but every time I interacted with the actual Builder Tools teams I was very aware that lived in different worlds)
  - nextos 2y ago
    > The average Amazon engineer is not expected to have awareness of CS fundamentals that go beyond LeetCode-y challenges I find this a bit unsettling. There are dozens of great CS schools in the US. Even non-elite BSc programs in EU sometimes teach formal methods. There are also some good introductory books now, e.g. [1]. Perhaps its time to interview more on concepts and less on algorithmic tricks favored by LeetCode? I doubt current undergrads can't go beyond LeetCode-like challenges. [1] Formal Methods, An Appetizer. https://link.springer.com/book/10.1007/978-3-030-05156-3 https://link.springer.com/book/10.1007/978-3-030-05156-3
    - retrocryptid 2y ago
      Modern CS programs teach to what they perceive to be the interview their students will encounter after graduation: what is a tree data structure, how to craft a SQL query and how to calculate a CRC with a python library. More advanced CS/CE departments still teach discrete math and compilers/parsing for students intending to go to grad schools. My experience with recent CS grads is it's easier to hire Art and Political Science grads and take the time to teach them programming and all it's fundamentals. At least they won't argue with you when you tell them not to use regexes to parse HTML.
- Dichlorodiphen 2y ago
  We recently did a proof of concept with P for our system, and the reception was warm enough that I expect adoption within the year. I wouldn’t exactly call us obscure, at least in the sense used above—greenfield big data system with a bog-standard mix of AWS services. I will say that time to productivity with P is low, and, in my experience, it emphasizes practical applicability more so than traditional modeling languages like TLA+ (this point is perhaps somewhat unsubstantiated, but the specific tooling we used is still internal). That is to say, it is fairly easy to sell to management, and I can see momentum already starting to pick up internally. No Ph.D. in formal methods required. And re: the hiring bar, I agree that the bulk of the distribution lies a bit further left than one would hope/imagine, but there is a long tail, and it only takes a handful of engineers to spearhead a project like this. For maintainability, we are betting on the approachable learning curve, but time will tell.
  - Taikonerd 2y ago
    The problem (in my mind) with using P is that only a small % of problems are formalizable as communicating state machines. In your greenfield big data system, what were the state machines? What states could they be in?
  - matu3ba 2y ago
    Thanks for the interesting insight. 1. What would you recommend to model multi-thread or multi-process problems on the same system? Is there a good read to give recommendations? 2. Is there a good overview on trade-offs between CSP, Actor model and other methods for this? 3. Are you aware of any process group models?
- gqgs 2y ago
  Cool anecdote but I'm not sure how reasonable it is to expect every person to have expert domain knowledge and recall of every single computer science field just because they got a job to work at Amazon or any other MAANG company.
- atdt 2y ago
  OK, I will be the useful idiot. I don't fully understand your anecdote. Could you explain what is exactly it that you perceived and that the other engineer failed to see?
  - sethammons 2y ago
    Periodic and regular cycles (sine wave) suggests that there is over correction happening in the system, preventing a stable point. More regular measurements or tempered corrections may be called for. Concrete example: the system sees it's queue utilization as high so it throttles incoming requests, but for too long, the queue looks super healthy on the next check, so the throttle removed but too long until checking again, and now the util is too high again.
nullorempty 2y ago
And what teams use these methods exactly?
- riknos314 2y ago
  The article directly mentions several. > Teams across AWS that build some of its flagship products—from storage (e.g., Amazon S3, EBS), to databases (e.g., Amazon DynamoDB, MemoryDB, Aurora), to compute (e.g., EC2, IoT)—have been using P to reason about the correctness of their system designs. Later it more specifically mentions these (I probably missed a few): S3 index, S3 ShardStore, Firecracker VMM, Aurora DB engine commit protocol, The RSA implementation on Graviton2 (EDIT: formatting)
  - yarapavan 2y ago
    If you are wondering "why do formal methods at all?" or "how is AWS using P to gain confidence in correctness of their services?", the following re:Invent 2023 talk answers this question, provides an overview of P, and its impact inside AWS: (Re:Invent 2023 Talk) Gain confidence in system correctness & resilience with Formal Methods (Finding Critical Bugs Early!!) - https://www.youtube.com/watch?v=FdXZXnkMDxs https://www.youtube.com/watch?v=FdXZXnkMDxs Github: https://github.com/p-org/P https://github.com/p-org/P
- jmccarthy 2y ago
  https://aws.amazon.com/verified-permissions/ https://aws.amazon.com/verified-permissions/ (AVP) is a team and product which uses the formally verified Cedar language. https://arxiv.org/abs/2403.04651 https://arxiv.org/abs/2403.04651
pera 2y ago
> we also sought a language that would allow us to model check (and later prove) key aspects of systems designs while being more approachable to programmers. I find it a bit surprising that TLA+ with PlusCal can be challenging to learn for your average software engineer, could anyone with experience in P show an example of something that can be difficult to express in TLA+ which is significantly easier in P?
- ngruhn 2y ago
  It's probably just the syntax
  - goostavos 2y ago
    I think it goes beyond that. TLA+ requires you to think about problems very differently. It is very much not programming. It took me a long time (and many false starts) to be able to think in TLA. To quote Lamport, the real challenge of TLA+ is learning to think abstractly. To that, I think plusCal and the teaching materials around it do a disservice to TLA. The familiar syntax hides the wildly different semantics
jlcases 2y ago
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.
- jjmarr 2y ago
  Could you explain how your "hierarchical documentation system" works? Does the tree parallel the code? Is there a particular tool that you use?
  - jlcases 2y ago
    The hierarchical system I've developed organizes knowledge in nested MECE categories (Mutually Exclusive, Collectively Exhaustive). Rather than paralleling code exactly, it creates a conceptual tree that represents the mental model behind the system. For example, in an e-commerce API: - Level 1: Core domains (Products, Orders, Users) - Level 2: Sub-domains (Product variants, Order fulfillment, User authentication) - Level 3: Implementation details (Variant pricing logic, Fulfillment status transitions) I'm currently using plain Markdown with a specific folder structure, making it friendly to version control and AI tools. The key innovation is the organization pattern rather than the tooling - ensuring each concept belongs in exactly one place (mutually exclusive) while collectively covering all needed context (collectively exhaustive). I should note that this is a work in progress - I've documented the vision and principles, but the implementation is still evolving. The early results are promising though: AI assistants navigating this conceptual tree find the context needed for specific coding tasks more effectively, significantly improving the quality of generated code.
csbartus 2y ago
I've recently created a likely-correct piece of software based on these principles. https://www.osequi.com/studies/list/list.html 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/ https://tonsky.me/blog/diagrams/
- matu3ba 2y ago
  "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.
  - jlcases 2y ago
    Fascinating approach with ologs and FSMs I've been working on PAELLADOC (https://github.com/jlcases/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.
wg0 2y ago
[flagged]
- catlover76 2y ago
  [dead]
gqgs 2y ago
A key concern I've consistently had regarding formal verification systems is: how does one confirm the accuracy of the verifier itself? This issue appears to present an intrinsically unsolvable problem, implying that a formally verified system could still contain bugs due to potential issues in the verification software. While this perspective doesn't necessarily render formal verification impractical, it does introduce certain caveats that, in my experience, are not frequently addressed in discussions about these systems.
- whattheheckheck 2y ago
  Yeah it reminds me of https://en.m.wikipedia.org/wiki/Tarski%27s_undefinability_theorem https://en.m.wikipedia.org/wiki/Tarski%27s_undefinability_th...
- alexisread 2y ago
  I'd guess the best approach is similar to security - minimal TCB (trusted computing base) that you can verify by hand, and then construct your proof checker on top, and have it verify itself. Proof and type checkers have a lot of overlap, so you can gain coverage via the language types. I can't recall exactly, but I think CakeML (https://cakeml.org/jfp14.pdf https://cakeml.org/jfp14.pdf) had a precursor lisp prover, written in a verified lisp, so would be amenable to this approach. EDIT: think it was this one https://www.schemeworkshop.org/2016/verified-lisp-2016-scheme-workshop.pdf https://www.schemeworkshop.org/2016/verified-lisp-2016-schem...
  - guerrilla 2y ago
    This is correct. That's why you have core type theories. Very small, easy to understand and implement in a canonocal way. Other languages can be compiled to them.
- csbartus 2y ago
  Perhaps there is no such thing like absolute truth. In category theory / ologs, a formal method for knowledge representation, the result is always mathematically sound, yet ologs are prefixed with "According to the author's world view ..." On the other way truth, even if it's not absolute, it's very expensive. Lately AWS advocates a middle ground, the lightweight formal methods, which are much cheaper than formal methods yet deliver good enough correctness for their business case. In the same way MIT CSAIL's Daniel Jackson advocates a semi-formal approach to design likely-correct apps (Concept design) It seems there is a push for better correctness in software, without the aim of perfectionism.
neuroelectron 2y ago
Great April 1st gag. Seems to have gone over everyone's head.
Cyphase 2y ago
Leslie Lamport gave the closing keynote at SCaLE 22x this year, talking about formal methods and TLA+. He mentioned some previous work Amazon has done in that area. https://www.youtube.com/watch?v=tsSDvflzJbc https://www.youtube.com/watch?v=tsSDvflzJbc > Coding isn't Programming - Closing Keynote with Leslie Lamport - SCaLE 22x
- jlcases 2y ago
  Very interesting video. Many thanks
- kuleshovsoup 2y ago
  Thanks for sharing!
deterministic 2y ago
I have used simulators to develop hard-to-make-correct distributed code. It helped me find all kinds of subtle non-intuitive bugs that would have gone unnoticed had I only used hand coded automatic tests. Highly recommended.

174 points by yarapavan 2y ago

deleted 2y ago

[deleted]

I find this highly unlikely. My first day at Amazon I encountered an engineer puzzling over a perfect sine wave in a graph. After looking at the scale I made the comment "oh. you're using 5 minute metrics." Their response was "how could you figure that out just by looking at the graph?" When I replied "Queuing theory and control theory," their response was "what's that?" Since then, Amazon's hiring practices have only gotten worse. Can you invert a tree? Can you respond "tree" or "hash map" when you're asked what is the best data structure for a specific situation? Can you solve a riddle or code an ill-explained l33tcode problem? Are you sure you can parse HTML with regexes? You're Amazon material. Did you pay attention to the lecture about formal proofs. TLA+ or Coq/Kami? That's great, but it won't help you get a job at Amazon. The idea that formal proofs are used anywhere but the most obscure corners of AWS is laughable. Although... it is a nice paper. Props to Amazon for supporting Ph.D.'s doing pure research that will never impact AWS' systems or processes.

georgeburdell 2y ago
A graph of what?
deleted 2y ago
[deleted]
deleted 2y ago
[deleted]
scubbo 2y ago
They specifically mention "the P team at AWS". The two following things are perfectly able to be simultaneously true: * The average Amazon engineer is not expected to have awareness of CS fundamentals that go beyond LeetCode-y challenges * The average Amazon engineer builds using tools which are each developed by a small core team who _are_ expected to know those fundamentals, and who package up those concepts to be usefully usable without full understanding (I did 10 years on CDO, and my experience matches yours when interacting with my peers, but every time I interacted with the actual Builder Tools teams I was very aware that lived in different worlds)
- nextos 2y ago
  > The average Amazon engineer is not expected to have awareness of CS fundamentals that go beyond LeetCode-y challenges I find this a bit unsettling. There are dozens of great CS schools in the US. Even non-elite BSc programs in EU sometimes teach formal methods. There are also some good introductory books now, e.g. [1]. Perhaps its time to interview more on concepts and less on algorithmic tricks favored by LeetCode? I doubt current undergrads can't go beyond LeetCode-like challenges. [1] Formal Methods, An Appetizer. https://link.springer.com/book/10.1007/978-3-030-05156-3 https://link.springer.com/book/10.1007/978-3-030-05156-3
  - retrocryptid 2y ago
    Modern CS programs teach to what they perceive to be the interview their students will encounter after graduation: what is a tree data structure, how to craft a SQL query and how to calculate a CRC with a python library. More advanced CS/CE departments still teach discrete math and compilers/parsing for students intending to go to grad schools. My experience with recent CS grads is it's easier to hire Art and Political Science grads and take the time to teach them programming and all it's fundamentals. At least they won't argue with you when you tell them not to use regexes to parse HTML.
Dichlorodiphen 2y ago
We recently did a proof of concept with P for our system, and the reception was warm enough that I expect adoption within the year. I wouldn’t exactly call us obscure, at least in the sense used above—greenfield big data system with a bog-standard mix of AWS services. I will say that time to productivity with P is low, and, in my experience, it emphasizes practical applicability more so than traditional modeling languages like TLA+ (this point is perhaps somewhat unsubstantiated, but the specific tooling we used is still internal). That is to say, it is fairly easy to sell to management, and I can see momentum already starting to pick up internally. No Ph.D. in formal methods required. And re: the hiring bar, I agree that the bulk of the distribution lies a bit further left than one would hope/imagine, but there is a long tail, and it only takes a handful of engineers to spearhead a project like this. For maintainability, we are betting on the approachable learning curve, but time will tell.
- Taikonerd 2y ago
  The problem (in my mind) with using P is that only a small % of problems are formalizable as communicating state machines. In your greenfield big data system, what were the state machines? What states could they be in?
- matu3ba 2y ago
  Thanks for the interesting insight. 1. What would you recommend to model multi-thread or multi-process problems on the same system? Is there a good read to give recommendations? 2. Is there a good overview on trade-offs between CSP, Actor model and other methods for this? 3. Are you aware of any process group models?
gqgs 2y ago
Cool anecdote but I'm not sure how reasonable it is to expect every person to have expert domain knowledge and recall of every single computer science field just because they got a job to work at Amazon or any other MAANG company.
atdt 2y ago
OK, I will be the useful idiot. I don't fully understand your anecdote. Could you explain what is exactly it that you perceived and that the other engineer failed to see?
- sethammons 2y ago
  Periodic and regular cycles (sine wave) suggests that there is over correction happening in the system, preventing a stable point. More regular measurements or tempered corrections may be called for. Concrete example: the system sees it's queue utilization as high so it throttles incoming requests, but for too long, the queue looks super healthy on the next check, so the throttle removed but too long until checking again, and now the util is too high again.

nullorempty 2y ago

And what teams use these methods exactly?

riknos314 2y ago
The article directly mentions several. > Teams across AWS that build some of its flagship products—from storage (e.g., Amazon S3, EBS), to databases (e.g., Amazon DynamoDB, MemoryDB, Aurora), to compute (e.g., EC2, IoT)—have been using P to reason about the correctness of their system designs. Later it more specifically mentions these (I probably missed a few): S3 index, S3 ShardStore, Firecracker VMM, Aurora DB engine commit protocol, The RSA implementation on Graviton2 (EDIT: formatting)
- yarapavan 2y ago
  If you are wondering "why do formal methods at all?" or "how is AWS using P to gain confidence in correctness of their services?", the following re:Invent 2023 talk answers this question, provides an overview of P, and its impact inside AWS: (Re:Invent 2023 Talk) Gain confidence in system correctness & resilience with Formal Methods (Finding Critical Bugs Early!!) - https://www.youtube.com/watch?v=FdXZXnkMDxs https://www.youtube.com/watch?v=FdXZXnkMDxs Github: https://github.com/p-org/P https://github.com/p-org/P
jmccarthy 2y ago
https://aws.amazon.com/verified-permissions/ https://aws.amazon.com/verified-permissions/ (AVP) is a team and product which uses the formally verified Cedar language. https://arxiv.org/abs/2403.04651 https://arxiv.org/abs/2403.04651

pera 2y ago

> we also sought a language that would allow us to model check (and later prove) key aspects of systems designs while being more approachable to programmers. I find it a bit surprising that TLA+ with PlusCal can be challenging to learn for your average software engineer, could anyone with experience in P show an example of something that can be difficult to express in TLA+ which is significantly easier in P?

ngruhn 2y ago
It's probably just the syntax
- goostavos 2y ago
  I think it goes beyond that. TLA+ requires you to think about problems very differently. It is very much not programming. It took me a long time (and many false starts) to be able to think in TLA. To quote Lamport, the real challenge of TLA+ is learning to think abstractly. To that, I think plusCal and the teaching materials around it do a disservice to TLA. The familiar syntax hides the wildly different semantics

jlcases 2y ago

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.

jjmarr 2y ago
Could you explain how your "hierarchical documentation system" works? Does the tree parallel the code? Is there a particular tool that you use?
- jlcases 2y ago
  The hierarchical system I've developed organizes knowledge in nested MECE categories (Mutually Exclusive, Collectively Exhaustive). Rather than paralleling code exactly, it creates a conceptual tree that represents the mental model behind the system. For example, in an e-commerce API: - Level 1: Core domains (Products, Orders, Users) - Level 2: Sub-domains (Product variants, Order fulfillment, User authentication) - Level 3: Implementation details (Variant pricing logic, Fulfillment status transitions) I'm currently using plain Markdown with a specific folder structure, making it friendly to version control and AI tools. The key innovation is the organization pattern rather than the tooling - ensuring each concept belongs in exactly one place (mutually exclusive) while collectively covering all needed context (collectively exhaustive). I should note that this is a work in progress - I've documented the vision and principles, but the implementation is still evolving. The early results are promising though: AI assistants navigating this conceptual tree find the context needed for specific coding tasks more effectively, significantly improving the quality of generated code.

csbartus 2y ago

I've recently created a likely-correct piece of software based on these principles. https://www.osequi.com/studies/list/list.html 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/ https://tonsky.me/blog/diagrams/

matu3ba 2y ago
"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.
- jlcases 2y ago
  Fascinating approach with ologs and FSMs I've been working on PAELLADOC (https://github.com/jlcases/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.

wg0 2y ago

[flagged]

catlover76 2y ago
[dead]

gqgs 2y ago

A key concern I've consistently had regarding formal verification systems is: how does one confirm the accuracy of the verifier itself? This issue appears to present an intrinsically unsolvable problem, implying that a formally verified system could still contain bugs due to potential issues in the verification software. While this perspective doesn't necessarily render formal verification impractical, it does introduce certain caveats that, in my experience, are not frequently addressed in discussions about these systems.

whattheheckheck 2y ago
Yeah it reminds me of https://en.m.wikipedia.org/wiki/Tarski%27s_undefinability_theorem https://en.m.wikipedia.org/wiki/Tarski%27s_undefinability_th...
alexisread 2y ago
I'd guess the best approach is similar to security - minimal TCB (trusted computing base) that you can verify by hand, and then construct your proof checker on top, and have it verify itself. Proof and type checkers have a lot of overlap, so you can gain coverage via the language types. I can't recall exactly, but I think CakeML (https://cakeml.org/jfp14.pdf https://cakeml.org/jfp14.pdf) had a precursor lisp prover, written in a verified lisp, so would be amenable to this approach. EDIT: think it was this one https://www.schemeworkshop.org/2016/verified-lisp-2016-scheme-workshop.pdf https://www.schemeworkshop.org/2016/verified-lisp-2016-schem...
- guerrilla 2y ago
  This is correct. That's why you have core type theories. Very small, easy to understand and implement in a canonocal way. Other languages can be compiled to them.
csbartus 2y ago
Perhaps there is no such thing like absolute truth. In category theory / ologs, a formal method for knowledge representation, the result is always mathematically sound, yet ologs are prefixed with "According to the author's world view ..." On the other way truth, even if it's not absolute, it's very expensive. Lately AWS advocates a middle ground, the lightweight formal methods, which are much cheaper than formal methods yet deliver good enough correctness for their business case. In the same way MIT CSAIL's Daniel Jackson advocates a semi-formal approach to design likely-correct apps (Concept design) It seems there is a push for better correctness in software, without the aim of perfectionism.

neuroelectron 2y ago

Great April 1st gag. Seems to have gone over everyone's head.

Cyphase 2y ago

Leslie Lamport gave the closing keynote at SCaLE 22x this year, talking about formal methods and TLA+. He mentioned some previous work Amazon has done in that area. https://www.youtube.com/watch?v=tsSDvflzJbc https://www.youtube.com/watch?v=tsSDvflzJbc > Coding isn't Programming - Closing Keynote with Leslie Lamport - SCaLE 22x

jlcases 2y ago
Very interesting video. Many thanks
kuleshovsoup 2y ago
Thanks for sharing!

deterministic 2y ago

I have used simulators to develop hard-to-make-correct distributed code. It helped me find all kinds of subtle non-intuitive bugs that would have gone unnoticed had I only used hand coded automatic tests. Highly recommended.