3 ms·
Also a C compiler (https://compcert.org/ https://compcert.org/). I did exaggerate bit in saying that anything non-trivial is "nearly impossible". However, both
by armchairhacker 3y ago
Also 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.