TE
科技回声
首页24小时热榜最新最佳问答展示工作
GitHubTwitter
首页

科技回声

基于 Next.js 构建的科技新闻平台,提供全球科技新闻和讨论内容。

GitHubTwitter

首页

首页最新最佳问答展示工作

资源链接

HackerNews API原版 HackerNewsNext.js

© 2025 科技回声. 版权所有。

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

174 点作者 yarapavan大约 1 个月前

9 条评论

Cyphase大约 1 个月前
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.<p><a href="https:&#x2F;&#x2F;www.youtube.com&#x2F;watch?v=tsSDvflzJbc" rel="nofollow">https:&#x2F;&#x2F;www.youtube.com&#x2F;watch?v=tsSDvflzJbc</a><p>&gt; Coding isn&#x27;t Programming - Closing Keynote with Leslie Lamport - SCaLE 22x
评论 #43560657 未加载
评论 #43553822 未加载
csbartus大约 1 个月前
I&#x27;ve recently created a likely-correct piece of software based on these principles.<p><a href="https:&#x2F;&#x2F;www.osequi.com&#x2F;studies&#x2F;list&#x2F;list.html" rel="nofollow">https:&#x2F;&#x2F;www.osequi.com&#x2F;studies&#x2F;list&#x2F;list.html</a><p>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)<p>The user-facing aspect of the software is designed with Concept Design, a semi-formal method from MIT CSAIL.<p>Creating software with these methods is refreshing and fun. Maybe one day we can reach Tonsky&#x27;s &quot;Diagrams are code&quot; vision.<p><a href="https:&#x2F;&#x2F;tonsky.me&#x2F;blog&#x2F;diagrams&#x2F;" rel="nofollow">https:&#x2F;&#x2F;tonsky.me&#x2F;blog&#x2F;diagrams&#x2F;</a>
评论 #43550342 未加载
pera大约 1 个月前
&gt; 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.<p>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?
评论 #43556743 未加载
gqgs大约 1 个月前
A key concern I&#x27;ve consistently had regarding formal verification systems is: how does one confirm the accuracy of the verifier itself?<p>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.<p>While this perspective doesn&#x27;t necessarily render formal verification impractical, it does introduce certain caveats that, in my experience, are not frequently addressed in discussions about these systems.
评论 #43550706 未加载
评论 #43552467 未加载
评论 #43553826 未加载
评论 #43558410 未加载
评论 #43550740 未加载
评论 #43550610 未加载
评论 #43553529 未加载
评论 #43554265 未加载
评论 #43577690 未加载
OhMeadhbh大约 1 个月前
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 &quot;oh. you&#x27;re using 5 minute metrics.&quot; Their response was &quot;how could you figure that out just by looking at the graph?&quot; When I replied &quot;Queuing theory and control theory,&quot; their response was &quot;what&#x27;s that?&quot;<p>Since then, Amazon&#x27;s hiring practices have only gotten worse. Can you invert a tree? Can you respond &quot;tree&quot; or &quot;hash map&quot; when you&#x27;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&#x27;re Amazon material.<p>Did you pay attention to the lecture about formal proofs. TLA+ or Coq&#x2F;Kami? That&#x27;s great, but it won&#x27;t help you get a job at Amazon.<p>The idea that formal proofs are used anywhere but the most obscure corners of AWS is laughable.<p>Although... it <i>is</i> a nice paper. Props to Amazon for supporting Ph.D.&#x27;s doing pure research that will never impact AWS&#x27; systems or processes.
评论 #43549462 未加载
评论 #43549563 未加载
评论 #43550279 未加载
评论 #43549089 未加载
评论 #43552944 未加载
评论 #43549053 未加载
评论 #43549401 未加载
deterministic大约 1 个月前
I have used simulators to develop hard-to-make-correct distributed code.<p>It helped me find all kinds of subtle non-intuitive bugs that would have gone unnoticed had I only used hand coded automatic tests.<p>Highly recommended.
nullorempty大约 1 个月前
And what teams use these methods exactly?
评论 #43548526 未加载
评论 #43552340 未加载
jlcases大约 1 个月前
I&#x27;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).<p>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.<p>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.
评论 #43550862 未加载
评论 #43553797 未加载
评论 #43549557 未加载
评论 #43549622 未加载
评论 #43554253 未加载
neuroelectron大约 1 个月前
Great April 1st gag. Seems to have gone over everyone&#x27;s head.