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

71–80 of 203 posts

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

#71

Post by guerrilla »

petergeoghegan wrote: post #63
guerrilla wrote: post #44

Earlier quoted context omitted.

> Software can still be provably correct and have security holes resulting from an insecure definition of "correct." Formal verification does not solve security. Nirvana fallacy. The point is that it can be much better and eliminate ALL non-design bugs. > Please explain how a company could profit more if formal verification does not bring more revenue than it costs? You seem to be assuming that revenue will appear th…

> Nirvana fallacy. The point is that it can be much better and eliminate ALL non-design bugs. Serious question: do you really believe that? > That's just stupid. Show me the studies. There is a kind of HAL-9000 quality to many of these arguments. Formal verification is perfect by definition. The fact that it hasn't had very much impact in the real world is all the more evidence of the world being full of wicked peopl…

> Serious question: do you really believe that?

I mean it's a fact, so yes. You can prove programs are correct. The only possible flaw they can have is the specification is wrong.

> The fact that it hasn't had very much impact in the real world is all the more evidence of the world being full of wicked people.

That's very much not what I said. There may be many reasons. Assuming some conclusion without actual research is braindead. Cost-benefit analysis is not the only reason things do/don't happen in businesses and we have no idea whether that's the reason here. It's an empirical question that requires actual research, not a priori jacking off.

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

#72

Post by yjftsjthsd-h »

moeris wrote: post #26
michaelsbradley wrote: post #15

Earlier quoted context omitted.

Evil: the privation of a good that should be present. It is the lack of a good that essentially belongs to a nature; the absence of a good that is natural and due to a being. Evil is therefore the absence of what ought to be there. https://www.catholicculture.org/culture/library/dictionary/i... https://en.m.wikisource.org/wiki/Catholic_Encyclopedia_(1913...

Quoted post unavailable.

> Like much of Christian thought, this is lazy to the extreme.

> But it nonetheless fits this idiotic definition.

Your personal bias is showing, to the point of going against the site guidelines; both 'When disagreeing, please reply to the argument instead of calling names. "That is idiotic; 1 + 1 is 2, not 3" can be shortened to "1 + 1 is 2, not 3."' and, y'know, literal religious flame warring.

Also, you're either wrong or at least not correct;

> Is ice cream that has thawed evil? No, rather obviously.

You are of course welcome to argue that it's not, but yes, there are Christians who would/do make this exact argument; they might not claim that ice cream has the capacity to be willfully evil, but they would absolutely argue that ice cream melting is Wrong and a symptom of a Fallen world (in the sense of "fallen creation"), and that in a Good world ice cream would not melt.

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

#73

Post by milkey_mouse »

hn_urbit_thr123 wrote: post #43

Is it even realistic to make a provably secure/stable applications on an OS like windows or linux? This (provable correctness of programs, at the expense of performance) is one of the explicit design goals or urbit. I know HN hates urbit and don't want to rehash that, but it seems like a good goal for some use cases and I'm not sure it's possible to achieve without building the OS around it.

Urbit has not put much effort into security, for some reason. To be fair, they don't claim their runtime is secure (yet)[1]. The process downloading and executing code from the network is not sandboxed with seccomp or anything similar, and its "jets" are unverified C libraries which any of this code is allowed to call into. They could sandbox it pretty easily (the worker process which runs third-party code only talks to a host process and not the rest of the world, so it could probably be run under seccomp, not even seccomp-bpf) which makes it all the more surprising that they haven't.

Urbit has also had (and almost certainly still has) bugs where jets give different results than the code they're supposed to accelerate (a "jet mismatch") [2]. I agree that its "axiomatic" bytecode would lend itself well to verification theoretically, but Urbit as she is spoke is not anywhere close. They also at least historically seemed somewhat hostile towards academic CS research (including formal methods) probably for weird Moldbug reasons.

[1]: https://urbit.org/faq#:~:text=The%20security%20of%20the%20ru....

[2]: https://urbit.org/blog/common-objections-to-urbit#:~:text=Ye...

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

#74

Post by yjftsjthsd-h »

So this actually looks really neat if it works. However, hopefully in the spirit of constructive criticism, I would be very nervous about sticking this in big letters at the top of the introduction:

> Software can literally be perfect

because that is a wonderful way to get people to invest in really robust, excellent, high-quality software - and then trust it blindly and ignore that even if everything goes well and the software is itself perfect, and the verification has no bugs, and the model that it perfectly implements actually maps the problem space correctly, it will still run on fallible hardware, interfacing with other software that is imperfect, taking direction and data from humans who can make mistakes. Now to the author's credit! Further down, under "Do you think this language will make all software perfectly secure?" and "Is logically verifying code even useful if that code relies on possibly faulty software/hardware?", this is discussed. And I think the writer actually does appreciate the limits of what this can actually do, and I very much appreciate them explaining that in what I'd call clear terms. Just... maybe don't headline with a claim like that when it has caveats and people are liable to read the claim and ignore the caveats?

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

