diff options
author | Leonardo Santiago <[email protected]> | 2024-06-02 08:50:55 -0300 |
---|---|---|
committer | Leonardo Santiago <[email protected]> | 2024-06-02 08:50:55 -0300 |
commit | 59a513c4dba6c8ff2b183d966ab6ca2dcdf5cce8 (patch) | |
tree | 3a56ec7e65ebc072d8b601786a31b616239672d4 /content | |
parent | c6c225f4746565977300982f97dda02758a8d11b (diff) |
fix typos
Diffstat (limited to 'content')
-rw-r--r-- | content/blog/rust-is-not-about-memory-safety.md | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/content/blog/rust-is-not-about-memory-safety.md b/content/blog/rust-is-not-about-memory-safety.md index abbc1d4..138c9ba 100644 --- a/content/blog/rust-is-not-about-memory-safety.md +++ b/content/blog/rust-is-not-about-memory-safety.md @@ -3,7 +3,7 @@ title = "rust is not about memory safety" author = ["santi"] description = "a lower case only blog, purely for aesthetics" publishDate = 2024-06-01T00:00:00-03:00 -lastmod = 2024-06-01T20:38:19-03:00 +lastmod = 2024-06-02T08:50:45-03:00 tags = ["rust", "correctness"] draft = false +++ @@ -40,7 +40,7 @@ framing it this way really exposes the fragility of C, because undefined behavio language designers and compiler developers are by no means dumb, and yes, they know much, much more than me about these problems. undefined behavior exists exactly because there must be parts of your code that your compiler **must** assume that aren't possible, so that it can correctly compile. for example, let's say that you inadvertently try to dereference a pointer that you have no knowledge about. the C compiler simply does not have enough information to know if it is `NULL`, if it is still pointing to valid memory, or if the memory has been initialized, so it's approach is to simply emit code **as if** it was a valid, initialized, non-null pointer. -it is essential to realize that this is an **assumption**, and in almost most cases, it does not care whether or not it actually was actually still valid, so writing to it may have a myriad of effects of different effects (none of which are the compiler's concerns). sometimes, your system might correctly intercept a read/write from invalid/null memory and raise you a signal, but that is not guaranteed. +it is essential to realize that this is an **assumption**, and in almost most cases, the compiler does not care whether or not it actually was actually still valid, so writing to it may have a myriad of effects of different effects (none of which are the compiler's concerns). sometimes, your system might correctly intercept a read/write from invalid/null memory and raise you a signal, but that is not guaranteed. and there are a huge number of tools to aid in finding undefined behavior in a code base, it's just that @@ -66,7 +66,7 @@ from this definition of **correctness** we can also derive a semantically useful what the regex example makes clear is that the key to correctness is to make your language tight enough to have defined and **desired** output for all possible inputs. this is not to say that it won't raise errors; much to the contrary, it must have parser errors saying that some strings aren't valid regexes. instead, it means that all errors are **predictable**, and **well defined** (in some sense). -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 [is not regular](https://en.wikipedia.org/wiki/Pumping_lemma_for_regular_languages#Use_of_the_lemma_to_prove_non-regularity), so no matter how hard you try it will never solve it. +you, as the programmer, are then in charge of ensuring that the resulting regex program actually solves the problem you have at hand. 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 [is not regular](https://en.wikipedia.org/wiki/Pumping_lemma_for_regular_languages#Use_of_the_lemma_to_prove_non-regularity), 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 [well specified languages](https://www.open-std.org/jtc1/sc22/wg14/www/docs/n1256.pdf), which is what makes it suitable for writing formally verifiable programs [^fn:3]. @@ -76,7 +76,7 @@ not only that, but rust languages features makes it so, so much easier to write note that i never ever talked about memory safety. even in a world where C wasn't in fact full of memory vulnerabilities, rust would still be miles better, because it statically assures you that the **meaning of your program is tightly reproduced by the code you've written**. it is, by design, more correct than C, and the only way a problem can possibly happen is by side stepping rust static checks by using `unsafe`. -it is just a happy coincidence that this leads to a language that isn't garbage collected, that is relatively lean, fast, easy to embed, has good ergonomics and that enables you to write asynchronous and multi-threaded programs. these properties are awesome to boost rust to a very well regarded status between developers, but aren't at all related to languages that enable you to build reliable, correct software. out of curiosity, i'd happily defend the case that [coq](https://coq.inria.fr/) is also one of these languages, and it absolutely does not hold any of these any of those. +it is just a happy coincidence that this leads to a language that isn't garbage collected, that is relatively lean, fast, easy to embed, has good ergonomics and that enables you to write asynchronous and multi-threaded programs. these properties are awesome to boost rust to a very well regarded status between developers, but aren't at all related to languages that enable you to build reliable, correct software. out of curiosity, i'd happily defend the case that [coq](https://coq.inria.fr/) is also one of these languages, and it absolutely does not hold any of these properties. ## software engineering as a craft {#software-engineering-as-a-craft} |