|
|
|
|
|
|
by Jweb_Guru
3117 days ago
|
|
|
A best-in-class, hard-real-time, preemptible operating system has been formally verified (along with many other components).
CompCert exists. Iris progresses apace. Every day, newer and more complex formal systems are proved correct. I don't really buy the "logic fails at sufficient complexity" argument. By all accounts, it's succeeded where people have put in the effort. |
|
|