Hacker News Reader

Comment by agentultra | Hacker News Reader

It is wishful thinking. Iris is cool and all but extracting useful programs from proofs is still an open research area. I don’t want to discourage someone from trying but it would help to be pragmatic.

At least the author seems somewhat aware of this when they describe the repo as a collection of earnings and ravings.

I’ve been interested in this since 2015 or so and even then the cost of doing formal verification had come down a lot. It has continued the downward trend. But we are still a long way from a language that industry programmers can use to write proofs and extract programs from.

One of the major challenges will be teaching industry programmers how to write proofs and convincing them that they want to do this.

View on HN

> One of the major challenges will be teaching industry programmers how to write proofs and convincing them that they want to do this.

"Industry programmers" are pretty far from being a monolith. There are a myriad of different approaches to testing, many of which are domain specific, for all kinds of reasons.

Usually the way that a new testing tool gets adapted is that individual programmers or companies that adapt the tool appear to have a competitive advantage over those that don't. The results generally speak for themselves, at least after a time.

Practically everybody that might use formal verification has already chosen to not go to certain lengths to increase reliability. They're already making an economic trade-off -- even with safety critical systems, or in domains where the cost of bugs is extraordinarily high. Why shouldn't formal verification be assessed in the same way?

Because many of the costs of their irresponsible practices are externalized.

> Because many of the costs of their irresponsible practices are externalized.

I'm sure that that's true in at least some important cases. I don't see what it has to do with formal verification.

To be honest, extracting Rust programs from Iris would be the easy part here. The hard part is, well... using Iris. If you've used it much you know what I mean.

Isn't this what matlab and other tools like it try to deliver to?

Most programs I've seen in the industry use matlab and simulink for formal verification (of course, still ignoring the hardware design part) and I'm asking myself how many dependencies the verification should have.

I mean, even a simple Hello World program could escalate really quickly once you have to deal with TTY quirks or say, %X as a printf parameter.

The issue I see with matlab's approach is that it has a huge set of assumptions in its own compiler chain, which I guess is the core problem of all ABI compatible outputs.

Not at all. See CompCert, seL4, F* (F-star) and Coq for examples of how it is done.

Reply on news.ycombinator.com