Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Make formal verification and provably correct software practical and mainstream

github.com

Post reply on HN
Print view View original

181–190 of 203 posts

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

#181

Post by guerrilla »

User23 wrote: post #160
practal wrote: post #92

Earlier quoted context omitted.

The threshold is mathematicians opting to use these tools themselves for their work. There are not many mathematicians using them so far. A nice example is the recent formalisation in Lean of some ideas by Peter Scholze: https://xenaproject.wordpress.com/2021/06/05/half-a-year-of-... That's great stuff, which shows what can in principle be done with this technology. But why is a team necessary to formalise Scholze's…

Most mathematicians are doing work that is, frankly, formally unsound. There's a huge culture of hidden assumptions in most mathematical fields. Not to mention that the syntax is literally unparseable. For example what does this mean? sin(x) + cos(x) Most mathematicians would say it's the sum of the sine of x and the cosine of x. But it parses fine as the sum of the product of s, i, and n(x), and the product of c, o,…

> But it parses fine as the sum of the product of s, i, and n(x), and the product of c, o, and s(x).

No it doesn't because math lexes greedily (and is also context sensitive anyway.) 'sin' is a symbol just like 'x'. There's no ambiguity in your example.

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

#182

Post by User23 »

practal wrote: post #178
User23 wrote: post #161

Earlier quoted context omitted.

Verification is largely a fool's errand[1]. The juicy opportunity is tooling that aids in constructing programs such that they necessarily have the desired properties. Predicate transformer semantics are up to the task. It's basically just applied lattice theory, which is a very well understood field of math and within the learning capacity of any competent programmer. Edit: Automated verification does however attrac…

Automated verification is not the latest in a long list of fads. First, it is not a fad, and second, it has been around for a long time (check for example [0], which dates from 1961). I agree with you that constructing programs such that they necessarily have the desired properties is the way to go. But we will disagree in how to go about that. Predicate transformer semantics is just another name for Hoare-Logic, and…

> Predicate transformer semantics is just another name for Hoare-Logic,

Sir Tony is certainly highly influential, but Hoare triples are a considerably more basic. Not to understate their importance, having a solid base to build on is essential.

> and is too narrowly focused on the program code itself. It is basically the opposite of correct by construction!

Please provide some explanation so that this doesn't read as an absurdity.

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

#183

Post by practal »

User23 wrote: post #182
practal wrote: post #178

Earlier quoted context omitted.

Automated verification is not the latest in a long list of fads. First, it is not a fad, and second, it has been around for a long time (check for example [0], which dates from 1961). I agree with you that constructing programs such that they necessarily have the desired properties is the way to go. But we will disagree in how to go about that. Predicate transformer semantics is just another name for Hoare-Logic, and…

> Predicate transformer semantics is just another name for Hoare-Logic, Sir Tony is certainly highly influential, but Hoare triples are a considerably more basic. Not to understate their importance, having a solid base to build on is essential. > and is too narrowly focused on the program code itself. It is basically the opposite of correct by construction! Please provide some explanation so that this doesn't read as…

PTS and Hoare-logic are really the same, just differently formulated. At least according to Wikipedia: https://en.wikipedia.org/wiki/Predicate_transformer_semantic...

What I mean by my comment is that typically with Hoare-style verifications, you add invariants to the program AFTER it has been constructed. So in this sense it is not correct by construction, but rather verified after construction. Instead, under correct by construction I would understand an upfront proof about some abstract function, and then the concrete code generated for this function will be automatically correct.

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

#184

Post by User23 »

practal wrote: post #183
User23 wrote: post #182

Earlier quoted context omitted.

> Predicate transformer semantics is just another name for Hoare-Logic, Sir Tony is certainly highly influential, but Hoare triples are a considerably more basic. Not to understate their importance, having a solid base to build on is essential. > and is too narrowly focused on the program code itself. It is basically the opposite of correct by construction! Please provide some explanation so that this doesn't read as…

PTS and Hoare-logic are really the same, just differently formulated. At least according to Wikipedia: https://en.wikipedia.org/wiki/Predicate_transformer_semantic... What I mean by my comment is that typically with Hoare-style verifications, you add invariants to the program AFTER it has been constructed. So in this sense it is not correct by construction, but rather verified after construction. Instead, under corre…

> What I mean by my comment is that typically with Hoare-style verifications, you add invariants to the program AFTER it has been constructed.

Ah, perhaps some people misuse predicate transformers that way, I don’t know. I do know however that that’s not how their inventors used them or meant for them to be used. The basic idea is that you define the postcondition you’d like to establish before writing any code. Then you derive a chain of predicate transformers such that the final precondition is suitable. A common choice is the predicate that is true for all states, but for partial correctness another might be used. Since any given predicate transformer has a syntactic representation, the result is the program text. As you can see the result is correct by construction.

