Hacker News with Generative AI: Formal Methods

100 theorems in Lean (leanprover-community.github.io)
Freek Wiedijk maintains a list tracking progress of theorem provers in formalizing 100 classic theorems in mathematics as a way of comparing prominent theorem provers.
Mathematics, Theorem Provers, Software, Formal Methods
8 points by ggzor 6 hours ago | 0 comments
GenAI-Accelerated TLA+ Challenge (tlapl.us)
The TLA+ Foundation, in collaboration with NVIDIA, is pleased to announce the GenAI-accelerated TLA+ challenge—an open call for submissions that explore the intersection of TLA+ and generative AI.
Generative AI, Software, Programming Challenges, Formal Methods, Artificial Intelligence
35 points by lemmster 17 days ago | 16 comments
Requirements change until they don't (buttondown.com)
Recently I got a question on formal methods1: how does it help to mathematically model systems when the system requirements are constantly changing?
Software Development, Formal Methods, Requirements Engineering
74 points by azhenley 25 days ago | 22 comments
Algebraic Semantics for Machine Knitting (uwplse.org)
As programming languages researchers, we’re entitled to a certain level of mathematical rigor behind the languages we write and analyze.
Computer Science, Programming Languages, Formal Methods, Machine Learning
246 points by PaulHoule 31 days ago | 20 comments
Systems Correctness Practices at AWS: Leveraging Formal and Semi-Formal Methods (queue.acm.org)
AWS (Amazon Web Services) strives to deliver reliable services that customers can trust completely.
Systems Correctness, Cloud Computing, AWS, Software Engineering, Formal Methods
174 points by yarapavan 52 days ago | 54 comments
The Calculated Typer (bahr.io)
We present a calculational approach to the design of type checkers, showing how they can be derived from behavioural specifications using equational reasoning.
Type Theory, Programming Languages, Software Engineering, Formal Methods
75 points by matt_d 67 days ago | 5 comments
Formal Methods: Just Good Engineering Practice? (2024) (brooker.co.za)
Yes. The answer is yes. In your face, Betteridge.
Software Engineering, Formal Methods
211 points by aiono 133 days ago | 133 comments
The P Programming Language: Formal modeling and analysis of distributed systems (github.com/p-org)
Challenge: Distributed systems are notoriously hard to get right. Programming these systems is challenging because of the need to reason about correctness in the presence of myriad possible interleaving of messages and failures. Unsurprisingly, it is common for service teams to uncover correctness bugs after deployment. Formal methods can play an important role in addressing this challenge!
Programming Languages, Distributed Systems, Formal Methods
17 points by wslh 195 days ago | 2 comments
Don't implement unification by recursion (philipzucker.com)
Unification is formal methods speak for solving equations.
Formal Methods, Programming, Computer Science
83 points by mathgenius 207 days ago | 62 comments
Reflecting away from definitions in Liquid Haskell (tweag.io)
We’ve all been there: wasting a couple of days on a silly bug. Good news for you: formal methods have never been easier to leverage.
Programming, Haskell, Formal Methods
4 points by JNRowe 253 days ago | 0 comments
Use of Formal Methods by a Silicon Manufacturer (1988) [pdf] (bris.ac.uk)
Formal Methods, Software Engineering, Manufacturing, History
11 points by todsacerdoti 314 days ago | 1 comments
Formal methods: Just good engineering practice? (brooker.co.za)
Formal Methods, Software Engineering, Programming Practices
179 points by ot 336 days ago | 149 comments
CBMC: C bounded model checker (2021) (cprover.org)
Software, Programming, Verification, Formal Methods
106 points by fanf2 384 days ago | 31 comments
Forge: A Tool to Teach Formal Methods (brownplt.org)
Formal Methods, Programming, Tools, Education
21 points by todsacerdoti 397 days ago | 1 comments