The reality is that programming is an engineering endeavor, and in the face of limited resources, we have to choose the tools that can offer realistic benefits now.
Formal verification is not that tool for most projects right now. Would instagram or even facebook be better off? Most people would, correctly, say no.
And ultimately in the end, nearly all software (including quite a bit of open source software!) is written in pursuit of business reasons, and has to answer to that.
I'd think the security of Facebook privacy settings will be improved by, for example, lightweight modelling using Alloy. Alloy would catch bugs like this one:
I just had a quick look at Alloy ([0]), and I'm interested in how it could be integrated into the software development process -- once you're confident about your Alloy model, you have to transfer it to working code somehow. I'd try to use both "fact" and "assert" statements from Alloy code as assertions in my production code (e.g. Python or Java). How is this usually done?
The reality is that programming is an engineering endeavor, and in the face of limited resources, we have to choose the tools that can offer realistic benefits now.
Formal verification is not that tool for most projects right now. Would instagram or even facebook be better off? Most people would, correctly, say no.
And ultimately in the end, nearly all software (including quite a bit of open source software!) is written in pursuit of business reasons, and has to answer to that.