I recommend reading Dijkstra’s A Discipline of Programming for pragmatic examples of using predicate transformers to derive correct programs. If you want a more rigorously formal treatment of the same subject there’s Dijkstra and Scholten’s Predicate Transformers and Program Semantics.

Edit: Here[1] is a nontrivial example, although it assumes some familiarity and doesn’t spell everything out. When you get to the acknowledgments section it’s clear why.

[1] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD07xx/E...

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

#185

Post by User23 »

guerrilla wrote: post #181
User23 wrote: post #160

Earlier quoted context omitted.

Most mathematicians are doing work that is, frankly, formally unsound. There's a huge culture of hidden assumptions in most mathematical fields. Not to mention that the syntax is literally unparseable. For example what does this mean? sin(x) + cos(x) Most mathematicians would say it's the sum of the sine of x and the cosine of x. But it parses fine as the sum of the product of s, i, and n(x), and the product of c, o,…

> But it parses fine as the sum of the product of s, i, and n(x), and the product of c, o, and s(x). No it doesn't because math lexes greedily (and is also context sensitive anyway.) 'sin' is a symbol just like 'x'. There's no ambiguity in your example.

Thank you for illustrating the culture of assumptions I was referring to.

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

#186

Post by hwayne »

guerrilla wrote: post #181
User23 wrote: post #160

Earlier quoted context omitted.

Most mathematicians are doing work that is, frankly, formally unsound. There's a huge culture of hidden assumptions in most mathematical fields. Not to mention that the syntax is literally unparseable. For example what does this mean? sin(x) + cos(x) Most mathematicians would say it's the sum of the sine of x and the cosine of x. But it parses fine as the sum of the product of s, i, and n(x), and the product of c, o,…

> But it parses fine as the sum of the product of s, i, and n(x), and the product of c, o, and s(x). No it doesn't because math lexes greedily (and is also context sensitive anyway.) 'sin' is a symbol just like 'x'. There's no ambiguity in your example.

Pretty much any mathematician, on seeing `xy`, would think it's `x*y`, and not a new symbol called "xy".

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

#187

Post by hwayne »

AnimalMuppet wrote: post #81
petergeoghegan wrote: post #60

Earlier quoted context omitted.

This sounds like motivated reasoning to me. Have you heard of Therac-25? You might be inclined to suggest that that could have been prevented if only they'd used formal methods. Perhaps that's true. It's something that could have been prevented in many different ways, though. Yet it still happened.

Hmm. If I recall correctly, Therac-25 destroyed the company. It (and incidents like it) led the FDA to gradually be more stringent on scrutinizing software in medical devices. And yet, to the best of my knowledge, even the FDA has not mandated formal verification of the embedded software in medical devices. And yet, there almost certainly were lawsuits. So maybe you found evidence that perfectly counters my theory. I…

The company is still around and still makes hundreds of millions in revenue. https://en.wikipedia.org/wiki/Atomic_Energy_of_Canada_Limite...

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

#188

Post by mbrodersen »

practal wrote: post #174
mbrodersen wrote: post #171

Earlier quoted context omitted.

Professional mathematicians are today using dependent types in LEAN to prove leading edge mathematics. Google LEAN and mathlib.

I am aware of Lean and mathlib. It's the group around Kevin Buzzard which is doing mathlib, and it is for sure a great effort. Being practical, they latched onto the theorem proving facilities that are currently available, Lean certainly being one of the best at this moment. But just because they can make type theory work for them, with much effort, doesn't mean that it is the right way to do formal math. They are st…

Thanks for a great reply. I would like to check out your references. However you mention more than one but I can only see [2]?

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

#189

Post by mbrodersen »

practal wrote: post #174
mbrodersen wrote: post #171

Earlier quoted context omitted.

Professional mathematicians are today using dependent types in LEAN to prove leading edge mathematics. Google LEAN and mathlib.

I am aware of Lean and mathlib. It's the group around Kevin Buzzard which is doing mathlib, and it is for sure a great effort. Being practical, they latched onto the theorem proving facilities that are currently available, Lean certainly being one of the best at this moment. But just because they can make type theory work for them, with much effort, doesn't mean that it is the right way to do formal math. They are st…

You might also want to check out nuPRL. It uses a completely different approach (computational types). It might be a better match for what you are talking about.

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

#190

Post by practal »

mbrodersen wrote: post #188
practal wrote: post #174

Earlier quoted context omitted.

I am aware of Lean and mathlib. It's the group around Kevin Buzzard which is doing mathlib, and it is for sure a great effort. Being practical, they latched onto the theorem proving facilities that are currently available, Lean certainly being one of the best at this moment. But just because they can make type theory work for them, with much effort, doesn't mean that it is the right way to do formal math. They are st…

Thanks for a great reply. I would like to check out your references. However you mention more than one but I can only see [2]?

No worries, happy to talk about this stuff all day long! The links are in a higher up post, they are:

[0] https://obua.com/publications/philosophy-of-abstraction-logi...

[1] https://obua.com/publications/practical-types/1/

Post reply on HN