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

191–200 of 203 posts

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

#191

Post by practal »

mbrodersen wrote: post #189
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…

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.

I've heard of nuPRL, it seems to be also based on type theory, with special emphasis on constructivity. It's basically the same as Coq, foundationally. At a summer school Bob Constable once said that he would refuse to fly in a plane with software which had been verified formally using classical logic, instead of constructive logic... Well, I wouldn't mind an intuitionistic verification, but I'd definitely take even "just" a classical one.

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

#192

Post by practal »

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,…

It's a weird example, but you definitely got a point. Of course, an ambiguity like in your example never causes a problem, because this text is parsed by humans, not by machines!

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

#193

Post by practal »

User23 wrote: post #184
practal wrote: post #183

Earlier quoted context omitted.

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…

Yes, I will concede that of course PTS can be used in a "first the invariants, then the code" way, and so my distinction doesn't make much sense here.

Nevertheless, PTS is for verifying imperative programs, and if whenever possible, I prefer reasoning about more elegant and simple mathematical objects instead.

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

#194

Post by User23 »

practal wrote: post #193
User23 wrote: post #184

Earlier quoted context omitted.

> 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…

Yes, I will concede that of course PTS can be used in a "first the invariants, then the code" way, and so my distinction doesn't make much sense here. Nevertheless, PTS is for verifying imperative programs, and if whenever possible, I prefer reasoning about more elegant and simple mathematical objects instead.

I find a lattice of functions from a predicate to another predicate to be about as simple as possible for describing the problem space. I’ve still got a lot to learn, but given that state is a reality for the computing automata we can actually build I like an abstraction that captures it directly.

I have found this to be an interesting exchange of ideas and I appreciate your taking the time to answer my queries. Thanks!

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

#195

Post by mbrodersen »

practal wrote: post #190
mbrodersen wrote: post #188

Earlier quoted context omitted.

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/

Same with me. It is really interesting stuff!

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

#196

Post by mbrodersen »

practal wrote: post #191
mbrodersen wrote: post #189

Earlier quoted context omitted.

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.

I've heard of nuPRL, it seems to be also based on type theory, with special emphasis on constructivity. It's basically the same as Coq, foundationally. At a summer school Bob Constable once said that he would refuse to fly in a plane with software which had been verified formally using classical logic, instead of constructive logic... Well, I wouldn't mind an intuitionistic verification, but I'd definitely take even…

No it is actually quite different. nuPRL starts with an untyped programming language and you then prove that an untyped expression has a certain behaviour. The behaviour is called a Type but it is fundamentally a very different idea from Martin Loff type theory (IMHO). They do say that it is MLTT, and in principle they are right, but MLTT is as powerful as set theory so that is true of anything mathematically. LEAN for example supports non-constructive mathematics. But it is still based on a type theory. Anyways … YouTube has a great talk about the ideas: https://www.youtube.com/watch?v=LE0SSLizYUI

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

#197

Post by [deleted] »

hwayne wrote: post #186
guerrilla wrote: post #181

Earlier quoted context omitted.

> 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".

[deleted]

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

#198

Post by nottorp »

Thiez wrote: post #175
nottorp wrote: post #121

You can prove that an algorithm is correct most of the time (yes, halting and decidability but for practical purposes you mostly can). How do you prove an event driven application is correct?

Modelling your application as a state machine will allow you to use model checking to prove various properties about your model. Proving that your program is equivalent (for some chosen definition of equivalence) to the state machine is left as an exercise for the reader.

> Proving that your program is equivalent (for some chosen definition of equivalence) to the state machine is left as an exercise for the reader.

"It's obvious" :)

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

#199

Post by blainehansen »

akomtu wrote: post #53

I suspect that verifying software is a lot like the termination problem of Turing machines: the more useful properties you want to verify, the closer it is to NP completeness. So a practical verifier should limit its scope to a modest subset of software and settle on verifying sonething with a sufficient degree of confidence, which is lower than 100%.

Hi, maintainer/author of Magmide here: https://github.com/magmide/magmide#isnt-is-undecidable-to-pr...

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

#200

Post by blainehansen »

88913527 wrote: post #19

For functional stuff, sure, but I don't think this is achievable within the UI domain. CSS rules have implementation details that change how you write it (some problems have workarounds), for example there's a documented set of issues in flex implementations maintained here: https://github.com/philipwalton/flexbugs It might be practical and possible to become mainstream for some domains, but it's doubtful for others.…

Hi, maintainer/author of Magmide here: https://github.com/magmide/magmide#isnt-most-software-too-fu...
Post reply on HN