diff options
Diffstat (limited to 'blog.org')
| -rw-r--r-- | blog.org | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -30,7 +30,7 @@ if you feel like smugly responding to any of my posts (or just want to kindly se - [[https://www.linkedin.com/in/leonardo-ribeiro-santiago/][linkedin]] - [[https://github.com/o-santi][github]] -this blog was built using emacs' excelent org-mode and [[https://github.com/gohugoio/hugo][hugo]] (with the [[https://github.com/janraasch/hugo-bearblog][bearblog theme]]). +this blog was built using emacs' excelent org-mode and [[https://github.com/gohugoio/hugo][hugo]] (with the [[https://github.com/janraasch/hugo-bearblog][bearblog theme]]), and it's source code is openly available [[https://github.com/o-santi/blog][here]]. * blog :PROPERTIES: @@ -92,7 +92,7 @@ what the regex example makes clear is that the key to correctness is to make you you, as the programmer, is then in charge of ensuring that the resulting regex program actually solves the problem you have at hands. want to match 3 words of 2 digit numbers followed by a capital letter? great, they can do that. want to match balanced parenthesized expressions? sadly, regex is incapable of ever solving that, because that language [[https://en.wikipedia.org/wiki/Pumping_lemma_for_regular_languages#Use_of_the_lemma_to_prove_non-regularity][is not regular]], so no matter how hard you try it will never solve it. -in a way, there's a beauty in how C sidesteps this: it defines one of the possible program outputs as being /undefined/, and it is on the programmers behalf to tightly ensure that the program has 0 paths to /undefined behavior/. in fact, it is probably one of the most [[https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf][well specified languages]], which is what makes it suitable for writing formally verifiable programs [fn::through the use of external tools like Coq's [[https://vst.cs.princeton.edu/veric/][verifiable C series]]]. +in a way, there's a beauty in how C sidesteps this: it defines one of the possible program outputs as being /undefined/, and it is on the programmers behalf to tightly ensure that the program has 0 paths to /undefined behavior/. in fact, it is probably one of the most [[https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf][well specified languages]], which is what makes it suitable for writing formally verifiable programs [fn::through the use of external tools like coq's [[https://vst.cs.princeton.edu/veric/][verifiable C series]]]. the main strength of rust, and where it differs from all mainstream languages, is that it has a very clear focus on program *correctness*. the raison d'être of the borrow checker is statically assuring that all references are pointing to valid memory, such that it is literally impossible for any borrow be null or to point to some freed memory (modulus [[https://github.com/Speykious/cve-rs][implementation errors of course]]). this completely rules out this possibility of bugs from the language we're trying to "parse". remember the C excerpt from above, where i said that the compiler should rule out the program as invalid? well, it is literally impossible to write that sort of program in rust, because one cannot construct a ~NULL~ reference. |