#75

Post by petergeoghegan »

guerrilla wrote: post #71
petergeoghegan wrote: post #63

Earlier quoted context omitted.

> Nirvana fallacy. The point is that it can be much better and eliminate ALL non-design bugs. Serious question: do you really believe that? > That's just stupid. Show me the studies. There is a kind of HAL-9000 quality to many of these arguments. Formal verification is perfect by definition. The fact that it hasn't had very much impact in the real world is all the more evidence of the world being full of wicked peopl…

> Serious question: do you really believe that? I mean it's a fact, so yes. You can prove programs are correct. The only possible flaw they can have is the specification is wrong. > The fact that it hasn't had very much impact in the real world is all the more evidence of the world being full of wicked people. That's very much not what I said. There may be many reasons. Assuming some conclusion without actual researc…

> You can prove programs are correct. The only possible flaw they can have is the specification is wrong.

So specifications are kind of like programs?

Have you heard of logical positivism?

> That's very much not what I said. There may be many reasons.

My point was that it always seems to be some external factor. That strikes me as being very convenient.

> Assuming some conclusion without actual research is braindead.

I didn't think I assumed anything. Like anybody else, I have many things that I need to assess in my day to day life, and often deal with considerable uncertainty.

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

#76

Post by picardo »

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?

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/

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

#77

Post by abeyer »

AlotOfReading wrote: post #69
Hizonner wrote: post #64

Earlier quoted context omitted.

I agree it sounds like pretty naive enthusiasm. Not just about how hard the formal verification problem is, but about how hard it is to get ANY kind of programming system up to the point where it's actually usable. However, every time somebody starts going negative on formal verification by talking about decidability, I get itchy. Sure, we know, all interesting properties of programs in all interesting languages are…

I disagree that most interesting programs don't need things that are Hard to Verify. For instance, approximately every C program would benefit from correct pointer analysis, yet this remains an open research question. For a personal example, I had a recent lunch interaction with our security team about some work I wanted to do formally verifying bits of a bootloader we have. Halfway through the conversation, one of t…

Sure, but how many of those C programs are inherently hard to verify vs how many of them are hard because they happen to be built with tools that make them hard to verify?

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

#78

Post by jbaba101 »

I want to understand what is verification process? How would programming will take new step forward if this is achieved? I have been programmer for a while but I don't understand context and discussion around verification. Please point me any useful resources which can give me deep understanding of what's being discussed here.

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

#79

Post by xavxav »

Honestly, to me this project is a means seeking an end, the same way JS devs love to play around with frontend frameworks, the author saw a bunch of shiny powerful (highly complex) tools and decided that combining them all was the solution to our problems.

I don't want to discourage them from learning Iris, or designing a dependently typed language, but I really think that's missing the difficulty in formal verification.

I think the two areas that need focus are: ease of specification and automation. In short, we need to lower the cost of verifying a line of code, by at least an order of magnitude. These two objectives are also directly opposed to the direction Magmide sets as the goal. Ease of specification means we want to use the least amount of seperation logic possible, and hide it from the user if possible. Doing proofs / writing specs in seperation logic sucks and not for interesting reasons. Automation means favoring simpler logics, specifically we want to stick as much as possible to FOL since that's where we have good automation. By doing everything in a rich dependently typed language from the start it also makes it harder to do incremental verification, I think there is a lot of value in having a 'pyramid of trust' with more and more powerful tools which take you up a level of trust and verification, potentially requiring more input from engineers as they go up.

Finally, I think there's a lot of potential to explore in the interfaces we use to write, read, and debug proofs. I don't think tactic languages (as exist today) are the last word, and I think we should be doing a lot more interesting things to interface with and explore the proofs.

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

#80

Post by topspin »

AnimalMuppet wrote: post #51
marcosdumay wrote: post #23

Earlier quoted context omitted.

We use static type systems all the time, as well as specialized checkers and linters, and none of those showed themselves to have "costs greater than the cost of the bugs". And none of them are even nearly similar to "demanding your house have all perfect right angles and completely level surfaces". Do you have any reason to believe that all the rest of the verification theory is completely impractical when every pie…

This is kind of like AI. When something succeeds in general practice, it is no longer "formal verification". Now it's "robust type systems" and "static analysis tools". Those provide formal verification of some aspects of the code. And that's great! It's progress! Full formal verification is (probably?) still a long way off, depending on your definition of "full". (My definition would be one where Knuth's observation…

> This is kind of like AI. When something succeeds in general practice, it is no longer "formal verification". Now it's "robust type systems" and "static analysis tools".

Yes indeed. That is insightful.

Is there a name for this process?

Post reply on HN