3 ms·

It probably depends on your trust assumptions and requirements. Ideally we write formally provable code for a formally proven compiler to run on a formally pro

It probably depends on your trust assumptions and requirements. Ideally we write formally provable code for a formally proven compiler to run on a formally proven OS/bios/hardware. But some use cases require safe client code that will nevertheless run on unsafe OS and hardware. Client-side and some server-side cryptocurrency apps are one example that comes to mind. Probably banking apps too. It's still useful to write them in strongly typed languages amenable to formal verification, even though they'll be running on unverified Windows, Linux, MacOS and smartphones. Also we really need OS's, firmware, etc. written in languages amenable to formal verification, but given the massive lockin of the mainstream options, that's a pipedream for now. But a worthy long-term goal.

tsimionescu 7y ago
I'm not sure that there are languages more or less amenable to full formal verification. Formal verification of a system is such a complex task that the language-level details are unlikely to be a significant proportion of the effort. You can also look at existing formally verified software and probably confirm my assumption - there is likely as much formally verified C code (a weakly-typed, memory unsafe language) as formally-verified Haskell code. And I do not agree at all that a formally verified banking app is a good idea. It would likely be so difficult to do that by the time it is finished it no longer runs on any current version of any OS. Formal verification is just too hard to be worth it. There are better methods of ensuring software correctness that are far less costly. Maybe something will be discovered in the future that will make it easier, but for now formal verification of any piece of software more complex than a few hundred lines of code is a multi-year research-level project.

tsimionescu 7y ago

I'm not sure that there are languages more or less amenable to full formal verification. Formal verification of a system is such a complex task that the language-level details are unlikely to be a significant proportion of the effort. You can also look at existing formally verified software and probably confirm my assumption - there is likely as much formally verified C code (a weakly-typed, memory unsafe language) as formally-verified Haskell code. And I do not agree at all that a formally verified banking app is a good idea. It would likely be so difficult to do that by the time it is finished it no longer runs on any current version of any OS. Formal verification is just too hard to be worth it. There are better methods of ensuring software correctness that are far less costly. Maybe something will be discovered in the future that will make it easier, but for now formal verification of any piece of software more complex than a few hundred lines of code is a multi-year research-level project.