Make formal verification and provably correct software practical and mainstream

Outside of mission critical applications, if the cost involved to make software "provably correct" (time, salaries) is greater than the cost of the bugs, it will never be adopted.

Believe me, I see the appeal, but it's kind of like demanding your house have all perfect right angles and completely level surfaces. Living with manageable imperfection is far more realistic.

Re: Make formal verification and provably correct software practical and mainstream

#7

Post by sharkbot » Sat, May 28, 2022, 10:15 PM UTC

naniwaduni wrote: post #4

eurasiantiger wrote: post #3

Can we formally verify the software cannot be used for evil?

gonna have to formally define evil

The constructivist in me thinks we could define it inductively :)

Re: Make formal verification and provably correct software practical and mainstream

#8

Post by KSteffensen » Sat, May 28, 2022, 10:22 PM UTC

daenz wrote: post #6

Outside of mission critical applications, if the cost involved to make software "provably correct" (time, salaries) is greater than the cost of the bugs, it will never be adopted. Believe me, I see the appeal, but it's kind of like demanding your house have all perfect right angles and completely level surfaces. Living with manageable imperfection is far more realistic.

Why does it always have to be all or nothing? Is your codebase 100% covered by unit tests?

You don't have to make sure all the angles of your house are perfect right angles, but there's probably a couple that really have to be. Formally verify those and live with manageable imperfection for the rest.

Re: Make formal verification and provably correct software practical and mainstream

#9

Post by dqpb » Sat, May 28, 2022, 10:24 PM UTC

pid-1 wrote: post #2

I've started watching Lamport's TLA+ course in YT and it totally blew my mind. What are other good resources in formal verification?

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.

Re: Make formal verification and provably correct software practical and mainstream

#10

Post by homodeus » Sat, May 28, 2022, 10:30 PM UTC

pid-1 wrote: post #2

I've started watching Lamport's TLA+ course in YT and it totally blew my mind. What are other good resources in formal verification?

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