2 ms·
For the same reason Google does not formally prove the correctness of their code. It's technically feasible but impossibly complex to actually achieve. Fully f
by qsort 5y ago
For the same reason Google does not formally prove the correctness of their code. It's technically feasible but impossibly complex to actually achieve.
Fully formalizing a proof with a tool like Coq or Isabelle is in and of itself a nontrivial problem.
- lostmsu 5y agoThere are multiple ways in which Google Mail while behaving incorrectly still be usable. But a theorem is not only useless if it is incorrect, it is dangerous.