summaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorLeonardo Santiago <[email protected]>2024-10-26 18:44:22 -0300
committerLeonardo Santiago <[email protected]>2024-10-26 18:44:22 -0300
commit8609f19617a98c8aab3ecf48dd5caed67497c952 (patch)
treebab5334e9c2f146f03ed209de9324f486cbd494d
parentdaca93760b5e4b250eabe026e35865d2932937ec (diff)
test commit
-rw-r--r--blog.org2
1 files changed, 1 insertions, 1 deletions
diff --git a/blog.org b/blog.org
index 0228336..58f764f 100644
--- a/blog.org
+++ b/blog.org
@@ -117,7 +117,7 @@ the part that programmers usually get paid millions of dollars for is the step *
it is not by chance that Yang et al. could only find measly 9 bugs after 6 CPU years of fuzzing in [[https://compcert.org/man/manual001.html][compcert]], a formally verified c compiler (written in coq), where as in gcc and clang, they [[https://users.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf#subsection.3.2][found and reported more than 300]]. all these 9 bugs where in the unverified front end of the compiler (the parser), and there were literally 0 middle end (compiler passes and AST translations) bugs found, which is unheard of. this is not by chance, they've spent many years writing proofs that all of their passes are correct, safe, and preserve the meaning of the original program.
i really think software developers should strive for that kind of resilience, which i believe can only be achieved through properly valuing *correctness* . i don't think it is reasonable to expect that all software be built using coq and proving every little bit of it (due to business constraints) but i think that rust is a good enough language to start taking things more seriously.
-** exploiting thunks for fun and profit
+
* COMMENT Local Variables :ARCHIVE: