From: Ralf Jung Date: Thu, 24 Jul 2025 15:34:23 +0000 (+0200) Subject: mention proving X-Git-Url: https://git.ralfj.de/web.git/commitdiff_plain/4a2c7e8d896f626c7c83488fcb06d59845f378df?ds=inline;hp=f2e0cb781b6f9b1de1abd6da079cd2022cc9104f mention proving --- diff --git a/personal/_posts/2025-07-24-memory-safety.md b/personal/_posts/2025-07-24-memory-safety.md index c12a125..6c4c7f6 100644 --- a/personal/_posts/2025-07-24-memory-safety.md +++ b/personal/_posts/2025-07-24-memory-safety.md @@ -127,6 +127,7 @@ There's no meaningful sense in which this can be further subdivided into memory In practice, of course, safety is not binary, it is a spectrum, and on that spectrum Go is much closer to a typical safe language than to C. It is plausible that UB caused by data races is less useful for attackers than UB caused by direct out-of-bounds or use-after-free accesses. But at the same time I think it is important to understand which safety guarantees a language reliably provides, and where the fuzzy area of trade-offs begins. +I am in the business of [*proving*](https://research.ralfj.de/thesis.html) safety claims of languages, and for Go, there's not much one could actually prove. I hope this post helps you to better understand some the non-trivial consequences of the choices different languages have made.[^go] :) [^go]: In case you are wondering why I am focusing on Go so much here... well, I simply do not know of any other language that claims to be memory safe, but where memory safety can be violated with data races. I originally wanted to write this blog post years ago, when Swift was pretty much in the same camp as Go in this regard, but Swift has meanwhile introduced "strict concurrency" and joined Rust in the small club of languages that use fancy type system techniques to deal with concurrency issues. That's awesome! Unfortunately for Go, that means it is the only language left that I can use to make my point here. This post is not meant to bash Go, but it is meant to put a little-known weakness of the language into the spotlight, because I think it is an instructive weakness.