Make formal verification and provably correct software practical and mainstream

Re:Make formal verification and provably correct software pr... by pid-1 on Saturday May 28, 2022 @05:56PM (#31544231)

I've started watching Lamport's TLA+ course in YT and it totally blew my mind.

What are other good resources in formal verification?

[ Parent | on HN ]

Re:Make formal verification and provably correct software pr... by picardo on Saturday May 28, 2022 @11:20PM (#31546054)

I found TLA+ syntax unapproachable as a beginner. I did more digging and discovered Alloy[0], a "lightweight" formal verification system, which is much simpler, and has industry adoption as well. It's working nicely for me so far.

-----------

[0] http://alloytools.org/

[ Parent | on HN ]

Re:Make formal verification and provably correct software pr... by homodeus on Saturday May 28, 2022 @06:30PM (#31544432)

The Bible of formal software logic, free of charge: https://softwarefoundations.cis.upenn.edu/

[ Parent | on HN ]

Re:Make formal verification and provably correct software pr... by practal on Saturday May 28, 2022 @07:07PM (#31544646)

If you are more practical than religious, try this: https://functional-algorithms-verified.org

[ Parent | on HN ]

Re:Make formal verification and provably correct software pr... by dqpb on Saturday May 28, 2022 @06:24PM (#31544393)

State Machines are the natural paradigm in TLA+. OOP is just poorly organized state machines. Try rewriting an OO program with state machines and you’ll have something that directly maps to TLA+, and it should demystify much of formal verification.

[ Parent | on HN ]