diff options
author | Leonardo Santiago <[email protected]> | 2024-10-26 18:44:22 -0300 |
---|---|---|
committer | Leonardo Santiago <[email protected]> | 2024-10-26 18:44:22 -0300 |
commit | 8609f19617a98c8aab3ecf48dd5caed67497c952 (patch) | |
tree | bab5334e9c2f146f03ed209de9324f486cbd494d | |
parent | daca93760b5e4b250eabe026e35865d2932937ec (diff) |
test commit
-rw-r--r-- | blog.org | 2 |
1 files changed, 1 insertions, 1 deletions
@@ -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: |