|
|
|
|
|
|
by mkleczek
1485 days ago
|
|
|
Just having a language that allows you to prove things does not mean it is possible to prove them. We still don't know if it is possible to build a provably correct multi-tasking OS or a web browser without security vulnerabilities. If it was easy we would already have one written in FStar or Idris. While admiring all the work done by Project Everest - the fact is that it is a
multi-year project (I first read about it about 3-4 years ago and it was already under way) with a very limited scope - it is more of an evidence of difficulties of writing correct software. |
|
|