1. 51
  1.  

  2. 21

    So I think I’m a bit late for the big go and rust and garbage collection and borrow checker discussion, but it took me a while to digest, and came up with the following (personal) summary.

    Determining when I’m done with a block of memory seems like something a computer could be good at. It’s fairly tedious and error prone to do by hand, but computers are good at monotonous stuff like that. Hence, garbage collection.

    Or there’s the rust approach, where I write a little proof that I’m done with the memory, and then the computer verifies my proof, or rejects my program. Proof verification is also something computers are good at. Nice.

    But writing the proof is still kind of a pain in the ass, no? Why can’t I have computer generated proofs? I have some memory, I send it there, then there, then I’m done. Go figure out the refs and borrows to make it work, kthxbye.

    1. 18

      But writing the proof is still kind of a pain in the ass, no? Why can’t I have computer generated proofs? I have some memory, I send it there, then there, then I’m done. Go figure out the refs and borrows to make it work, kthxbye

      I’m in the middle of editing an essay on this! Long story short, proving an arbitrary code property is undecidable, and almost all the decidable cases are in EXPTIME or worse.

      1. 10

        I’m kinda familiar with undecidable problems, though with fading rigor these days, but the thing is, undecidable problems are undecidable for humans too. The impossible task becomes no less impossible by making me do it!

        I realize it’s a pretty big ask, but the current state of the art seems to be redefine the problem, rewrite the program, find a way to make it “easy”. It feels like asking a lot from me.

        1. 10

          The problem is undecidable (or very expensive to decide) in the most general case; what Rust does is solve it in a more limited case. You just have to prove that your usage fits into this more limited case, hence the pain in the ass. Humans can solve more general cases of the problem than Rust can, because they have more information about the problem. Things like “I only ever call function B with inputs produced from function A, function A can only produce valid inputs, so function B doesn’t have to do any input validation”. Making these proofs without computer assistance is no less of a pain in the ass. (Good languages make it easy to enforce these proofs automatically at compile or run time, good optimizers remove redundant runtime checks.)

          Even garbage collectors do this; their safety guarantees are a subset of what a perfect solution would provide.

          1. 3

            “Humans have more information about the problem”

            And this is why a conservative borrower checker is ultimately the best. It can be super optimal, and not step on your toes. It’s up to the human to adjust the lifetime of memory because only the human knows what it wants.

            I AM NOT A ROBOT BEEP BOOP

          2. 3

            Humans have a huge advantage over the compiler here though. If they can’t figure out whether a program works or not, they can change it (with the understanding gained by thinking about it) until they are sure it does. The compiler can’t (or shouldn’t) go making large architectural changes to your code. If the compiler tried it’s hardest to be as smart as possible about memory, the result would be that when it says “I give up, the code needs to change” the human who can change the code is going to have a very hard time understanding why and what they need to change (since they haven’t been thinking about the problem).

            Instead, what Rust does is apply as intelligent a set of rules they could that produce consistent understandable results for the human. So the compiler can say “I give up, here’s why”. And the human can say “I know how the compiler will work, it will accept this this time” instead of flailing about trying to convince the compiler it works.

            1. 1

              I realize it’s a pretty big ask

              I’ve been hearing this phrase lately “big ask” from business people generally, seems very odd to me. Is it new or have I just missed it up to now?

              1. 2

                I’ve been hearing it from “business people” for a couple years at least, I assume it’s just diffusing out slowly to the rest of society.

                The new one I’m hearing along these lines is “learnings”. I think people just think it makes them sound smart if they use different words.

                1. 1

                  A “learning”, as a noun, is attested at least as far back as the early 1900s, FYI.

                  1. 0

                    This sort of comment annoys me greatly. Someone used a word incorrectly 100 years ago. That doesn’t mean it’s ‘been a word for 100 years’ or whatever you’re implying. ‘Learning’ is not a noun. You can argue about the merits of prescriptivism all you like, you can have whatever philosophical discussion you like as to whether it’s valid to say that something is ‘incorrect English’, but ‘someone used it in that way X hundred years ago’ does not justify anything.

                    1. 2

                      This sort of comment annoys me greatly. Someone used a word incorrectly 100 years ago. That doesn’t mean it’s ‘been a word for 100 years’ or whatever you’re implying. ‘Learning’ is not a noun.

                      It wasn’t “one person using it incorrectly” that’s not even remotely how attestation works in linguistics. And of course, of course it is very much a noun. What precisely, man, do you think a gerund is? We have learning curves, learning processes, learning centres. We quote Pope to one another when we say that “a little learning is a dangerous thing”.

                      To take the position that gerunds aren’t nouns and cannot be pluralized requires objecting to such fluent Englishisms as “the paintings on the wall”, “partings are such sweet sorrow”, “I’ve had three helpings of soup”

                      1. 0

                        ‘Painting’ is the process of painting. You can’t pluralise it. It’s also a (true) noun, the product of doing some painting. There it obviously can be pluralised. But ‘the paintings we did of the house kept improving the sheen of the walls’ is not valid English. They’re different words.

                        1. 2

                          LMAO man, how do you think Painting became a “true” noun? It’s just a gerund being used as a noun that you’re accustomed to. One painted portraits, landscapes, still lifes, studies, etc. To group all these things together as “paintings” was an instance of the exact same linguistic phenomenon that gives us the idea that one learns learnings.

                          You’re arguing against literally the entire field of linguistics here on the basis of gut feelings and ad hoc nonsense explanations.

                          1. 0

                            You’re arguing against literally the entire field of linguistics here on the basis of gut feelings and ad hoc nonsense explanations.

                            No, I’m not. This has literally nothing to do with linguistics. That linguistics is a descriptivist scientific field has nothing to do with whether ‘learnings’ is a real English word. And it isn’t. For the same reason that ‘should of’ is wrong: people don’t recognise it as a real word. Words are what we say words are. People using language wrong are using it wrong in the eyes of others, which makes it wrong.

                            1. 1

                              That linguistics is a descriptivist scientific field has nothing to do with whether ‘learnings’ is a real English word. And it isn’t. For the same reason that ‘should of’ is wrong: people don’t recognise it as a real word. Words are what we say words are.

                              Well, I hate to break it to you, but plenty of people say learnings is a word, like all of the people you were complaining use it as a word.

                              1. 0

                                There are lots of people that write ‘should of’ when they mean ‘should’ve’. That doesn’t make them rightt.

                                1. 1

                                  Yes and OK is an acronym for Oll Korrect, anyone using it as a phrase is not OK.

                                  1. 0

                                    OK has unknown etymology. And acronyms are in no way comparable to simply incorrect grammar.

                                    1. 1

                                      Actually it is known. Most etymologists agree that it came from Boston in 1839 originating in a satirical piece on grammar. This was responding to people who insist that English must follow some strict unwavering set of laws as though it were a kind of formal language. OK is an acronym, and it stands for Oll Korrect, and it was literally invented to make pedants upset. Certain people were debating the use of acronyms in common speech, and to lay it on extra thick the author purposefully misspelled All Correct. The word was quickly adopted because pedantry is pretty unpopular.

                                      1. 1

                                        What I said is that there is what is accepted as valid and what is not. Nobody educated thinks that ‘should of’ is valid. It’s a misspelling of ‘should’ve’. Nobody thinks ‘shuold’ is a valid spelling of ‘should’ either. Is this really a debate you want to have?

                                        1. 1

                                          I was (mostly) trying to be playful while also trying to encourage you to be a little less litigious about how people shuold and shuold not use words.

                                          Genuinely sorry for making you actually upset though, I was just trying to poke fun a little for getting a bit too serious at someone over smol beans, and I was not trying to make you viscerally angry.

                                          I also resent the attitude that someone’s grammatical or vocabulary knowledge of English represents an “education”.

                2. 1

                  It seems like in the last 3 years all the execs at my company started phrasing everything as “The ask is…” I think they are trying to highlight that you have input (you can answer an ask with no) vs an order.

                  In practice, of course, many “asks” are orders.

                  1. 4

                    Sure, but we already have a word for that, it’s “request”.

                    1. 4

                      Sure, but the Great Nouning of Verbs in English has been an ongoing process for ages and continues apace. “An ask” is just a more recent product of the process that’s given us a poker player’s “tells”, a corporation’s “yearly spend”, and the “disconnect” between two parties’ understandings.

                      All of those nouned verbs have or had perfectly good non-nominalized verb nouns, at one point or another in history.

                      1. 1

                        One that really upsets a friend of mine is using ‘invite’ as a noun.

                  2. 1

                    Newly popular? MW quotes this usage and says Britishism.

                    https://www.merriam-webster.com/dictionary/ask

                    They don’t date the sample, but I found it’s from a 2008 movie review.

                    https://www.spectator.co.uk/2008/10/cold-comfort/

                    So at least that old.

                3. 3

                  You no doubt know this, but the undecidable stuff mostly becomes decidable if you’re willing to accept a finite limit on addressable memory, which anyone compiling for, say, x86 or x86_64 is already willing to do. So imo it’s the intractability rather than undecidability that’s the real problem.

                  1. 1

                    It becomes decidable by giving us an upper bound on the number of steps the program can take, so should require us to calculate the LBA equivalent of a very large BB. I’d call that “effectively” undecidable, which seems like it would be “worse” than intractable.

                    1. 2

                      I agree it’s, let’s say, “very” intractable to make the most general use of a memory bound to verify program properties. But the reason it doesn’t seem like a purely pedantic distinction to me is that once you make a restriction like “64-bit pointers”, you do open up a bunch of techniques for finite solving, some of which are actually usable in practice to prove properties that would be undecidable without the finite-pointer restriction. If you just applied Rice’s theorem and called verifying those properties undecidable, it would skip over the whole class of things that can be decided by a modern SMT solver in the 32-bit/64-bit case. Granted, most still can’t be, but that’s why the boundary that interests me more nowadays is the “SMT can solve this” vs. “SMT can’t solve this” one rather than the CS-theory sense of decidable/undecidable.

                4. 6

                  Why can’t I have computer generated proofs? I have some memory, I send it there, then there, then I’m done.

                  It’s really hard. The main tool for that is separation logic. Manually doing it is harder than borrow-checking stuff. There are people developing solvers to automate such analyses. Example. It’s possible what you want will come out of that. I think there will still be restrictions on coding style to ease analyses.

                  1. 3

                    In my experience, automated proof generators are very leaky abstractions. You have to know their search methods in detail, and present your hypotheses in a favorable way for those methods. It can look very clean, but it can mean that seemingly easy changes turn out to be frustrated by the methods’ limitations.

                    1. 4

                      I’m totally with you on this. Rust very much feels like an intermediate step and I don’t know why they didn’t take it to it’s not-necessarily-obvious conclusion.

                      1. 5

                        In my personal opinion, it might be just that we’re happy that we can actually get to this intermediate point (of Rust) reliably enough, but have no idea yet how to get to the further point (conclusion). So they took it where they could, and left the subsequent part as an excercise for the reader… I mean, to be explored by future generations of programmers, hopefully.

                        1. 4

                          We have the technology, sort of. Total program analysis is really expensive though, and the workflow is still “edit some code” -> “compile on a laptop” -> repeat. Maybe if we built a gc’ed language that had a mode where you push your program to a long running job on a compute cluster to figure out all the memory proofs.

                          This would be especially cool if incrementals could be cached.

                          1. 4

                            I’ve recommended that before. There’s millions being invested into SMT/SAT solvers for common bugs that might make that happen, too. Gotta wait for the tooling to catch up. My interim recommendation was a low-false-positive, static-analysis tool like RV-Match to be used on everything in the fast path. Anything that passes is done no GC. Anything that hangs or fails is GC’d. Same with automated proofs to eliminate safety checks. If it passes, remove that check if that’s what pass allows. If it fails, maybe it’s safe or maybe tool is too dumb. Keep the check. Might not even need cluster given number of cores in workstations/servers and efficiency improvements in tools.

                          2. 4

                            I think it’s because there’s essentially no chance that a random piece of code will be provable in such a way. Rust encourages, actually to the point of forcing, the programmer to reason about lifetimes and ownership along with other aspects of the type as they’re constructing the program.

                            I think there may be a long term evolution as tools get better: the languages checks the proofs (which, in my dream, can be both types and more advanced proofs, say that unsafe blocks actually respect safety), and IDE’s provide lots of help in producing them.

                            1. 2

                              there’s essentially no chance that a random piece of code will be provable in such a way

                              There must be some chance; rust is already proving memory safety.

                              Rust forces us to think about lifetimes and ownership, but to @tedu’s point, there doesn’t seem be much stopping it from inferring those lifetimes & ownership based upon usage. The compiler knows everywhere a variable is used, why can’t it determine for us how to borrow it and who owns it?

                              1. 17

                                Rust forces us to think about lifetimes and ownership, but to @tedu’s point, there doesn’t seem be much stopping it from inferring those lifetimes & ownership based upon usage. The compiler knows everywhere a variable is used, why can’t it determine for us how to borrow it and who owns it?

                                This is a misconception. The Rust compiler does not see anything beyond the function boundary. That makes lifetime checking efficient. Basically, when compiling a function, the compiler makes an reasonable assumption about how input and output references are connected (the assumption is “they are connected”, also known as “lifetime elision”). This is an assumption communicated the outside world. If this assumption is wrong, you need to annotate lifetimes.

                                When compiling, the compiler will check if the assumption holds for the function body. So, for every function call, it will check if the the signature holds (lifetimes are part of the function signature).

                                Note that functions with different lifetime annotations taking the same data might differ in their behaviour. It also isn’t always obvious to the compiler whether you want references to be bound together or not and that situation might be ambigous.

                                The benefit of this model is that functions only need to be rechecked/compiled when they actually change, not some other code somewhere else in the program. It’s very predictable and errors are local to the function.

                                1. 2

                                  I’ve been waiting for you @skade.

                                  1. 2

                                    Note that functions with different lifetime annotations taking the same data might differ in their behaviour.

                                    I wrote this late at night and have some errata here: they might differ in their behaviour wrt. lifetime checking. Lifetimes have no impact on the runtime, an annotation might only prove something safe that the compiler previously didn’t see as safe.

                                  2. 4

                                    Maybe I’m misunderstanding. I’m interpreting “take it to its conclusion” as accepting programs that are not annotated with explicit lifetime information but for which such an annotation can be added. (In the context of Rust, I would consider “annotation” to include choosing between &, &mut, and by-move, as well as adding .clone() when needed, especially for refcount types, and of course adding explicit lifetimes in cases that go beyond the present lifetime elision rules, which are actually pretty good). My point is that such a “smarter compiler” would fail a lot of the time, and that failures would be mysterious. There’s a lot of experience around this for analyses where the consequence of failure is performance loss due to not being able to do an optimization, or false positives in static analysis tools.

                                    The main point I’m making here is that, by requiring the programmer to actually provide the types, there’s more work, but the failures are a lot less mysterious. Overall I think that’s a good tradeoff, especially with the present state of analysis tools.

                                    1. 1

                                      I’m interpreting “take it to its conclusion” as accepting programs that are not annotated with explicit lifetime information but for which such an annotation can be added.

                                      I’ll agree with that definition

                                      My point is that such a “smarter compiler” would fail a lot of the time, and that failures would be mysterious.

                                      This is where I feel we disagree. I feel like you’re assuming that if we make lifetimes optional that we would for some reason also lose the type system. That was not my assumption at all. I assumed the programmer would still pick their own types. With that in mind, If this theoretical compiler could prove memory safety using the developer provided types and the inferred ownership, why would it still fail a lot?

                                      where the consequence of failure is performance loss due to not being able to do an optimization

                                      That’s totally understandable. I assume like any compiler, it would eventually get better at this. I also assume lifetimes become an optional piece of the program as well. Assuming this compiler existed it seems reasonable to me that it could accept and prove lifetimes provided by the developer along with inferring and proving on it own.

                                      1. 3

                                        Assuming this compiler existed it seems reasonable to me that it could accept and prove lifetimes provided by the developer along with inferring and proving on it own.

                                        That’s what Rust does. And many improvements to Rust focus on increasing the number of lifetime patterns the compiler can recognize and handle automatically.

                                        You don’t have to annotate everything for the compiler. You write code in patterns the compiler understands, and annotate things it doesn’t. So Rust has gotten easier and easier to write as the compiler gets smarter and smarter. It requires fewer and fewer annotations / unsafe blocks / etc as the compiler authors discover how to prove and compile more things safely.

                                    2. 4

                                      Rust forces us to think about lifetimes and ownership, but to @tedu’s point, there doesn’t seem be much stopping it from inferring those lifetimes & ownership based upon usage. The compiler knows everywhere a variable is used, why can’t it determine for us how to borrow it and who owns it?

                                      I wondered this at first, but inferring the lifetimes (among other issues) has some funky consequences w.r.t. encapsulation. Typically we expect a call to a function to continue to compile as long as the function signature remains unchanged, but if we infer the lifetimes instead of making them an explicit part of the signature, subtle changes to a function’s implementation can lead to new lifetime restrictions being inferred, which will compile fine for you but invisibly break all of your downstream callers.

                                      When the lifetimes are an explicit part of the function signature, the compiler stops you from compiling until you either fix your implementation to conform to your public lifetime contract, or change your declared lifetimes (and, presumably, since you’ve been made conscious of the breakage in this scenario, notify your downstream and bump your semver).

                                      It’s basically the same reason that you don’t want to infer the types of function arguments from how they’re used inside a function – making it easy for you to invisibly breaking your contract with the outside world is bad.

                                      1. 3

                                        I think this is the most important point here. Types are contracts, and contracts can specify far more than just int vs string. Complexity, linearity, parametricity, side-effects, etc. are all a part of the contract and the more of it we can get the compiler to enforce the better.

                                2. 1

                                  Which is fine, until you have time or memory constraints that are not easily met by the tracing GC, which is all software of sufficient scale or complexity. At that point, you end up with half-assed and painful to debug/optimize manual memory management in the form of pools, ect.

                                  1. 1

                                    Or there’s the rust approach, where I write a little proof that I’m done with the memory, and then the computer verifies my proof, or rejects my program. Proof verification is also something computers are good at. Nice.

                                    Oh I wish that were how Rust worked. But it isn’t. A variant of Rust where you could actually prove things about your programme would be wonderful. Unfortunately, in Rust, you instead just have ‘unsafe’, which means ‘trust me’.

                                  2. 4

                                    there were multiple times during my learning process in which I was transported back in time to when I was initially trying to learn how to program

                                    I totally agree. When you start out learning Rust, you feel like a total beginner all over again. It’s a really hard language to learn, even for an experienced software engineer.

                                    I’m about a year and a bit into my Rust excursion, and I’ just about productive now.

                                    1. 2

                                      I keep bouncing off of learning Rust, working through the Rust Book and the Gentle Introduction, and losing the will to continue.

                                      I think my problem is that there’s so much to the language in terms of syntax and semantics, and to read and really understand existing code, you have to know all of it, from lifetimes to macros, because all of the code out there uses all of it. You can’t understand a subset and use that to bootstrap your understanding of the rest of it, it’s all or nothing. This is really, really far from my experience with other languages. Some of it may be my age and decreasing neural plasticity, but surely not all of it (I’m learning Common Lisp right now and not having any comparable problems).

                                      1. 2

                                        I feel the same way.

                                        I had similar experiences with Scala, too.

                                        My observation so far is that with other languages, it was much easier to design my APIs. With Rust, I kept changing my API because I didn’t understand the restrictions of the compiler. The final API was not what I had in my mind at all, with lots of leaky abstractions or compromises.

                                        I didn’t give up but I am not in a good position either. I checked ReasonML recently and felt much more at home.

                                        1. 1

                                          I’ve been working with Rust some, and I don’t really agree with this. It may be hard to really understand some existing code without knowing everything, but you certainly don’t need to know it all to write basic programs. I haven’t really learned macros yet, and still consider them to be basically magic methods. I’m not super-used to working with lifetimes, but you can ignore them for like 90% of code. Most of the rest is very similar to every other type-checked language with generics out there. The only exception is having to think more about ownership and when to move or borrow, but the compiler often helps you figure out what to change when you’ve done something the borrow checker doesn’t like.

                                        2. 1

                                          Rust is cool, and it’s faster but has less correctness guarantees than I need.

                                          1. 1

                                            What do you use instead?

                                            1. 2

                                              I use F# (.net core) personally and I’m not a systems programmer so that’s probably part of my motivations. It looks like some of my preconceptions were wrong as I looked into it more but it also has some edge cases that can still bite you in abstract.

                                              I guess I should also qualify that part of why I don’t use Rust is that getting started seems wowzers complex. I often think “Wow rust looks cool, but using it outside of as a toy looks very complicated.”

                                              1. 1

                                                I’ve never used F#, but I read a lot about it and I always seen it as a very interesting and well designed language.

                                                1. 1

                                                  Yeah it’s spiritually similar to Rust in several ways, both having come out of OCaml. They are like brothers who went down very very different paths. I’ve long considered Rust, maybe I’ll try it out to mess with making a game is there anything you recommend?

                                                  1. 1

                                                    Sorry, I can’t recommend anything. I’ve no significant experience with Rust yet :-)

                                          2. [Comment removed by author]

                                            1. 1
                                              Why Nim in particular?  Why not <name one of a hundred other languages>?
                                              
                                            2. -1

                                              “Contact Sales” button position:absolute’d to the bottom of my screen is very, very irritating. Especially for a long article.

                                              I’m having difficulty engaging with these rust stories.

                                              Since a big part of learning a new thing is rote memorization…

                                              :(

                                              To anyone who up-voted this: what are the parts of interest? Anything you would recommend to outsiders?

                                              1. 4

                                                Long story short, rust is a great language with a bright future. It has great documentation. It also can be difficult to learn and he struggled with the borrow checker like almost every person who writes a blog post similar to this. To learn rust he attempted to follow this book except he wrote it in rust instead of go.

                                                1. 2

                                                  Thankyou for summary steveno, but I’m after “why is this of interest” more than “what he wrote”.

                                                  almost every person who writes a blog post similar to this

                                                  This is more of my concern. I’ve heard of rust, these advantages and these problems before. What’s new in the linked post? Is there anything inside of it of interest to an outsider like me? Anything different?

                                                  I tried to readthrough this article, but had trouble enjoying it. What are other people enjoying in it?

                                                  EDIT: General thanks for the replies. I’ll do this rather than individually.

                                                  1. 12

                                                    Unlike the vast majority of the people writing Rust experience posts, Paul Dix has decades of experience in systems programming and is CTO of a company that makes systems software, so not only do I trust his opinions more than most, he has more influence on adoption than most. So even if he says the same things, that itself is interesting to me.

                                                    Same with Bryan Cantrill: http://dtrace.org/blogs/bmc/2018/09/18/falling-in-love-with-rust/

                                                    1. 3

                                                      With that in mind, his write-up is a lot more humble about learning a new language than some people I read with as much experience as he has. He even opened a pull request soliciting ideas for improving the work.

                                                      1. 1

                                                        For the record, my remarks were in no way meant to convey anything negative toward or about the author.

                                                      2. 2

                                                        Anything different?

                                                        In my opinion, no.