4 ms·
tl;dr; Yes. But trying to prove anything beyond very tiny functions (especially things like GUIs and world state) is near-impossible and massive overkill. Also,
by armchairhacker 3y ago
tl;dr; Yes. But trying to prove anything beyond very tiny functions (especially things like GUIs and world state) is near-impossible and massive overkill. Also, you'll need to work around termination checking (even if your functions always terminate, proving that is another matter).
Theorem provering languages are cool. Being able to prove the absence of bugs, enforce complex invariants, etc. is cool and useful in certain cases (like cryptography and safety-critical software). But it's also very hard, at least state-of-the-art, so often I feel writing good tests is better.
- MichaelZuo 3y agoDidn't some Australian group manage to prove a simplified kernel?
- throwaway17_17 3y agoseL4 has a formal correctness prof that was developed by NICTA. The project started in 2006 and the formal proof and artifact was submitted in 2009. The elements of the implementation and resulting qualities present during run time are well defined but are limited to exactly those properties the project chose, like lack of dead and livelocks, arithmetic based exceptions, and buffer overruns. L4 is less a simplified kernel and more of a microkernel, but it is fully general purpose. One of the neat things they did was transport memory/resource management to userland and maintain a strict capabilities scheme for ensuring correctness. The other was the cost estimate they claim, which was something like a 60% cost saving for doing the formally verified programming compared to standard ‘high assurance’ programming. It was a cool project but is not often used to support further pushes into more general systems level applicability of ‘theorem proving’ based programming languages.
- RetroTechie 3y agohttps://sel4.systems https://sel4.systems Working on a number of platforms, verified on some. Multicore support is an ongoing effort afaict. An OS built on this kernel is still subject to some assumptions (like, hardware working correctly, bootloader doing its job, etc). But mostly those assumptions are less of a problem / easier to prove than the properties of a complex software system. As I understand it, guarantees that seL4 does provide, go well beyond anything else currently out there.
- MichaelZuo 3y agoThanks for the link, that's pretty advanced stuff then.
- armchairhacker 3y agoAlso a C compiler (https://compcert.org/ https://compcert.org/). I did exaggerate bit in saying that anything non-trivial is "nearly impossible". However, both CompCert and sel4 took a few years to develop, whereas it would only take months if not weeks to make versions of both which aren't formally verified but heavily tested.
- MichaelZuo 3y agoIt demonstrates that proving a full featured operating system, as complex as Windows 7 for example, is within the realm of possibility. It would just likely take a Manhattan project equivalent, with a truly unlimited budget.
- deterministic 3y agoIt takes years to develop a quality C compiler. I am a professional compiler writer and the difference between a toy compiler and a production compiler is vast.
- AnimalMuppet 3y agoYeah, to me that's the real question: Can the language of proof assistance be efficiently used for general purpose programming? As you say, right now it's too hard for general use.
- deterministic 3y agoNope. CompCert is an example of a small team of people writing a proven correct C compiler. seL4 is another. The problem is training. Universities are currently not training CS students to prove code correct. This will change. But slowly.