3 ms·
> But "verified" software often means formal mathematical verification, and that is orthogonal to if the source is open. I think there may be cross-talk here r
by lomnakkus 10y ago
> But "verified" software often means formal mathematical verification, and that is orthogonal to if the source is open.
I think there may be cross-talk here related to who's doing the verifying too. I think the parent is assuming "verification" would imply that a 3rd party could verify the software in question. AFAIUI it's currently nowhere near practical for a 3rd party to verify closed-source software of any non-trivial size. (Correct me, if I'm wrong, obviously.)
It's still a research problem even for open-source unless the software is built with formal verification in mind (for example in Coq or Agda), but at least there's an existence proof that it's possible to do for non-trivial software (see CompCert C). That was still a multi-year effort and it's still a somewhat (architecturally) simple program as compilers tend to be.
- nl 10y agoDownthread tptacek talks about how his company does verification of binary images. I assume there are limits to what is possible, but that's really the same as any verification approach. I do agree that 'who is verifying' is a valid way of looking at it too. Regardless, it's pretty clear that tptacek means formal verification. Edit: see http://arieg.bitbucket.org/pdf/seahorn.pdf http://arieg.bitbucket.org/pdf/seahorn.pdf
- tptacek 10y agoMy company doesn't do this. But many companies specialize in it.
- jsudhams 10y agoIf whatsapp allows few experts or companies access to code they can always verify but the issue is centrally hosted , that is the issue not open or close. If i can build software on and host on my server that might be better
- jsudhams 10y agoIf whatsapp allows few experts or companies access to code they can always verify but the issue is centrally hosted , that is the issue not open or close. If i can build software on and host on my server that might be better