1. 1

    Nice, yet another reason not to use Rust!

    1. 17

      Be careful, they also use C (e.g. in zstd). Better not use C either!

      1. 5

        It is one thing to dislike Facebook having influence on the Rust Foundation. However, it is another thing to not use Rust because of this event. Would you care to unpack your reasoning? Does it have to do with moral principles? Predictions about where this leads?

        Also, for the language(s) you prefer, to what degree are they “free” from the same concerns you have about Rust and/or Facebook’s involvement in Rust?

        I admit that I’m prodding a bit here, because when people say “reasons” it is only fair to dig in and get, well, the reasoning as opposed to a one-liner.

        1. 2

          I don’t write Rust, but most it seems like most developers have had an overwhelmingly positive reaction to the emergence of Rust. I’m curious, what (other than Facebook’s involvement) makes you hesitant to get on board? What are some alternatives that you would consider instead?

          1. 6

            I’ve been told many, many times, “Why are you using Rust? You should use Rust!”, and it feels very much like the push for everything to be Java and OOP years ago. I actually like writing Rust and I’ve made a few things with it. I might have burned out of learning updates to it since I started writing it around 1.0 until around async/await getting stabilized.

            Ada 2012 is a viable mature alternative, and is very close in feature set and many conceptual constructs to a Pascal version of a safer C++, with extra features for type safety and error detection. Going from C++ -> Ada is actually a two week process or so because there’s many similarities, despite the languages being in different families.

            1. 11

              With all due respect, I was around for the “everything Java” push (maybe you were too!) and the movement around Rust is much more “grassroots”. Java had the backing of a big “hot” corporation (yes kids, Sun was hot once!) and there were endless streams of books and tutorials and people cold calling companies and seminars and stuff. Not to mention tons of back-end development of standard libraries, etc.

              Rust to me still feels like an enthusiast movement, but coupled with an actual, delivered product.

              1. 2

                My tone may not have come across well, I’m not trying to disparage Rust or be combative, I’m just giving my opinion. Rust usage would likely affect me at work, so I’ve been trying to predict it’s adoption by reading about Theory of Reasoned Action, the Technology Acceptance Model and similar concepts. At the time people were just trying to solve development problems, just like they’re trying to do now. I’m curious if Github and more widespread internet and computing resources existed back then, if there would have been more parallels, or if Smalltalk would have had more sticking power.

              2. 2

                I’ve been told many, many times, “Why are you using Rust? You should use Rust!”, and it feels very much like the push for everything to be Java and OOP years ago.

                I take your point. There are (at least) two underlying aspects:

                1. Distinguishing initial enthusiasm from longer-term suitability.

                2. Distinguishing ‘disinterested’ (i.e. unbiased) recommendations from marketing-driven hype.

                Another factor to consider: Around Java’s first public release in 1996, the main popular alternatives were C and C++. (Fair? I’m not a historical expert, so please add to this – i.e. let me know if others were considered both popular and situated similarly.) In contrast, compare 1996 to 2015, when Rust 1.0 was released. The diversity and language competition is much deeper now. My point is to say that Rust’s popularity is even more impressive given the choices available; e.g. C, C++, Java, Python, Go, Scala, C#, F#, Haskell …

                1. 3

                  I think Delphi was a popular alternative back then while Smalltalk was close to where Rust is now in industrial mindshare.

                  1. 1

                    A lot of this was told to me by a Smalltalk developer at the time. Smalltalk was somewhat already established. It wasn’t just Sun, but it was competing against IBM, a giant at the time, that made the independent Smalltalk tool developers feel like they had to merge together and resulted in many internal issues. With the smaller folks struggling, Smalltalk effectively died when IBM pivoted to Java. This is a bit oversimplified, there were other technical concerns involved.

                    I think Facebook joining up, along with other big names is the equivalent of Sun and IBM with Java. In this way, I feel Rust vs Ada seems to parallel Java vs Smalltalk in some ways and I think Ada (and possibly C++) is in big trouble, if it wasn’t already. However, AdaCore is in full swing promotion and marketing mode right now, so things might get interesting over the next year.

              3. 2

                Be careful. We the Lobste.rs are crustaceans.

              1. 8

                This is interesting and I am prolly going to use it in our services. Could you talk more about the underlying protocol?

                Also, aren’t these sentences contradicting:

                So we rewrote gRPC and migrated our live network. DRPC is a drop-in replacement that handles everything we needed from gRPC

                and

                It’s worth pointing out that DRPC is not the same protocol as gRPC, and DRPC clients cannot speak to gRPC servers and vice versa.

                How it is a drop in replacement if both client and server needs to be changed

                1. 15

                  This is interesting and I am prolly going to use it in our services. Could you talk more about the underlying protocol?

                  The wire format used is defined here.

                  Logically, a sequence of Packets are sent back and forth over the wire. Each Packet has a enumerated kind, a message id (to order messages within a stream), a stream id (to identify which stream), and a payload. To bound the payload size, Packets are split into Frames which are marshaled and sent.

                  A marshaled Frames has a single header byte, the varint encoded stream and message ids, a varint encoded length, and that many bytes of payload. The header byte contains the kind, if it is the last frame for a Packet, and a control bit reserved for future use (the implementation currently ignores any frame with that bit set).

                  Because there’s no multiplexing at this layer, the reader can assume the Frames come in contiguously with non-decreasing ids, limiting the amount of memory and buffer space required to a single Packet. The Frame writing code is as simple as appending some varints, and the reading code is about 20 lines, neither of which have any code paths that can panic.

                  How it is a drop in replacement if both client and server needs to be changed

                  There’s a drpcmigrate package that has some helpers to let you serve both DRPC and gRPC clients on the same port by having the DRPC clients send a header that does not collide with anything. You first migrate the servers to do both, and can then migrate the clients.

                  The drop in replacement part refers to the generated code being source code API compatible in the sense that you can register any gRPC server implementation with the DRPC libraries with no changes required. The semantics of the streams and stuff are designed to match.

                  Sorry if this was unclear. There’s multiple dimensions of compatibility and it’s hard to clearly talk about them.

                  1. 8

                    (not the one who asked). Thank you for the comment. Do you plan to document the protocol somewhere (other than code)? It seems to me a RPC protocol needs a healthy ecosystem of implementations in many languages to be viable long term :-)

                    (edit: I mean document it cleanly, with request/reply behavior, and talk about the various transports that are supported.)

                    1. 6

                      You are absolutely right that having good documentation is essential, and I’ve created a github issue to start to keep track of the most important bits I can think of off the top of my head. To be honest, I’ve always struggled a bit with documentation, but I’m trying to work on it. In fact, the current CI system will fail if any exported symbols do not have a doc string. :) Thanks for bringing this up.

                    2. 2

                      Thanks for the explanation! Are there any plans for writing Python client/server?

                      1. 4

                        I do hope to get more languages supported. I created an issue to add Python support. I don’t currently deal with any Python code, so help will probably be needed to make sure it “fits” correctly with existing codebases.

                        1. 1

                          I have started looking into the drpcwire code, I will wait for the documentation. Meanwhile, is there any place, like IRC, Discord where drpc/storj developers hang out? The Python issue is tagged help-wanted, so, can I be of any help?

                  1. 8

                    Oh, and fn belongs to the left of control. Apple and Lenovo get this right, why can’t anyone else?

                    I know some people have strong opinions the other way; ThinkPads allow configuring this in the BIOS – a little quality of life detail that matters a lot to some people.

                    I never use the TrackPoint, but I like that it’s there as it means I have discrete buttons (I don’t care that they’re on the top). I really dislike the integrated buttons that almost all other laptop ship with. I know a lot of people like the trackpad on macs, but personally I hate it. “Right click” with two fingers fails often enough (or is triggered accidentally!) to be highly annoying, and other gestures are even worse. And the cursor often moves while clicking.

                    I mostly just use ThinkPads because it’s easy; I know they will work on Linux most of the time, the design doesn’t change that fast or from iteration to iteration. I know what to expect, which is boring and the way I like it. Researching other laptops is a lot of work and I have more important and/or fun stuff to do.

                    When my x270 broke last year (slipped with laptop in backpack, fell on my back) I ended up getting a E585, just because someone had it on sale nearby for a good price. It’s not my most favourite model (battery life and size of the x270 was much better), but it works well enough.

                    When I had a Dell XPS 15 for work I started having annoying screen flickering problems; not the only one with those problems on that specific model it turned out, which seemed to be some sort of BIOS issue(?) Of course, Dell will spend no effort on fixing this, no matter if it’s a BIOS bug or not. I ended up just returning the laptop to work and buying the x270 myself.

                    The job before that I had the XPS 13 “developer edition” which came pre-installed with Ubuntu, and had some issues with that too. Curiously, I had fewer issues after I reinstalled the machine to Arch Linux; it actually worked pretty well after that 🤷 I think the pre-installed Dell drivers on the Ubuntu LTS didn’t quite work correctly or something, I tried removing those to just use the mainline Linux ones, but the kernel was too old or whatnot and it left me without WiFi (and no Ethernet port…) It was ridiculously time-consuming to get that fixed.

                    tl;dr: ThinkPads are the most boring predictable laptops I know; which I consider a good thing.

                    I agree with the sometimes ridiculous amount of ThinkPad wankery on /r/ThinkPad and the like btw. Peter Bright at Ars Technica was also a big ThinkPad fanboy and every move Lenovo made on ThinkPads made was extensively reported (whereas little reporting was done on other laptops, unless it was proper big news like the M1) until he left.

                    1. 2

                      Thank you, that’s better than the annoyed response I was going to write. Thinkpads are just decent predictable linux laptops that work well. With an external battery, my x270 has excellent battery life, and 16GB of RAM, I’m happier with it than with something that would force me to use mac OS.

                      1. 1

                        The job before that I had the XPS 13 “developer edition” which came pre-installed with Ubuntu, and had some issues with that too.

                        Running Linux on the one I had (a 9360 from 2017, so it’s been a bit) was ultimately just kind of a bad experience. Weirdly terrible performance, display glitches, network weirdness. Which feels like a risk I take every time I burn money on a laptop that’s not a ThinkPad. It might be ok, but it’s a lot of money to spend not to be sure that it’s going to be ok.

                        ThinkPads have been, in truth, kind of a mixed bag for most of the time Lenovo’s owned the brand, and they’ve made some bad design decisions along the way - the keyboard is ok now, it used to be a lot better, for example. But they remain a known quantity for my purposes in a way that I’m not sure anything else really does. This is in no small way because laptops generally are a really sad and infuriating class of product, where the priorities and interests of the manufacturers pretty much only align with mine by accident.

                        1. 1

                          I had that too with a work laptop. Then I replaced it with Manjaro and everything worked as expected.

                          Seems like it’s Ubuntu having those issues on the XPS (15).

                          1. 1

                            Take Peter Bright’s reporting with a grain of salt. I also enjoyed his journalistic interests… until one day I saw that ArsTechnica had yanked all of his articles off their site. You should just search duckduckgo for his name. I’m not sure that he has made the best choices in life.

                            1. 2

                              They’re not yanked. The articles are still there, but his author page is gone and the primary author is now listed as “ars staff”. It’s not hard to find them, though; they’re still up.

                              I’m very glad he’s not free to do what he was convicted of doing any longer. Not sure I’d call it relevant to a discussion of whether or not Thinkpads are overrated.

                          1. 5

                            It is me or Rust’s async is much harder than Erlang’s?

                            1. 18

                              Rust’s async has to deal with some very hard constraints. I linked this in another thread today, but here’s Graydon Hoare, the original creator of Rust, talking about some of the history. (Edit: replaced link to the thread with a link to a collection, as Twitter’s threading breaks the thread in the middle, making it easy to miss the second half)

                              1. 1

                                Great details. So ultimately C compat won. Good to know.

                              2. 7

                                That’s hardly a surprise, erlang is a much higher-level (and slower) language.

                                1. 3

                                  Erlang is better overall for low-latency tasks. It is worse for high throughput tasks. Async Rust is also worse than non-Async Rust for high throughput tasks. “Slower” does not describe actually measurable characteristics.

                                  1. 1

                                    I think he probably though about numerical calculation performance which is irrelevant in the topic of async communication.

                                    1. 1

                                      I was thinking about general CPU bound tasks, yes (not just numerics). Rust isn’t just targetting distributed services :-)

                              1. 4

                                It’s worth keeping in mind that this worldview only includes memory safety in the definition of “safe”. Plan interference, deadlocks, SQL injection, or other high-level “interleaving” safety problems are not considered. The reason I bring this up is because memory safety is broadly a solved problem for any language implemented with a GC, and so the original article implicitly limits Zig’s safety to a specific niche where GCs are not available.

                                1. 4

                                  Sorry, but wtf is “plan interference”? The paper doesn’t even bother defining it, even though it’s not, afaik, a common term.

                                  SQL injections and deadlocks are, of course, a risk in every language, to the best of my knowledge.

                                  1. 7

                                    We have to define “plan” first. Originally, capability theorists were informal, and a plan was simply what a programmer intended for a chunk of code to do. We can be far more formal without losing the point: For a chunk of code, its plan is the collection of possible behaviors and effects that it can have in any context.

                                    We often want to explicitly interleave plans. For example, suppose that we want to compute the sum of a list in Python 3:

                                    s = sum(l)
                                    

                                    And also we want to compute the arithmetic mean:

                                    a = sum(l) / len(l)
                                    

                                    Then we could deliberately interfere the two programs with each other to create a composite program which computes both the sum and the arithmetic mean, sharing work:

                                    s = sum(l)
                                    a = s / len(l)
                                    

                                    Plan interference is a nebulous but real class of bugs that arise from the fact that, when we interleave programs together from component programs, we also interleave their behaviors, creating complex plans with non-trivial feedback and emergent new behaviors. If the linked paper seems to have trouble explaining itself, it’s because, as I understand it, this paper was the first attempt to explain all of this with sufficiently-convincing examples.

                                    To summon the examples from the paper from E to Python 3, it is sufficient to imagine that sum() is locally overridden by a coroutine. Then, evaluation of sum() might suspend execution of the stack frame for an indefinite period of time. In my example, this is harmless, but the paper explains how easy it is for this to become a problem.

                                    What we think is fundamental is a matter of perspective. I currently think that SQL injection is an API problem, for example, rather than a fundamental limitation of string-handling. In contrast, I think that plan interference and deadlocks are both fundamentally impossible to prevent at compile time. I could be wrong about all of this.

                                1. 19

                                  I think under-appreciated aspect is that Rust not only prevents safety issues from being exploitable, but in many cases prevents them from happening in the first place.

                                  Contrast this with C where safety efforts are all focused on crashing as fast as possible. Things are nullable, but you get segfaults. Buffers are unsafe, but you have crashes on guard pages and canaries. Memory management is ad-hoc, but the allocator may detect an invalid free and abort.

                                  Rust in some places ensures safety by panicking too, but it also has plenty of tools that guarantee safety by construction, like move semantics, borrowing, iterators, match on options and results. So the bar is higher than merely “not exploitable because it crashes”. It’s not exploitable, because it works correctly.

                                  1. 10

                                    Interestingly, “crash early, crash often” is actually AFAIU an approach that can also lead to really robust software when properly embraced, as in Erlang. Personally I’m not convinced C is a particularly exemplary follower of this philosophy, at least as seen in the wild. With that said, I sometimes wonder if this isn’t something of a blind spot for Rust - i.e. stuff like cosmic rays (which I read start becoming noticeable at some scales), or processor bugs and attacks based on them. Maybe some of those risks can be mitigated with stuff like ECC memory? I’m certainly not an expert in this area FWIW, far from it. Just when thinking, I sometimes wonder if the Erlang philosophy is not the winner here in what it can achieve in the biggest horizon of robustness/resiliency (?)

                                    1. 7

                                      Rust has the “crash early” philosophy too (asserts, indexing panic, overflows can panic), but it just doesn’t need it as often at run time. You wouldn’t want to crash just for the sake of crashing :)

                                      Rust has all of C’s protections too. They’re added by LLVM, OS, and hardware.

                                      1. 20

                                        Erlang’s “Let It Crash” philosophy is more than just ‘die a lot’ – the other part is that, recognizing that software can fail for a wide variety of reasons but that those reasons are frequently sporadic edge cases, you can get huge operational wins by having an intentional and nuanced system of recovery in-platform.

                                        In practice what this means is that in Erlang/OTP, you frequently have tens, thousands, or millions of concurrent processes, as you might in an OS. Many of these processes are executing business logic, etc. But some of them are ‘supervisor’ processes, which detects when one of the processes it is monitoring has died, and then attempts to restart it (perhaps with a maximum number of attempts in a given time period). This is recursive; for complex applications you might have supervisor trees that are several layers deep.

                                        The benefit here is that you start by writing the golden path. And then, sometimes, you just stop. Get illegal JSON input? Explode. Get an HTTP request you didn’t expect? Explode. Frequently, pragmatically, you don’t need to write the code that handles all of the garbage cases if your supervision tree is solid enough and your lightweight processes start ultra fast.

                                        This philosophy has downsides – if the processes are carrying a large amount of important internal state, then sometimes them dying can be inconvenient because resurrection might involve an expensive rebuild step. So you need to pay more than the usual amount of attention to the stateful/stateless boundaries.

                                        Rust at one point had this as a core idea, but abandoned it for, in my opinion, poor reasons. And now lands up grappling with janky concurrency coloring problems, as it unfortunately appears Zig will too.

                                        1. 9

                                          Rust at one point had this as a core idea, but abandoned it for, in my opinion, poor reasons.

                                          The OTP monitoring system seems really really cool. However rust abandoned green threads for a very good reason: performance. When the goal is to be able to maximize performance, and compete with C++, you can’t exactly ask for heavy runtime with reduction counters and all the bells and whistles of BEAM, useful as they are.

                                          The “coloring problem” caused by async stems from the same root causes: you can’t really have resizable stacks and lightweight threads in a language that is supposed to be able to run without even a heap allocator (“no-std” in rust parlance). That’s better left to higher-level languages like java or Go (or python if they had made less bad choices).

                                          1. 5

                                            Here’s a more detailed explanation by Graydon Hoare, the original creator of Rust.

                                            In short: Rust’s removal of green threads was for two reasons: 1) performance (as you mentioned), 2) difficult interoperation with C. Given Rust’s design constraints, including that you shouldn’t pay for what you don’t use, and that interoperation with C is expected to be easy, this approach didn’t work for Rust.

                                            Edit: Replaced link to thread with a link to a collection, as Twitter’s default threading makes it easy to miss the second half.

                                      2. 5

                                        Crash-early is fine, as long as the process has a supervisor process that promises to take care of restarting it. That’s the part that seems missing in a lot of systems (in C or otherwise.) Often it just seems kind of ad-hoc. Having implemented some IPC in C++ in the past using POSIX APIs, I remember it being nontrivial for the first process to handle the child’s death (but I may be misremembering.) Its certainly not something done for you, the way it is in Erlang.

                                      3. 4

                                        Things are nullable, but you get segfaults.

                                        If you are lucky. Note that this isn’t guaranteed and doesn’t always happen.

                                        1. 1

                                          Yes, the worst part is when something overwrites some other (valid) memory, causing an error when that memory is next accessed (or worse no error at all). Pretty much your only recourse at that point is to whip out hardware watchpoints (which IME tends to be buggy and tank performance).

                                      1. 25

                                        I think threads are better than a lot of people think, but in this case the measurement strikes me as a bit naive. Go very likely consumes more memory than strictly needed because of the GC overhead. The actual memory occupied by goroutines could be less than half the memory used in total, but here we only see goroutine overhead + GC overhead without a way of separating them.

                                        1. 8

                                          What overhead specifically? Stack maps for GC?

                                          The benchmark doesn’t seem to have many heap objects, and I thought Go used a conservative/imprecise GC anyway so objects don’t have GC space overhead (mark bits, etc.). Although I think the GC changed many times and I haven’t followed all the changes.

                                          1. 7

                                            The GC has been fully precise since Go 1.4.

                                            1. 6

                                              OK that’s what I suspected, but as far as I can tell it’s a moot point because the benchmark doesn’t have enough GC’d objects for it to matter. Happy to be corrected.

                                            2. 5

                                              I think when people speak of GC overhead they’re not talking about the per-object overhead of tracking data. Rather, the total amount of memory space one needs to set aside to cover both memory actually in use, and memory no longer in use but not yet collected: garbage. This can often be quite a lot larger than the working set, especially if there is a lot of churn.

                                              1. 3

                                                Where does that exist in the benchmark?

                                                I see that each goroutine calculates a hash and calls time.Sleep(). I don’t see any garbage (or at least not enough to know what the grandparent comment is talking about)

                                                1. 1

                                                  The space can be reserved for future collections anyway. It’s well known that GCs require more space than strictly needed for alive objects.

                                          1. 4

                                            What’s the advantage of using ReScript, when you can use something like F# (an underestimated language) in both backend and frontend, not to mention with WASM support and decent server remoting? cf. https://fsbolero.io/

                                            1. 8

                                              Can’t say about ReScript, but here goes for OCaml: F# on linux is still very new (using dotnet core) and I’m not sure what the open source ecosystem (not the windows one) looks like. OCaml can also be used on frontend and backend and is quite robust, if sometimes quirky. I’m not sure if OCaml is more or less underestimated than F# :-)

                                              1. 3

                                                Do you have some links I can checkout to understand the current state of full-stack web development in OCaml?

                                                F# on linux is still very new (using dotnet core) and I’m not sure what the open source ecosystem (not the windows one) looks like

                                                I’m just starting to look at F#, and it works decently on VSCode with Ionide plugin. Also, the F# team has announced that they are going to improve the OSS story further. From the F# 5.0 announcement post,

                                                We also plan on making significant F# tooling improvements over time. We’ve already started this work. One of the first steps was to incorporate FSharp.Compiler.Service into our build and packaging infrastructure so that any consumers of this package (e.g., the Ionide plugin in VSCode) can simply add a NuGet feed and get nightly updates. Next, we’ll work towards retiring the FSharp.Compiler.Private project, which is functionally equivalent to FSharp.Compiler.Service, so that all F# tooling consumes the same functionality in the same way. From there, we intend on working with the F# community to eventually harden the F# LSP implementation so that it powers all F# editor tooling (including Visual Studio). The long-term goal is that all F# tools have consistent behavior and feature availability, with individual editors adding their own “flavor” and unique feature set on top of that behavior so that F# programmers can pick the tool they like the most.

                                              2. 5

                                                Compile speed (milliseconds incremental), fast and efficient editor plugins, quality of JS output (seriously try out some simple examples and compare), onboarding JS devs onto a bit more familiar syntax (parentheses & curly braces), and close relationship with underlying JS/npm ecosystem, e.g. high-quality bindings to React.js, Next.js, Tailwind, and many other libraries/frameworks.

                                                If your primary focus is on staying in the F# ecosystem, then Fable is a decent choice. For every other use case, ReScript is the obvious choice. Btw, last time I checked, Bolero or Blazor and everything outside C/C++/Rust produces super bloated WASM output and they will continue to until the runtime ships with a garbage collector.

                                              1. 45

                                                FWIW, this is how you express conditional arguments / struct fields in Rust. The condition has to encompass the name as well as the type, not just the type as was first attempted.

                                                I feel like Rust has definitely obliterated its complexity budget in unfortunate ways. Every day somebody comes to the sled discord chat with confusion over some async interaction. The fixation on async-await, despite it slowing down almost every real-world workload it is applied to, and despite it adding additional bug classes and compiler errors that simply don’t exist unless you start using it, has been particularly detrimental to the ecosystem. Sure, the async ecosystem is a “thriving subcommunity” but it’s thriving in the Kuhnian sense where a field must be sufficiently problematic to warrant collaboration. There’s no if-statement community anymore because they tend to work and be reasonably well understood. With async-await, I observed that the problematic space of the overall community shifted a bit from addressing external issues through memory safety bug class mitigation to generally coping with internal issues encountered due to some future not executing as assumed.

                                                The problematic space of a community is a nice lens to think about in general. It is always in-flux with the shifting userbase and their goals. What do people talk about? What are people using it for? As the problematic space shifts, at best it can introduce the community to new ideas, but there’s also always an aspect of it that causes mourning over what it once represented. Most of my friends who I’ve met through Rust have taken steps to cut interactions with “the Rust community” down to an absolute minimum due to it tending to produce a feeling of alienation over time. I think this is pretty normal.

                                                I’m going to keep using Rust to build my database in and other things that need to go very fast, but I see communities like Zig’s as being in some ways more aligned with the problematic spaces I enjoy geeking out with in conversations. I’m also thinking about getting a lot more involved in Erlang since I realized I haven’t felt that kind of problem space overlap in any language community since I stopped using it.

                                                1. 31

                                                  I was surprised to see the Rust community jump on the async-await bandwagon, because it was clear from the beginning it’s a bandwagon. When building a stable platform (e.g. a language) you wait for the current fashion to crest and fall, so you can hear the other side of the story – the people who used it in anger, and discovered what the strengths and weaknesses really are. Rust unwisely didn’t do that.

                                                  I will note though that the weaknesses of the async-await model were apparent right from the beginning, and yet here we are. A lesson for future languages.

                                                  1. 28

                                                    This hits me particularly hard because I had experienced a lot of nearly-identical pain around async when using various flavors of Scala futures for a few years before picking up Rust in 2014. I went to the very first Rust conference, Rust Camp in 2015 at Berkeley, and described a lot of the pain points that had caused significant issues in the Scala community to several of the people directly working on the core async functionality in Rust. Over the years I’ve had lots of personal conversations with many of the people involved, hoping that sharing my experiences would somehow encourage others to avoid well-known painful paths. This overall experience has caused me to learn a lot about human psychology - especially our inability to avoid problems when there are positive social feedback loops that lead to those problems. It makes me really pessimistic about climate apocalypse and rising authoritarianism leading us to war and genocides, and the importance of taking months and years away from work to enjoy life for as long as it is possible to do so.

                                                    The content of ideas does not matter very much compared to the incredibly powerful drive to exist in a tribe. Later on when I read Kuhn’s Structure of Scientific Revolutions, Feyerabend’s Against Method, and Ian Hacking’s Representing and Intervening, which are ostensibly about the social aspects of science, I was blown away by how strongly their explanations of how science often moves in strange directions that may not actually cause “progress” mapped directly to the experiences I’ve had while watching Rust grow and fail to avoid obvious traps due to the naysayers being drowned out by eager participants in the social process of Making Rust.

                                                    1. 7

                                                      Reminds me of the theory that Haskell and Scala appeal because they’re a way for the programmer to needsnipe themselves

                                                      1. 5

                                                        Thanks for fighting the good fight. Just say “no” to complexity.

                                                        Which of those three books you mentioned do you think is most worthwhile?

                                                        1. 10

                                                          I think that Kuhn’s Structure of Scientific Revolutions has the broadest appeal and I think that nearly anyone who has any interaction with open source software will find a tremendous number of connections to their own work. Science’s progressions are described in a way that applies equally to social-technical communities of all kinds. Kuhn is also the most heavily cited thinker in later books on the subject, so by reading his book, you gain deeper access to much of the content of the others, as it is often assumed that you have some familiarity with Kuhn.

                                                          You can more or less replace any mention of “paper citation” with “software dependency” without much loss in generality while reading Kuhn. Hacking and Feyerabend are more challenging, but I would recommend them both highly. Feyerabend is a bit more radical and critical, and Hacking zooms out a bit more and talks about a variety of viewpoints, including many perspectives on Kuhn and Feyerabend. Hacking’s writing style is really worth experiencing, even by just skimming something random by him, by anyone who writes about deep subjects. I find his writing to be enviably clear, although sometimes he leans a bit into sarcasm in a way that I’ve been put off by.

                                                        2. 4

                                                          If you don’t mind, what’s an example of async/await pain that’s common among languages and not to do with how Rust uniquely works? I ask because I’ve had a good time with async/await, but in plainer, application-level languages.

                                                          (Ed: thanks for the thoughtful replies)

                                                          1. 12

                                                            The classic “what color is your function” blog post describes what is, I think, such a pain? You have to choose in your API whether a function can block or not, and it doesn’t compose well.

                                                            1. 3

                                                              I read that one, and I took their point. All this tends to make me wonder if Swift (roughly, Rust minus borrow checker plus Apple backing) is doing the right thing by working on async/await now.

                                                              But so far I don’t mind function coloring as I use it daily in TypeScript. In my experience, functions that need to be async tend to be the most major steps of work. The incoming network request is async, the API call it makes is async, and then all subsequent parsing and page rendering aren’t async, but can be if I like.

                                                              Maybe, like another commenter said, whether async/await is a net positive has more to do with adapting the language to a domain that isn’t otherwise its strong suit.

                                                              1. 16

                                                                You might be interested in knowing that Zig has async/await but there is no function coloring problem.

                                                                https://kristoff.it/blog/zig-colorblind-async-await/

                                                                1. 3

                                                                  Indeed this is an interesting difference at least in presentation. Usually, async/await provides sugar for an existing concurrency type like Promise or Task. It doesn’t provide the concurrency in the first place. Function colors are then a tradeoff for hiding the type, letting you think about the task and read it just like plain synchronous code. You retain the option to call without await, such that colors are not totally restrictive, and sometimes you want to use the type by hand; think Promise.all([…]).

                                                                  Zig seems like it might provide all these same benefits by another method, but it’s hard to tell without trying it. I also can’t tell yet if the async frame type is sugared in by the call, or by the function definition. It seems like it’s a sort of generic, where the nature of the call will specialize it all the way down. If so, neat!

                                                                  1. 7

                                                                    It seems like it’s a sort of generic, where the nature of the call will specialize it all the way down. If so, neat!

                                                                    That’s precisely it!

                                                                    1. 2

                                                                      I’ve been poking at Zig a bit since this thread; thank you for stirring my interest. :)

                                                            2. 6

                                                              Well, I think that async/await was a great thing for javascript, and generally it seems to work well in languages that have poor threading support. But Rust has great threading support, and Rust’s future-based strategy aimed from the beginning at copying Scala’s approach. A few loud research-oriented voices in the Rust community said “we think Scala’s approach looks great” and it drowned out the chorus of non-academic users of Scala who had spent years of dealing with frustrating compilation issues and issues where different future implementations were incompatible with each other and overall lots of tribalism that ended up repeating in a similar way in the Rust async/await timeline.

                                                              1. 5

                                                                I am somewhat surprised that you say Rust’s futures are modeled after Scala’s. I assume the ones that ended up in the standard library. As for commonalities: They also offer combinators on top of a common futures trait and you need explicit support in libraries - that’s pretty much all that is similar to Rust’s.

                                                                In Scala, futures were annoying because exceptions and meaningless stacktraces. In Rust, you get the right stacktraces and error propagation.

                                                                In Rust, Futures sucked for me due to error conversions and borrowing being basically unsupported until async await. Now they are still annoying because of ecosystem split (sync vs various partially compatible async).

                                                                The mentioned problem of competing libraries is basically unpreventable in fields without wide consensus and would have happened with ANY future alternative. If you get humans to agree on sensible solutions and not fight about irrelevant details, you are a wizard.

                                                                Where I agree is that it was super risky to spend language complexity budget on async/await, even though solving the underlying generator/state machine problem felt like a good priority. While async await feels a bit to special-cased and hacky to be part of the language… It could be worse. If we find a better solution for async in Rust, we wouldn’t have to teach the current way anymore.

                                                                Other solutions would just have different pros and cons. E.g. go’s or zig’s approach seemed the solution even deeper into the language with the pro of setting a somewhat universal standard for the language.

                                                                1. 3

                                                                  It was emulating Finagle from the beginning: https://medium.com/@carllerche/announcing-tokio-df6bb4ddb34 but then the decision to push so much additional complexity into the language itself so that people could have an easier time writing strictly worse systems was just baffling.

                                                                  Having worked in Finagle for a few years before that, I tried to encourage some of the folks to aim for something lighter weight since the subset of Finagle users who felt happy about its high complexity seemed to be the ones who went to work at Twitter where the complexity was justified, but it seemed like most of the community was pretty relieved to switch to Akka which didn’t cause so much type noise once it was available.

                                                                  I don’t expect humans not to fragment now, but over time I’ve learned that it’s a much more irrational process than I had maybe believed in 2014. Mostly I’ve been disappointed about being unable to communicate with what was a tiny community about something that I felt like I had a lot of experience with and could help other people avoid pain around, but nevertheless watch it bloom into a huge crappy thing that now comes back into my life every day even when I try to ignore it by just using a different feature set in my own stuff.

                                                              2. 3

                                                                I hope you will get a reply by someone with more Rust experience than me, but I imagine that the primary problem is that even if you don’t have to manually free memory in Rust, you still have to think about where the memory comes from, which tends to make lifetime management more complicated, requiring to occasionally forcefully move things unto the heap (Box) and also use identity semantics (Pin), and so all of this contributes to having to deal with a lot of additional complexity to bake into the application the extra dynamicism that async/await enables, while still maintaining the safety assurances of the borrow checker.

                                                                Normally, in higher level languages you don’t ever get to decide where the memory comes from, so this is a design dimension that you never get to explore.

                                                              3. 2

                                                                I’m curious if you stuck around in Scala or pay attention to what’s going on now because I think it has one of the best stories when it comes to managing concurrency. Zio, Cats Effect, Monix, fs2 and Akka all have different goals and trade offs but the old problem of Future is easily avoided

                                                              4. 6

                                                                I was surprised to see the Rust community jump on the async-await bandwagon, because it was clear from the beginning it’s a bandwagon.

                                                                I’m not surprised. I don’t know how async/await works exactly, but it definitely has a clear use case. I once implemented a 3-way handshake in C. There was some crypto underneath, but the idea was, from the server’s point of view was to receive a first message, respond, then wait for the reply. Once the reply comes and is validated the handshake is complete. (The crypto details were handled by a library.)

                                                                Even that simple handshake was a pain in the butt to handle in C. Every time the server gets a new message, it needs to either spawn a new state machine, or dispatch it to an existing one. Then the state machine can do something, suspend, and wait for a new message. Note that it can go on after the handshake, as part of normal network communication.

                                                                That state machine business is cumbersome and error prone, I don’t want to deal with it. The programming model I want is blocking I/O with threads. The efficiency model I want is async I/O. So having a language construct that easily lets me suspend & resume execution at will is very enticing, and I would jump to anything that gives me that —at least until I know better, which I currently don’t.

                                                                I’d even go further: given the performance of our machines (high latencies and high throughputs), I believe non-blocking I/O at every level is the only reasonable way forward. Not just for networking, but for disk I/O, filling graphics card buffers, everything. Language support for this is becoming as critical as generics themselves. We laughed “lol no generics” at Go, but now I do believe it is time to start laughing “lol no async I/O” as well. The problem now is to figure out how to do it. Current solutions don’t seem to be perfect (though there may be one I’m not aware of).

                                                                1. 2

                                                                  The whole thing with async I/O is that process creation is too slow, and then thread creation was too slow, and some might even consider coroutine creation too slow [1]. It appears that concerns that formerly were of the kernel (managing I/O among tasks; scheduling tasks) are now being pushed out to userland. Is this the direction we really want to go?

                                                                  [1] I use coroutines in Lua to manage async I/O and I think it’s fine. It makes the code look like non-blocking, but it’s not.

                                                                  1. 2

                                                                    I don’t think it’s unreasonable to think that the kernel should have as few concerns as possible. It’s a singleton, it doesn’t run with the benefit of memory protection, and its internal APIs aren’t as stable as the ones it provides to userland.

                                                                    … and, yes, I think a lot of async/await work is LARPing. But that’s because a lot of benchmark-oriented development is LARPing, and probably isn’t special to async/await specifically.

                                                                    1. 1

                                                                      I’m not sure what you’re getting at. I want async I/O to avoid process creation and thread creation and context switches, and even scheduling to some extent. What I want is one thread per core, and short tasks being sent to them. No process creation, no thread creation, no context switching. Just jump the instruction pointer to the relevant task, and return to the caller when it’s done.

                                                                      And when the task needs to, say, read from the disk, then it should do so asynchronously: suspend execution, return to the caller, wait for the response to come back, and when it does resume execution. It can be done explicitly with message passing, but that’s excruciating. A programming model where I can kinda pretend the call is blocking (but in fact we’re yielding to the caller) is much nicer, and I believe very fast.

                                                                  2. 5

                                                                    Agreed. I always told people that async/await will be just as popular as Java’s synchronized a few years down the road. Some were surprised, some were offended, but sometimes reality is uncomfortable.

                                                                  3. 29

                                                                    Thank you for sharing, Zig has been much more conservative than Rust in terms of complexity but we too have splurged a good chunk of the budget on async/await. Based on my experience producing introductory materials for Zig, async/await is by far the hardest thing to explain and probably is going to be my biggest challenge to tackle for 2021. (that said, it’s continuations, these things are confusing by nature)

                                                                    On the upside

                                                                    despite it slowing down almost every real-world workload it is applied to

                                                                    This is hopefully not going to be a problem in our case. Part of the complexity of async/await in Zig is that a single library implementation can be used in both blocking and evented mode, so in the end it should never be the case that you can only find an async version of a client library, assuming authors are willing to do the work, but even if not, support can be added incrementally by contributors interested in having their use case supported.

                                                                    1. 17

                                                                      I feel like Rust has definitely obliterated its complexity budget in unfortunate ways.

                                                                      I remember the time I asked one of the more well-known Rust proponents “so you think adding features improves a language” and he said “yes”. So it was pretty clear to me early on that Rust would join the feature death march of C++, C#, …

                                                                      Rust has many language features and they’re all largely disjoint from each other, so knowing some doesn’t help me guess the others.

                                                                      That’s so painfully true.

                                                                      For instance, it has different syntax for struct creation and function calls, their poor syntax choices also mean that structs/functions won’t get default values any time soon.

                                                                      ; is mandatory (what is this, 1980?), but you can leave out , at the end.

                                                                      The severe design mistake of using <> for generics also means you have to learn 4 different syntax variations, and when to use them.

                                                                      The whole module stuff is way too complex and only makes sense if you programmed in C before. I have basically given up on getting to know the intricacies, and just let IntelliJ handle uses.

                                                                      Super weird that both if and switch exist.

                                                                      Most of my friends who I’ve met through Rust have taken steps to cut interactions with “the Rust community” down to an absolute minimum due to it tending to produce a feeling of alienation over time.

                                                                      Yes, that’s my experience too. I have some (rather popular) projects on GitHub that I archive from time to time to not having to deal with Rust people. There are some incredibly toxic ones, which seem to be – for whatever reason – close to some “core” Rust people, so they can do whatever the hell they like.

                                                                      1. 6

                                                                        For instance, it has different syntax for struct creation and function calls

                                                                        Perhaps they are trying to avoid the C++ thing where you can’t tell whether foo(bar) is struct creation or a function call without knowing what foo is?

                                                                        The whole module stuff is way too complex and only makes sense if you programmed in C before. I have basically given up on getting to know the intricacies, and just let IntelliJ handle uses.

                                                                        It only makes sense to someone who has programmed in C++. C’s “module” system is far simpler and easier to grok.

                                                                        Super weird that both if and switch exist.

                                                                        Would you have preferred

                                                                        match condition() {
                                                                            true => {
                                                                            
                                                                            },
                                                                            false => {
                                                                        
                                                                            },
                                                                        }
                                                                        

                                                                        I think that syntax is clunky when you start needing else if.

                                                                        1. 1

                                                                          Perhaps they are trying to avoid the C++ thing where you can’t tell whether foo(bar) is struct creation or a function call without knowing what foo is?

                                                                          Why wouldn’t you be able to tell?

                                                                          Even if that was the issue (it isn’t), that’s not the problem C++ has – it’s that foo also could be 3 dozen other things.

                                                                          Would you have preferred […]

                                                                          No, I prefer having one unified construct that can deal with both usecases reasonably well.

                                                                          1. 2

                                                                            Why wouldn’t you be able to tell?

                                                                            struct M { };
                                                                            void L(M m);
                                                                            
                                                                            void f() {
                                                                                M(m); // e.g. M m;
                                                                                L(m); // function call
                                                                            }
                                                                            

                                                                            The only way to tell what is going on is if you already know the types of all the symbols.

                                                                            No, I prefer having one unified construct that can deal with both usecases reasonably well.

                                                                            Ok, do you have an example from another language which you think handles this reasonably well?

                                                                            1. 2

                                                                              The only way to tell what is going on is if you already know the types of all the symbols.

                                                                              Let the IDE color things accordingly. Solved problem.

                                                                              Ok, do you have an example from another language which you think handles this reasonably well?

                                                                              I’m currently in the process of implementing it, but I think this is a good intro to my plans.

                                                                              1. 1

                                                                                Let the IDE color things accordingly. Solved problem.

                                                                                The problem of course is for the writer of the IDE :)

                                                                                Constructs like these in C++ make it not only harder for humans to parse the code, but for compilers as well. This turns into real-world performance decreases which are avoided in other languages.

                                                                                I’m currently in the process of implementing it, but I think this is a good intro to my plans.

                                                                                That’s interesting, but I think there’s a conflict with Rust’s goal of being a systems-level programming language. Part of that is having primitives which map reasonably well onto things that the compiler can translate into machine code. Part of the reason that languages like C have both if and switch is because switch statements of the correct form may be translated into an indirect jump instead of repeated branches. Of course, a Sufficiently Smart Compiler could optimize this even in the if case, but it is very easy to write code which is not optimizable in such a way. I think there is value to both humans and computers in having separate constructs for arbitrary conditionals and for equality. It helps separate intent and provides some good optimization hints.

                                                                                Another reason why this exists is for exhaustiveness checks. Languages with switch can check that you handle all cases of an enum.

                                                                                The other half of this is that Rust is the bastard child of ML and C++. ML and C++ both have match/switch, so Rust has one too.


                                                                                I think you will have a lot of trouble producing good error messages with such a syntax. For example, say someone forgets an = or even both ==s. If your language does false-y and truth-y coercion, then there may be no error at all here. And to the parser, it is not clear at all where the error is. Further, this sort of extension cannot be generalized to one-liners. That is, you cannot unambiguously parse if a == b then c == d then e without line-breaks.

                                                                                On the subject, in terms of prior-art, verilog allows expressions in its case labels. This allows for some similar syntax constructions (though more limited since functions are not as useful as in regular programming languages).

                                                                        2. 3

                                                                          For instance, it has different syntax for struct creation and function calls, their poor syntax choices also mean that structs/functions won’t get default values any time soon.

                                                                          This is a good thing. Creating a struct is a meaningfully different operation from calling a function, and there’s no problem with having there be separate syntax for these two separate things.

                                                                          The Rust standard library provides a Default trait, with examples of how to use it and customize it. I don’t find it at all difficult to work with structs with default values in Rust.

                                                                          The whole module stuff is way too complex and only makes sense if you programmed in C before. I have basically given up on getting to know the intricacies, and just let IntelliJ handle uses.

                                                                          I don’t understand this comment at all. Rust’s module system seems fairly similar to module systems in some other languages I’ve used, although I’m having trouble thinking of other languages that allow you to create a module hierarchy within a single file, like you can do with the mod { } keyword (C++ allows nested namespaces I think, but that’s it). I don’t see how knowing C has anything to do with understand Rust modules better. C has no module system at all.

                                                                          1. 2

                                                                            I’m having trouble thinking of other languages that allow you to create a module hierarchy within a single file

                                                                            Lua can do this, although it’s not common.

                                                                            1. 1

                                                                              This is a good thing.

                                                                              I guess that’s why many Rust devs – immediately after writing a struct – also define a fun to wrap their struct creation? :-)

                                                                              Creating a struct is a meaningfully different operation from calling a function

                                                                              It really isn’t.

                                                                              The Rust standard library provides a Default trait, with examples of how to use it and customize it. I don’t find it at all difficult to work with structs with default values in Rust.

                                                                              That’s clearly not what I alluded to.

                                                                              I don’t see how knowing C has anything to do with understand Rust modules better. C has no module system at all.

                                                                              Rust’s module system only makes sense if you keep in mind that it’s main goal is to produce one big ball of compiled code in the end. In that sense, Rust’s module system is a round-about way to describe which parts of the code end up being part of that big ball.

                                                                              1. 3

                                                                                Putting a OCaml hat on:

                                                                                • Struct creation and function calls are quite different. In particular it’s good to have structure syntax that can be mirrored in pattern matching, whereas function call has no equivalent in match.
                                                                                • Multiple modules in one file is also possible in ML/OCaml. Maybe in some Wirth language, though I’m not sure on that one.

                                                                                it’s main goal is to produce one big ball of compiled code in the end.

                                                                                What other goal would there be? That’s what 100% of compiled languages aim at… Comparing rust to C which has 0 notion of module is just weird.

                                                                                1. 1

                                                                                  Struct creation and function calls are quite different. In particular it’s good to have structure syntax that can be mirrored in pattern matching, whereas function call has no equivalent in match.

                                                                                  In what sense would this be an obstacle? I would expect that a modern language let’s you match on anything that provides the required method/has the right signature. “This is a struct, so you can match on it” feels rather antiquated.

                                                                                  What other goal would there be? That’s what 100% of compiled languages aim at… Comparing rust to C which has 0 notion of module is just weird.

                                                                                  It feels like it was built by someone who never used anything but C in his life, and then went “wouldn’t it be nice if it was clearer than in C which parts of the code contribute to the result?”.

                                                                                  The whole aliasing, reexporting etc. functionality feels like it exists as a replacement for some convenience C macros, and not something one actually would want. I prefer that there is a direct relationship between placing a file somewhere and it ending up in a specific place, without having to wire up everything again with the module system.

                                                                                  1. 1

                                                                                    There is documented inspiration from OCaml from the rust original creator. The first compiler was even in OCaml, and a lot of names stuck (like Some/None rather than the Haskell Just/Nothing). It also has obvious C++ influences, notably the namespace syntax being :: and <> for generics. The module system most closely reminds me of a mix of OCaml and… python, with special file names (mod.rs, like __init__.py or something like that?), even though it’s much much simpler than OCaml. Again not just “auto wiring” files in is a net benefit (another lesson from OCaml I’d guess, where the build system has to clarify what’s in or out a specific library). It makes build more declarative.

                                                                                    As for the matching: rust doesn’t have active patterns or the scala-style deconstruction. In this context (match against values you can pre-compile pattern-matching very efficiently to decision trees and constant time access to fields by offset. This would be harder to do efficiently with “just call this deconstuct method”. This is more speculation on my side, but it squares with rust’s efficiency concerns.

                                                                                    1. 1

                                                                                      I see your point, but in that case Rust would need to disallow match guards too (because what else are guards, but less reusable unapply methods?).

                                                                                  2. 1

                                                                                    Comparing rust to C which has 0 notion of module is just weird.

                                                                                    Well there are translation units :) (though you can only import using the linker)

                                                                                2. 1

                                                                                  I’m having trouble thinking of other languages that allow you to create a module hierarchy within a single file,

                                                                                  Perl can do this.

                                                                                  1. 3

                                                                                    Elixir also allows you to create a module hierarchy within a single file.

                                                                                    1. 2

                                                                                      And Julia. Maybe this isn’t so rare.

                                                                                3. 1

                                                                                  ; is mandatory (what is this, 1980?), but you can leave out , at the end.

                                                                                  Ugh this one gets me every time. Why Rust, why.

                                                                                  1. 2

                                                                                    Same in Zig? Curious to know Zig rationale for this.

                                                                                    1. 10

                                                                                      In almost all languages with mandatory semicolons, they exist to prevent multi-line syntax ambiguities. The designers of Go and Lua both went to great pains to avoid such problems in their language grammars. Unlike, for example, JavaScript. This article about semicolon insertion rules causing ambiguity and unexpected results should help illustrate some of these problems.

                                                                                      1. 3

                                                                                        Pointing out Javascript isn’t a valid excuse.

                                                                                        Javascript’s problems are solely Javascript’s. If we discarded every concept that was implemented poorly in Javascript, we wouldn’t have many concepts left to program with.

                                                                                        I want semicolon inference done right, simple as that.

                                                                                        1. 4

                                                                                          That’s not what I’m saying. JavaScript is merely an easy example of some syntax problems that can occur. I merely assume that Rust, which has many more features than Go or Lua, decided not to maintain an unambiguous grammar without using semicolons.

                                                                                          1. 2

                                                                                            Why would the grammar be ambiguous? Are you sure that you don’t keep arguing from a JavaScript POV?

                                                                                            Not needing ; doesn’t mean the grammar is ambiguous.

                                                                                            1. 4

                                                                                              ~_~

                                                                                              Semicolons are an easy way to eliminate grammar ambiguity for multi-line syntax. For any language. C++ for example would have numerous similar problems without semicolons.

                                                                                              Not needing ; doesn’t mean the grammar is ambiguous.

                                                                                              Of course. Go and Lua are examples of languages designed specifically to avoid ambiguity without semicolons. JavaScript, C++, and Rust were not designed that way. JavaScript happens to be an easy way to illustrate possible problems because it has janky automatic semicolon insertion, whereas C++ and Rust do not.

                                                                                              1. 0

                                                                                                I’m completely unsure what you are trying to argue – it doesn’t make much sense. Has your triple negation above perhaps confused you a bit?

                                                                                                The main point is that a language created after 2000 simply shouldn’t need ;.

                                                                                                1. 5

                                                                                                  ; is mandatory (what is this, 1980?), but you can leave out , at the end.

                                                                                                  Same in Zig? Curious to know Zig rationale for this.

                                                                                                  The rationale for semicolons. They make parsing simpler, particularly for multi-line syntax constructs. I have been extremely clear about this the entire time. I have rephrased my thesis multiple times:

                                                                                                  In almost all languages with mandatory semicolons, they exist to prevent multi-line syntax ambiguities.

                                                                                                  Semicolons are an easy way to eliminate grammar ambiguity for multi-line syntax.

                                                                                                  Many underestimate the difficulty of creating a language without semicolons. Go has done so with substantial effort, and maintaining that property has by no means been effortless for them when adding new syntax to the language.

                                                                                                  1. 0

                                                                                                    Yeah, you know, maybe we should stop building languages that are so complex that they need explicitly inserted tokens to mark “previous thing ends here”? That’s the point I’m making.

                                                                                                    when adding new syntax to the language

                                                                                                    Cry me a river. Adding features does not improve a language.

                                                                                                    1. 1

                                                                                                      Having a clear syntax where errors don’t occur 15 lines below the missing ) or } (as would unavoidably happen without some separator — trust me, it’s one of OCaml’s big syntax problems for toplevel statements) is a net plus and not bloat.

                                                                                                      What language has no semicolon (or another separator, or parenthesis, like lisp) and still has a simple syntax? Even python has ; for same-line statements. Using vertical whitespace as a heuristic for automatic insertion isn’t a win in my book.

                                                                                                      1. 2

                                                                                                        Both Kotlin and Swift have managed to make a working , unambiguous C-like syntax without semicolons.

                                                                                                        1. 2

                                                                                                          I didn’t know. That involves no whitespace/lexer trick at all? I mean, if you flatten a whole file into one line, does it still work? Is it still in LALR(1)/LR(1)/some nice fragment?

                                                                                                          The typical problem in this kind of grammar is that, while binding constructs are easy to delimit (var/val/let…), pure sequencing is not. If you have a = 1 b = 2 + 3 c = 4 d = f(a) semicolons make things just simpler for the parser.

                                                                                                          1. 1

                                                                                                            Why are line breaks not allowed to be significant? I don’t think I care if I can write an arbitrarily long program on one line…

                                                                                                        2. 0

                                                                                                          Using vertical whitespace as a heuristic for automatic insertion isn’t a win in my book.

                                                                                                          I agree completely. I love Lua in particular. You can have zero newlines yet it requires no semicolons, due to its extreme simplicity. Lua has only one ambiguous case: when a line begins with a ( and the previous line ends with a value.

                                                                                                          a = b
                                                                                                          (f or g)() -- call f, or g when f is nil
                                                                                                          

                                                                                                          Since Lua has no semantic newlines, this is exactly equivalent to:

                                                                                                          a = b(f or g)()
                                                                                                          

                                                                                                          The Lua manual thus recommends inserting a ; before any line starting with (.

                                                                                                          a = b
                                                                                                          ;(f or g)()
                                                                                                          

                                                                                                          But I have never needed to do this. And if I did, I would probably write this instead:

                                                                                                          a = b
                                                                                                          local helpful_explanatory_name = f or g
                                                                                                          helpful_explanatory_name()
                                                                                                          
                                                                                        2. 3

                                                                                          Also curious, as well as why Zig uses parentheses in ifs etc. I know what I’ll say is lame, but those two things frustrate me when looking at Zig’s code. If I could learn the rationale, it might hopefully at least make those a bit easier for me to accept and get over.

                                                                                          1. 3

                                                                                            One reason for this choice is to remove the need for a ternary operator without greatly harming ergonomics. Having the parentheses means that the blocks may be made optional which allows for example:

                                                                                            const foo = if (bar) a else b;
                                                                                            
                                                                                            1. 8

                                                                                              There’s a blog post by Graydon Hoare that I can’t find at the moment, where he enumerates features of Rust he thinks are clear improvements over C/C++ that have nothing to do with the borrow checker. Forcing if statements to always use braces is one of the items on his list; which I completely agree with. It’s annoying that in C/C++, if you want to add an additional line to a block of a brace-less if statement, you have to remember to go back and add the braces; and there have been major security vulnerabilities caused by people forgetting to do this.

                                                                                              1. 6
                                                                                              2. 6

                                                                                                The following would work just as well:

                                                                                                const foo = if bar { a } else { b };
                                                                                                

                                                                                                I’ve written an expression oriented language, where the parenthesis were optional, and the braces mandatory. I could use the exact same syntactic construct in regular code and in the ternary operator situation.

                                                                                                Another solution is inserting another keyword between the condition and the first branch, as many ML languages do:

                                                                                                const foo = if bar then a else b;
                                                                                                
                                                                                                1. 2

                                                                                                  I don’t get how that’s worth making everything else ugly. I imagine there’s some larger reason. The parens on ifs really do feel terrible after using go and rust for so long.

                                                                                                  1. 1

                                                                                                    For what values of a, b, c would this be ambiguous?

                                                                                                    const x = if a b else c
                                                                                                    

                                                                                                    I guess it looks a little ugly?

                                                                                                    1. 5

                                                                                                      If b is actually a parenthesised expression like (2+2), then the whole thing looks like a function call:

                                                                                                      const x = if a (2+2) else c
                                                                                                      

                                                                                                      Parsing is no longer enough, you need to notice that a is not a function. Lua has a similar problem with optional semicolon, and chose to interpret such situations as function calls. (Basically, a Lua instruction stops as soon as not doing so would cause a parse error).

                                                                                                      Your syntax would make sense in a world of optional semicolons, with a parser (and programmers) ready to handle this ambiguity. With mandatory semicolons however, I would tend to have mandatory curly braces as well:

                                                                                                      const x = if a { b } else { c };
                                                                                                      
                                                                                                      1. 4

                                                                                                        Ah, Julia gets around this by banning whitespace between the function name and the opening parenthesis, but I know some people would miss that extra spacing.

                                                                                                      2. 3
                                                                                                        abs() { x = if a < 0 - a else a }
                                                                                                        
                                                                                                        1. 1

                                                                                                          Thanks for the example!

                                                                                                          I think this is another case where banning bad whitespace makes this unambiguous.

                                                                                                          a - b => binary
                                                                                                          -a => unary
                                                                                                          a-b => binary
                                                                                                          a -b => error
                                                                                                          a- b => error
                                                                                                          - a => error
                                                                                                          

                                                                                                          You can summarise these rules as “infix operators must have balanced whitespace” and “unary operators must not be followed by whitespace”.

                                                                                                          Following these rules, your expression is unambiguously a syntax error, but if you remove the whitespace between - and a it works.

                                                                                                          1. 1

                                                                                                            Or you simply ban unary operators.

                                                                                                            1. 1

                                                                                                              Sure, seems a bit drastic, tho. I like unary logical not, and negation is useful sometimes too.

                                                                                                              1. 1

                                                                                                                Not sure how some cryptic operator without working jump-to-declaration is better than some bog-standard method …

                                                                                                                1. 1

                                                                                                                  A minus sign before a number to indicate a negative number is probably recognizable as a negative number to most people in my country. I imagine most would recognise -x as “negative x”, too. Generalising that to other identifiers is not difficult.

                                                                                                                  An exclamation mark for boolean negation is less well known, but it’s not very difficult to learn. I don’t see why jump-to should fail if you’re using a language server, either.

                                                                                                                  More generally, people have been using specialist notations for centuries. Some mathematicians get a lot of credit for simply inventing a new way to write an older concept. Maybe we’d be better off with only named function calls, maybe our existing notations are made obsolete by auto-complete, but I am not convinced.

                                                                                            2. 9

                                                                                              My current feeling is that async/await is the worst way to express concurrency … except for all the other ways.

                                                                                              I have only minor experience with it (in Nim), but a good amount of experience with concurrency. Doing it with explicit threads sends you into a world of pain with mutexes everywhere and deadlocks and race conditions aplenty. For my current C++ project I built an Actor library atop thread pools (or dispatch queues), which works pretty well except that all calls to other actors are one-way so you now need callbacks, which become painful. I’m looking forward to C++ coroutines.

                                                                                              1. 3

                                                                                                except for all the other ways

                                                                                                I think people are complaining about the current trend to just always use async for everything. Which ends up complaining about rust having async at all.

                                                                                              2. 8

                                                                                                This is amazing. I had similar feelings (looking previously at JS/Scala futures) when the the plans for async/await were floating around but decided to suspend my disbelief because of how good previous design decisions in the language were. Do you think there’s some other approach to concurrency fit for a runtime-less language that would have worked better?

                                                                                                1. 17

                                                                                                  My belief is generally that threads as they exist today (not as they existed in 2001 when the C10K problem was written, but nevertheless keeps existing as zombie perf canon that no longer refers to living characteristics) are the nicest choice for the vast majority of use cases, and that Rust-style executor-backed tasks are inappropriate even in the rare cases where M:N pays off in languages like Go or Erlang (pretty much just a small subset of latency-bound load balancers that don’t perform very much CPU work per socket). When you start caring about millions of concurrent tasks, having all of the sources of accidental implicit state and interactions of async tasks is a massive liability.

                                                                                                  I think The ADA Ravenscar profile (see chapter 2 for “motivation” which starts at pdf page 7 / marked page 3) and its successful application to safety critical hard real time systems is worth looking at for inspiration. It can be broken down to this set of specific features if you want to dig deeper. ADA has a runtime but I’m kind of ignoring that part of your question since it is suitable for hard real-time. In some ways it reminds me of an attempt to get the program to look like a pretty simple petri net.

                                                                                                  I think that message passing and STM are not utilized enough, and when used judiciously they can reduce a lot of risk in concurrent systems. STM can additionally be made wait-free and thus suitable for use in some hard real-time systems.

                                                                                                  I think that Send and Sync are amazing primitives, and I only wish I could prove more properties at compile time. The research on session types is cool to look at, and you can get a lot of inspiration about how to encode various interactions safely in the type system from the papers coming out around this. But it can get cumbersome and thus create more risks to the overall engineering effort than it solves if you’re not careful.

                                                                                                  A lot of the hard parts of concurrency become a bit easier when we’re able to establish maximum bounds on how concurrent we’re going to be. Threads have a little bit more of a forcing function to keep this complexity minimized due to the fact that spawning is fallible due to often under-configured system thread limits. Having fixed concurrency avoids many sources of bugs and performance issues, and enables a lot of relatively unexplored wait-free algorithmic design space that gets bounded worst-case performance (while still usually being able to attempt a lock-free fast path and only falling back to wait-free when contention picks up). Structured concurrency often leans into this for getting more determinism, and I think this is an area with a lot of great techniques for containing risk.

                                                                                                  In the end we just have code and data and risk. It’s best to have a language with forcing functions that pressure us to minimize all of these over time. Languages that let you forget about accruing data and code and risk tend to keep people very busy over time. Friction in some places can be a good thing if it encourages less code, less data, and less risk.

                                                                                                  1. 17

                                                                                                    I like rust and I like threads, and do indeed regret that most libraries have been switching to async-only. It’s a lot more complex and almost a new sub-language to learn.

                                                                                                    That being said, I don’t see a better technical solution for rust (i.e. no mandatory runtime, no implicit allocations, no compromise on performance) for people who want to manage millions of connections. Sadly a lot of language design is driven by the use case of giant internet companies in the cloud and that’s a problem they have; not sure why anyone else cares. But if you want to do that, threads start getting in the way at 10k threads-ish? Maybe 100k if you tune linux well, but even then the memory overhead and latency are not insignificant, whereas a future can be very tiny.

                                                                                                    Ada’s tasks seem awesome but to the best of my knowledge they’re for very limited concurrency (i.e the number of tasks is small, or even fixed beforehand), so it’s not a solution to this particular problem.

                                                                                                    Of course async/await in other languages with runtimes is just a bad choice. Python in particular could have gone with “goroutines” (for lack of a better word) like stackless python already had, and avoid a lot of complexity. (How do people still say python is simple?!). At least java’s Loom project is heading in the right direction.

                                                                                                    1. 11

                                                                                                      Just like some teenagers enjoy making their slow cars super loud to emulate people who they look up to who drive fast cars, we all make similar aesthetic statements when we program. I think I may write on the internet in a way that attempts to emulate a grumpy grey-beard for similarly aesthetic socially motivated reasons. The actual effect of a program or its maintenance is only a part of our expression while coding. Without thinking about it, we also code as an expression of our social status among other coders. I find myself testing random things with quickcheck, even if they don’t actually matter for anything, because I think of myself as the kind of person who tests more than others. Maybe it’s kind of chicken-and-egg, but I think maybe we all do these things as statements of values - even to ourselves even when nobody else is looking.

                                                                                                      Sometimes these costumes tend to work out in terms of the effects they grant us. But the overhead of Rust executors is just perf theater that comes with nasty correctness hazards, and it’s not a good choice beyond prototyping if you’re actually trying to build a system that handles millions of concurrent in-flight bits of work. It locks you into a bunch of default decisions around QoS, low level epoll behavior etc… that will always be suboptimal unless you rewrite a big chunk of the stack yourself, and at that point, the abstraction has lost its value and just adds cycles and cognitive complexity on top of the stack that you’ve already fully tweaked.

                                                                                                      1. 3

                                                                                                        The green process abstraction seems to work well enough in Erlang to serve tens of thousands of concurrent connections. Why do you think the async/await abstraction won’t work for Rust? (I understand they are very different solutions to a similar problem.)

                                                                                                        1. 4

                                                                                                          Not who you’re asking, but the reason why rust can’t have green threads (as it used to have pre-1.0, and it was scraped), as far as I undertand:

                                                                                                          Rust is shooting for C or C++-like levels of performance, with the ability to go pretty close to the metal (or close to whatever C does). This adds some constraints, such as the necessity to support some calling conventions (esp. for C interop), and precludes the use of a GC. I’m also pretty sure the overhead of the probes inserted in Erlang’s bytecode to check for reduction counts in recursive calls would contradict that (in rust they’d also have to be in loops, btw); afaik that’s how Erlang implements its preemptive scheduling of processes. I think Go has split stacks (so that each goroutine takes less stack space) and some probes for preemption, but the costs are real and in particular the C FFI is slower as a result. (saying that as a total non-expert on the topic).

                                                                                                          I don’t see why async/await wouldn’t work… since it does; the biggest issues are additional complexity (a very real problem), fragmentation (the ecosystem hasn’t converged yet on a common event loop), and the lack of real preemption which can sometimes cause unfairness. I think Tokio hit some problems on the unfairness side.

                                                                                                          1. 3

                                                                                                            The biggest problem with green threads is literally C interop. If you have tiny call stacks, then whenever you call into C you have to make sure there’s enough stack space for it, because the C code you’re calling into doesn’t know how to grow your tiny stack. If you do a lot of C FFI, then you either lose the ability to use small stacks in practice (because every “green” thread winds up making an FFI call and growing its stack) or implementing some complex “stack switching” machinery (where you have a dedicated FFI stack that’s shared between multiple green threads).

                                                                                                            Stack probes themselves aren’t that big of a deal. Rust already inserts them sometimes anyway, to avoid stack smashing attacks.

                                                                                                            In both cases, you don’t really have zero-overhead C FFI any more, and Rust really wants zero-overhead FFI.

                                                                                                            I think Go has split stacks (so that each goroutine takes less stack space)

                                                                                                            No they don’t any more. Split Stacks have some really annoying performance cliffs. They instead use movable stacks: when they run out of stack space, they copy it to a larger allocation, a lot like how Vec works, with all the nice “amortized linear” performance patterns that result.

                                                                                                          2. 3

                                                                                                            Two huge differences:

                                                                                                            • Erlang’s data structures are immutable (and it has much slower single threaded speed).
                                                                                                            • Erlang doesn’t have threads like Rust does.

                                                                                                            That changes everything with regard to concurrency, so you can’t really compare the two. A comparison to Python makes more sense, and Python async has many of the same problems (mutable state, and the need to compose with code and libraries written with other concurrency models)

                                                                                                      2. 4

                                                                                                        I’d like to see a good STM implementation in a library in Rust.

                                                                                                    2. 6

                                                                                                      The fixation on async-await, despite it slowing down almost every real-world workload it is applied to, and despite it adding additional bug classes and compiler errors that simply don’t exist unless you start using it, has been particularly detrimental to the ecosystem.

                                                                                                      I’m curious about this perspective. The number of individual threads available on most commodity machines even today is quite low, and if you’re doing anything involving external requests on an incoming-request basis (serializing external APIs, rewriting HTML served by another site, reading from slow disk, etc) and these external requests take anything longer than a few milliseconds (which is mostly anything assuming you have a commodity connection in most parts of the world, or on slower disks), then you are better off with a some form of “async” (or otherwise lightweight concurrent model of execution.) I understand that badly-used synchronization can absolutely tank performance with this many “tasks”, but in situations where synchronization is low (e.g. making remote calls, storing state in a db or separate in-memory cache), performance should be better than threaded execution.

                                                                                                      Also, if I reach for Rust I’m deliberately avoiding GC. Go, Python, and Haskell are the languages I tend to reach for if I just want to write code and not think too hard about who owns which portion of data or how exactly the runtime schedules my code. With Rust I’m in it specifically to think about these details and think hard about them. That means I’m more prone to write complicated solutions in Rust, because I wouldn’t reach for Rust if I wanted to write something “simple and obvious”. I suspect a lot of other Rust authors are the same.

                                                                                                      1. 5

                                                                                                        The number of individual threads available on most commodity machines even today is quite low

                                                                                                        I don’t agree with the premise here. It depends more on the kernel, not the “machine”, and Linux in particular has very good threading performance. You can have 10,000 simultaneous threads on vanilla Linux on a vanilla machine. async may be better for certain specific problems, but that’s not the claim.

                                                                                                        Also a pure async model doesn’t let you use all your cores, whereas a pure threading model does. If you really care about performance and utilization, your system will need threads or process level concurrency in some form.

                                                                                                        1. 4

                                                                                                          I don’t agree with the premise here. It depends more on the kernel, not the “machine”, and Linux in particular has very good threading performance. You can have 10,000 simultaneous threads on vanilla Linux on a vanilla machine. async may be better for certain specific problems, but that’s not the claim.

                                                                                                          I wasn’t rigorous enough in my reply, apologies.

                                                                                                          What I meant to say was, the number of cores available on a commodity machine is quite low. Even if you spawn thousands of threads, your actual thread-level parallelism is limited to the # of cores available. If you’re at the point where you need to spawn more kernel threads than there are available cores, then you need to put engineering into determining how many threads to create and when. For IO bound workloads (which I described in my previous post), the typical strategy is to create a thread pool, and to allocate threads from this pool. Thread pools themselves are a solution so that applications don’t saturate available memory with threads and so you don’t overwhelm the kernel with time spent switching threads. At this point, your most granular “unit of concurrency” is each thread in this thread pool. If most of your workload is IO bound, you end up having to play around with your thread pool sizes to ensure that your workload is processed without thread contention on the one hand (too few threads) or up against resource limits (too many threads). You could of course build a more granular scheduler atop these threads, to put threads “to sleep” once they begin to wait on IO, but that is essentially what most async implementations are, just optimizations on “thread-grained” applications. Given that you’re already putting in the work to create thread pools and all of the fiddly logic with locking the pool, pulling out a thread, then locking and putting threads back, it’s not a huge lift to deal with async tasks. Of course if your workload is CPU bound, then these are all silly, as your main limiting resource is not IO but is CPU, so performing work beyond the amount of available CPU you have necessitates queuing.

                                                                                                          Moreover the context with which I was saying this is that most Rust async libraries I’ve seen are async because they deal with IO and not CPU, which is what async models are good at.

                                                                                                        2. 3

                                                                                                          Various downsides are elaborated at length in this thread.

                                                                                                          1. 2

                                                                                                            Thanks for the listed points. What it’s made me realize is that there isn’t really a detailed model which allows us to demonstrate tradeoffs that come with selecting an async model vs a threaded model. Thanks for some food for thought.

                                                                                                            My main concern with Rust async is mostly just its immaturity. Forget the code semantics; I have very little actual visibility into Tokio’s (for example) scheduler without reading the code. How does it treat many small jobs? Is starvation a problem, and under what conditions? If I wanted to write a high reliability web service with IO bound logic, I would not want my event loop to starve a long running request that may have to wait longer on IO than a short running request and cause long running requests to timeout and fail. With a threaded model and an understanding of my IO processing latency, I can ensure that I have the correct # of threads available with some simple math and not be afraid of things like starvation because I trust the Linux kernel thread scheduler much more than Tokio’s async scheduler.

                                                                                                        3. 3

                                                                                                          There’s no if-statement community

                                                                                                          That had me laughing out loud!

                                                                                                          1. 2

                                                                                                            probably because it’s if-expressions 🙃

                                                                                                          2. 2

                                                                                                            I hope I’m not opening any wounds or whacking a bee-hive for asking but… what sort of problematic interactions occur with the Rust community? I follow Rust mostly as an intellectual curiosity and therefor aren’t in deep enough to see the more annoying aspects. When I think of unprofessional language community behavior my mind mostly goes to Rails during the aughts when it was just straight-up hostile towards Java and PHP stuff. Is Rust doing a similar thing to C/C++?

                                                                                                          1. 5

                                                                                                            Ada looks really nice, and I would like to give it a serious try some day. Alas, I think rust is more ergonomic for “normal” programming (read: non embedded, on a modern machine), and has more amenities I’m personally used to. That includes cargo (makes building a breeze) and a decent LSP server implementation (rust-analyzer). I know AdaCore has been working on tooling a lot but I’m not sure how far along it is.

                                                                                                            Besides that, the syntax looks really a bit too verbose, but I think I can get over it if the feedback loop is tight enough — meaning again a good LSP server.

                                                                                                            1. 6

                                                                                                              I think rust is more ergonomic for “normal” programming (read: non embedded, on a modern machine),

                                                                                                              I’ve worked a fair bit with both languages and I’d say that, as far as pure language things are concerned, Ada is much easier to program in by virtue of not forcing you to think about lifetimes and borrowing. But this advantage quickly disappears when you try to use Spark’s equivalent concepts :).

                                                                                                              That includes cargo (makes building a breeze)

                                                                                                              The community effort Alire has reached v1.0 last week! The only thing really missing is the ton of crates that cargo has, but this is probably going to change now that there’s a central repository for libraries.

                                                                                                              and a decent LSP server implementation (rust-analyzer)

                                                                                                              There’s the ada_language_server but it’s true that it’s not as great as rust-analyzer (yet!). Syntax errors and jump-to-definition works really well though. There are also plans to add support for GCC’s -fdiagnostics-format=json to gnat, but it’s still a bit far from being ready.

                                                                                                              1. 4

                                                                                                                Thanks for the pointers to Alire and the LSP server, good to know.

                                                                                                                Ada is much easier to program in by virtue of not forcing you to think about lifetimes and borrowing.

                                                                                                                See, that’s not clear to me. Is there an equivalent of Rc / Arc? How do you pass stuff by reference from the caller’s stack frame? I only ever read about Ada’s approach to dynamic allocation being “it’s manual and unsafe” so I’d love to read more about, well, ergonomic alternatives. The borrow checker in rust is pretty neat and not that hard in the common case (it can be horrible if you try to avoid all allocations and have to add complex lifetime annotations though).

                                                                                                                1. 3

                                                                                                                  Is there an equivalent of Rc / Arc?

                                                                                                                  AFAIK, there is no “language-level” Rc type. Instead, you build your own with controlled types (you can read more about this here).

                                                                                                                  I only ever read about Ada’s approach to dynamic allocation being “it’s manual and unsafe” so I’d love to read more about, well, ergonomic alternatives.

                                                                                                                  Ada has a thing named “secondary stack” that allows you to return variable-length arrays/types that look like they’re on the stack, and it is often enough to help you avoid “traditional” dynamic allocations.

                                                                                                                  However it’s true that when you really need to allocate something on the heap, you’ll have to do it in a way that is less safe than Rust (unless you prove your program with Spark - then you get a similar level of safety but also a similar level of complexity :) ).

                                                                                                                  The borrow checker in rust is pretty neat and not that hard in the common case

                                                                                                                  I agree that it’s pretty neat (wonderful even!) but I disagree that it’s “not that hard”. It disallows a ton of useful patterns - you can usually re-arrange your program in a way that pleases it and you eventually get used to it, but it’s still a very annoying restriction.

                                                                                                                2. 1

                                                                                                                  How would you compare the Ravenscar or Jorvik profiles of Ada + Spark against Rust’s Send and Sync marker traits? I’m often frustrated by how difficult it is to bolt down various undesirable properties in Rust, and I keep hearing nice things about Spark in terms of mixing proofs with programs.

                                                                                                                  1. 2

                                                                                                                    How would you compare the Ravenscar or Jorvik profiles of Ada + Spark against Rust’s Send and Sync marker traits?

                                                                                                                    I’ve watched a few videos about Spark but I don’t know enough to answer authoritatively to this question, sorry.

                                                                                                                    I’m often frustrated by how difficult it is to bolt down various undesirable properties in Rust

                                                                                                                    I think Spark’s ability to prove that pre and post conditions hold is really good for this.

                                                                                                              1. 18

                                                                                                                If a software project actively goes out and gets users, which just about any project with a serious number of users has done, then yes, they have an obligation to those users. The reason is that they sold users on the idea of using their software. In other words, they were marketing their software, which means making promises.

                                                                                                                This argument is regularly contradicted by free software licenses themselves. Here is GPLv3, a copyleft license:

                                                                                                                This program is distributed in the hope that it will be useful,
                                                                                                                but WITHOUT ANY WARRANTY; without even the implied warranty of
                                                                                                                MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. 
                                                                                                                

                                                                                                                And here’s a permissive MIT license:

                                                                                                                THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,

                                                                                                                When does this supposed entitlement to a volunteer’s time end? When they leave the project? When they die?

                                                                                                                Paid free software development muddies the waters, because people employed to work on a free software project aren’t usually volunteers. Regardless, there is still a lack of warranty.

                                                                                                                1. 10

                                                                                                                  Literal interpretation of licenses will conclude that there was nothing wrong with event-stream version 3.3.6, which after all, was released under MIT license. event-stream’s maintainership was taken over and code was added to harvest private keys of Bitcoin accounts. Is that okay because the maintainer was a volunteer and code was provided WIHTOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED? I reject such interpretation.

                                                                                                                  https://blog.npmjs.org/post/180565383195/details-about-the-event-stream-incident.html

                                                                                                                  1. 4

                                                                                                                    Let’s be clear–what happened with event-stream and what may happen with other attacks on open source software should not be taken as an excuse for users to get free support. Using a giant dependency chain while taking absolutely no responsibility for locking it down and doing vulnerability checks (which are both supported by the npm ecosystem) is super irresponsible, perhaps even rising to the level of malpractice. And just to be clear, we shouldn’t place the blame solely on lazy or nefarious devs; this is a systemic problem in organizations that use open source software, starting from the top down.

                                                                                                                    1. 3

                                                                                                                      Agreed. As is often the case, what the legal document says is rather at odds with reality. There’s multiple layers in that:

                                                                                                                      • Is it what users want? Of course not.
                                                                                                                      • Is it ethical? Of course not.
                                                                                                                      • Is it legal? Mmmmmmmaybe? The license basically is there to put the onus of this argument on the user.
                                                                                                                      1. 1

                                                                                                                        There’s a reasonable argument that the event-stream update is piracy/unlawful intrusion in someone else’s computer. That goes beyond just breaking your code and directly into illegality. So, not the same thing at all.

                                                                                                                      2. 5

                                                                                                                        You are right.

                                                                                                                        I liked the article except for the “they have obligation part”. No way. Each piece of FOSS is just a precious gift. What if I release something and then die the next day. Do I have an obligation to not die?

                                                                                                                        1. 4

                                                                                                                          Yeah the bits about lib authors wanting users to hop onto their stuff sounded right. But then going on about an obligation to support the same set of features (platforms,languages..) for eternity is just plain wrong. Also it’s not like their working non-rust version is going away. People really could fork it and continue with that. There should be enough developers capable of doing that.

                                                                                                                          1. 6

                                                                                                                            I’d argue it’s worse than that. There’s this huge culture in the Linux and FreeBSD space which has been clearly demonstrated by this saga where distribution packagers/ports maintainers will build software in completely untested/unsupported configurations and then rouse a mob when the authors break these (despite never committing to support them in the first place).

                                                                                                                            1. 3

                                                                                                                              When you make a “minor patch” to your software, you kinda promise there won’t be any breaking change. Such as, no longer working on a bunch of relevant platforms.

                                                                                                                              Deprecation is okay. Just mark it as such, and do change the major version number when making breaking changes.

                                                                                                                              1. 7

                                                                                                                                All changes in open source software are made on a best-effort basis. No ‘promises’ are made, ‘kinda’ or otherwise. Publishing open source software does not entitle users to expect free support or any other expectations from the software. Let’s be really clear on this.

                                                                                                                                1. 1

                                                                                                                                  Oh, yeah, I didn’t allow for the possibility of an honest mistake. My bad. Of course any change can introduce bugs, so there’s that.

                                                                                                                                  What would not be okay would be insisting that this change is not breaking, even after being told it is. The correct response from the feedback they got, I believe, would be to revert the change, bump the major version number, then apply the change back. The old versions don’t even have to be maintained.

                                                                                                                            2. 1

                                                                                                                              Author here.

                                                                                                                              No, you don’t have an obligation to not die. :)

                                                                                                                              My broader point is that not all FOSS is a pure gift, but an exchange. We can definitely disagree on that, but your opinion is just as valid as mine. In fact, I fully acknowledge that I may be wrong. It’s just that my opinion is what it is based on my current experience.

                                                                                                                              1. 4

                                                                                                                                Your opinion is incorrect based on the actual license terms that you agree to when you use the software.

                                                                                                                                1. 2

                                                                                                                                  Legally, I agree with you. Socially? That is still debatable.

                                                                                                                                  1. 4

                                                                                                                                    As far as I know, open source projects don’t agree to any ‘social’ terms of service with users.

                                                                                                                                    EDIT: also, try saying that commercial software projects have a ‘social’ obligation to support you for free :-)

                                                                                                                                    1. 1

                                                                                                                                      Your edit is a good counterpoint.

                                                                                                                                      I think you and I have clarified where we disagree. I think it is best to leave the conversation there, with your leave. :)

                                                                                                                            3. 3

                                                                                                                              Using the licence’s legal disclaimers to absolve yourself of all actual responsibility is dishonest. I use the same legal disclaimers, and I would never dare.

                                                                                                                              When does this supposed entitlement to a volunteer’s time end? When they leave the project? When they die?

                                                                                                                              This is not a case of developers stopping to work on their product. This is a case of developers actively making the life of some of their users more difficult. They failed to do no harm.

                                                                                                                              1. 6

                                                                                                                                This is a case of developers actively making the life of some of their users more difficult.

                                                                                                                                I’d argue at the point that a distribution starts repackaging software in ways the authors haven’t tested, or shipping it on platforms the original authors never tested or supported, the users of that software are no longer the author’s responsibility but the distribution maintainer’s. Just because the authors didn’t list that the software definitely won’t work on a 30 year old DEC Alpha processor they are not suddenly owed to make it work there.

                                                                                                                                1. 3

                                                                                                                                  Well, I also happen to disagree with the very notion of Linux distribution. We shouldn’t need those middle men either.

                                                                                                                                  Nevertheless, depending on Rust is a breaking change. That would have warranted at least a major version bump. That’s how much effort I would have asked of them: increment a number. That would be enough to make it right in my book.

                                                                                                                                  1. 4

                                                                                                                                    It’s obviously not a breaking change in supported platforms, because it didn’t break those platforms. And breaking changes in unsupported platforms are, by definition, not supported.

                                                                                                                                    1. 1

                                                                                                                                      That’s something important I didn’t check: do they have an explicit description, or list, of supported platforms? If they did, that’s all good, and shame on distro maintainers for distributing them on unsupported platforms.

                                                                                                                                      If they did not… then the list of supported platforms is “wherever it builds and works out of the box”. Whether the maintainers like it or not.

                                                                                                                                2. 5

                                                                                                                                  There’s a world of difference between what the python-cryptography developers did and what happened with eventstream. The latter was intentionally malicious; the former was not. Legal language doesn’t absolve one of responsibility for malicious behavior.

                                                                                                                                  People are justified in being pissed off about the python-cryptography change. They’re justified in saying that “python-cryptography has broken trust with us”. They’re justified in applying Freedom 3 from GNU’s Four Freedoms and forking the project.

                                                                                                                                  They aren’t justified in feeling and voicing a sense of entitlement. That is all I’m saying.

                                                                                                                                  1. 2

                                                                                                                                    s/feeling and //

                                                                                                                                    Right? People can feel all kinds of weird and unfounded and unjust feelings and that’s OK.

                                                                                                                                    1. 2

                                                                                                                                      Excellent correction, thank you. It was the voicing and the language that I had a problem with.

                                                                                                                                  2. 4

                                                                                                                                    I use the same legal disclaimers, and I would never dare.

                                                                                                                                    So if someone sued you, you would tell your lawyer to ignore the legal disclaimer that would protect you? Why even use it at all, just use public domain.

                                                                                                                                1. 7

                                                                                                                                  a terrible take from a person who is full of 💩 https://campaign.gavinhoward.com/platform/

                                                                                                                                  the author is too shortsighted to see how shortsighted they are 🤷

                                                                                                                                  https://twitter.com/wbolster/status/1365983352835231744?s=19

                                                                                                                                  1. 15

                                                                                                                                    To be fair, author’s extremist views on christianity, society, medicine or politics doesn’t make him wrong on another unrelated subject. “You should first fix bugs instead of switching to a less portable language” is not a wrong thing to say. “You should not break other people’s operating systems” is not a wrong thing to say. Rust may be superior in terms of end product quality, but it is not the default choice for every situation.

                                                                                                                                    1. 17

                                                                                                                                      “don’t write bugs” doesn’t work despite 40 years of industry experience with unsafe languages. see other comments.

                                                                                                                                      the piece is littered with opinions about what others should do (with their spare time even), while at the same time maintaining poor people shouldn’t be allowed to vote, and holding other dehumanising views. imo, that is very relevant background: it tells me that whatever this person thinks that others should do is completely irrelevant.

                                                                                                                                      1. 4

                                                                                                                                        yes you are entitled to your opinion, so is the author else we could not have a dialog about these subjects. The view in the piece is “fix your bugs” and “fuzz your bugs” and “be responsible” not “don’t write bugs”.

                                                                                                                                        And Rust is about “preempt a class of bugs” well so is any language that consider nulls a design flaw for instance. So are languages that prevent side effects, that enforce exhaustive conditionals, that enforce exception handling, and so on. So it isn’t the ultimate language.

                                                                                                                                        1. 2

                                                                                                                                          “don’t write bugs” doesn’t work despite 40 years of industry experience with unsafe languages.

                                                                                                                                          Except in cryptography. In this particular niche, “don’t write bug” is both mandatory and possible. In this particular niche, Rust is of very little help.

                                                                                                                                          That said, the author may not be aware of the specifics of cryptography. He may be right for the wrong reasons.

                                                                                                                                        2. 13

                                                                                                                                          I think “consistently being wrong” is a valuable insight, and can span unrelated subjects.

                                                                                                                                          1. 5

                                                                                                                                            “You should not break other people’s operating systems” is not a wrong thing to say.

                                                                                                                                            Very reasonable, but not what’s happening, nor what he’s saying.

                                                                                                                                            What’s happening is “making a change to one software project”, that is provided under a license that does not guarantee support.

                                                                                                                                            What he’s saying is “changing what platforms you support is unacceptable”. He’s also saying “switching to Rust is a dereliction of duty”. Which implies “you have a duty that is not listed in your software license, and which I won’t elaborate on”.

                                                                                                                                            In other words, what he’s saying is, ultimately, “nobody should make changes to their software that I disapprove of”. Which is wildly unreasonable.

                                                                                                                                            Unsurprisingly, his political views skew towards “the only people who are allowed to be part of society are people that I approve of” (he approves only of a certain subset of Christian faithful, who must also be straight and cisgendered, believe that certain parts of the Constitution are invalid, and be in the top fraction of earners).

                                                                                                                                            In other words, his poor political thinking mirrors his thinking on the politics of open source development in ways that make it relevant to the conversation.

                                                                                                                                            1. 2

                                                                                                                                              What’s happening is “making a change to one software project”, that is provided under a license that does not guarantee support.

                                                                                                                                              What’s happening is “making a breaking change” without marking it as such (deprecation, major version number bump, that kind of thing). That’s not okay. I don’t care it was a labour of love provided for free. The rules should be:

                                                                                                                                              1. Don’t. Break. Users. Pretty please.
                                                                                                                                              2. If you break rule (1), bump the major version number.
                                                                                                                                              3. If rule (1) was broken, keep the old versions around for a while. Bonus point if you can actually support them (fix bugs etc).
                                                                                                                                              1. 5

                                                                                                                                                It’s not a breaking change if it breaks on platforms that were never explicitly supported (not even by python). (I’m not entirely sure if they used to support these explicitly, but it’s not obvious).

                                                                                                                                                1. 2

                                                                                                                                                  I agree if there’s an explicit description of supported platforms. If not… the only reasonable fallback would be any platform supported by Python where it builds & run out of the box. That can mean a lot of platforms.

                                                                                                                                                2. 2

                                                                                                                                                  If you break rule (1), bump the major version number

                                                                                                                                                  They did, at least for certain values of “major version number”. Rust was introduced in 3.4. The x.y releases are when backwards-incompatible changes are introduced. They’re changing their versioning scheme to make it more explicity: next major version will be 35 (instead of 3.5).

                                                                                                                                                  Honestly, a quick look at their changelog shows backwards-incompatible changes at 3.3, 3.1, 3.0, 2.9, … In other words, adding rust when they did was entirely in line with their release cycle.

                                                                                                                                                  1. 1

                                                                                                                                                    I commend them for listening to feedback (or is it cave in to mass anger?), and switch to semantic versioning. That’s cogent evidence of trustworthiness in my book.

                                                                                                                                            2. 2

                                                                                                                                              Author here.

                                                                                                                                              Everyone is full of crud on some level. However, interacting with people nicely on the Internet is a good way for me to get rid of that and to become less of a terrible person.

                                                                                                                                              On that note, hi! I’m Gavin. Nice to meet you. :)

                                                                                                                                            1. 10

                                                                                                                                              While the average Rust code is much safer than the average C code, even in the hand of very competent developers, we must keep in mind that cryptographic code is not average. Especially modern cryptographic code, designed after NaCl.

                                                                                                                                              • It is pathologically straight-line, with very few branches.
                                                                                                                                              • It has pathologically simple allocation patterns. It often avoids heap allocation altogether.
                                                                                                                                              • It is pathologically easy to test, because it is generally constant time: we can test all code paths by covering all possible input & output lengths. If it passes the sanitizers & Valgrind under those conditions, it is almost certainly correct (with very few exceptions).

                                                                                                                                              You thought writing cryptographic code would be harder to write than application code? I mean, don’t everyone tell you not to roll your own? Well, the answer is two-fold: the logic of cryptography is often very delicate. Rust won’t save you here. But the system aspects of it are often very easy. Rust will help you there, but we hardly need that help to begin with.

                                                                                                                                              I have to agree with the author here. There was no need to rewrite it in Rust, and the decision to do so anyway is most probably not worth the trouble. Especially damning is treating this major breaking change as if it was a mere patch. Affected users should probably leave and use something else.

                                                                                                                                              Speaking of which, Shameless plug time: Monocypher is an extremely simple crypto library, written in portable C99. It has Python bindings, written by a user who needed it to update the firmware of the embedded device they sell. If you were using this crypto library and your platform doesn’t support Rust, take a look at Monocypher. It’s not a drop-in replacement, but it might be a worthy alternative.

                                                                                                                                              1. 5

                                                                                                                                                Or, instead of using a non audited library written by a single person, look for actual improvements like project Everest where absence of memory errors, and validity of the code, are proven formally, not just trusted because “fuzzer says it’s ok”.

                                                                                                                                                1. 7

                                                                                                                                                  non audited library written by a single person

                                                                                                                                                  Two things you should probably have checked before writing this:

                                                                                                                                                  Now Project Everest sounds very nice, if you can get it to build on your particular platform, with little enough effort. By comparison, Monocypher is basically a single file C library, extremely easy to deploy for C/C++ project, and easy to write bindings for (though it already has bindings for Python, .NET, WASM, Rust, Go, and more. I think that count as an “actual improvement” over TweetNaCl and Libsodium in some niches.

                                                                                                                                                  1. 3

                                                                                                                                                    Ah, good about the successful recent audit, I wrote that based on memories from earlier :-). That changes my view a bit on your library, and maybe some day, if it gets OCaml bindings, I might use it.

                                                                                                                                                    1. 6

                                                                                                                                                      And now I regret the salt in my earlier comment. :-)

                                                                                                                                                      maybe some day, if it gets OCaml bindings, I might use it.

                                                                                                                                                      You can find the list of language bindings here. Someone did the Ocaml bindings there. You may want to take a look, perhaps get in touch with the author if you feel like contributing.

                                                                                                                                              1. 8

                                                                                                                                                I hope it’s not too obvious, given who wrote this and who they were talking to respectively, but formal methods and category theory are easily far more powerful than their current applications would suggest. Even mathematicians are still skeptical of these fields; many folks have a lot of catching up to do. An example in formal methods might be Metamath, a syntax-driven prover capable of handling multiple different foundations of maths. It is faster than type-driven provers, verifying thousands of proofs per second. In category theory, Chu spaces generalize matrices, but also generalize a broad range of set-like objects, and have unexplored connections to programming and digital logic.

                                                                                                                                                1. 1

                                                                                                                                                  Metamath is also very, err, quirky. The usability is pretty low, I think, compared to other proof assistants. I think metamath-zero is a promising replacement with better foundations and barely higher complexity.

                                                                                                                                                1. 8

                                                                                                                                                  I wonder whether choice of programming language affects perception here. When I use jq or awk, for example, it feels very obvious that I’m constructing a filter from inputs to outputs. As requested, here is a non-trivial jq program; Curry-Howard says that it takes a presentation of a category and constructs the Knuth-Bendix completion.

                                                                                                                                                  If we have a countably infinite number of objects, then we can index them with the natural numbers. The Curry-Howard way to interpret “there is an infinite number of objects with property X” is with a program that maps natural numbers to objects and any extra witnesses required for the property. If there is an infinite number of primes, then Curry-Howard gives us a program which takes a natural number and returns the indexed member of the sequence [2, 3, 5, 7, …] along with a witness of primality.

                                                                                                                                                  Let’s walk through a garden of constructive proofs in elementary logic. We’ll consider what Curry-Howard says about a few examples. And yes, like the post says, many of these are boring.

                                                                                                                                                  • The praeclareum theorema is the lambda term λ (f, g). λ (x, y). (f x, g y). Curry-Howard says that because we only used lambda calculus with products, this statement is true in any CCC, and hints that maybe we only need products. Curry-Howard also lets me read that lambda term directly from a proof of the theorem.
                                                                                                                                                  • The fact that equality of natural numbers is decideable (proof) can be used to produce programs which take two natural numbers and return a disjoint union whose left side indicates that the inputs are equal and whose right side indicates that they are unequal.
                                                                                                                                                  • The fact that the axiom of choice implies excluded middle, Diaconescu’s theorem, gives a program (proof). The axiom of choice is passed in as a polymorphic choice function, and the program takes an input type, looks up the choice function, and builds a program which decides equality on that type. The choice functions themselves take a type and an value of that type, which is a constructive proof that the type is inhabited, and return another value of the same type along with a witness which shows that the two values give an ordered pair. (This is confusing to everybody, and Metamath has an explanation of this encoding.)

                                                                                                                                                  But beyond all of that, Curry-Howard lets us consider the final entry on this table of correspondences, which I’ve discussed before here: We can generate programming languages for interesting mathematical objects of study. Choose a synthetic domain of objects and receive a lambda calculus.

                                                                                                                                                  1. 7

                                                                                                                                                    I’m unclear about the relevance of any of this. The OP talks about programs and proofs. How does discussing axiom of choice and the decidability of equality of natural numbers matter?

                                                                                                                                                    1. 1

                                                                                                                                                      The proofs I chose are strongly related to computability via the BHK interpretation. But they can also just be seen as four arbitrary logical statements, one of which happens to be the one used in the original article.

                                                                                                                                                      I am not sure how to cross the bridge any further. Given any constructive proof, there is a program whose closure is the proof’s context, whose inputs are the proof’s hypotheses, whose subroutines are the proof’s subproofs, and whose outputs are the proof’s conclusions. Consider this (untested) Python code:

                                                                                                                                                      def isEqual(x, y):
                                                                                                                                                          if x == 0 and y == 0:
                                                                                                                                                              return True
                                                                                                                                                          elif x > 0 and y > 0:
                                                                                                                                                              return isEqual(x - 1, y - 1)
                                                                                                                                                          else:
                                                                                                                                                              return False
                                                                                                                                                      

                                                                                                                                                      Apply a solid dab of native type theory and we can see that this is the same control flow that we would have in a logical proof of the equality of two natural numbers. Either they’re both zero and they’re equal, or they’re both successors and they’re equal if their predecessors are equal, or one and not the other are zero and they’re not equal. (Note that Python’s native type theory requires us to presume that x and y are natural numbers and not anything else.)

                                                                                                                                                    2. 2

                                                                                                                                                      I’m a bit confused by the jq program. I’m no categorician so 1/3rd of CH escapes me anyway, it seems; but what would be the type of this jq program? What is it a proof of?

                                                                                                                                                      If you’re saying that it relies on CH to build a completion of a category, that’s cool, but it still doesn’t refuse my point I think. I have an OCaml theorem prover, in the dozens of klocs, which implements a more complicated version of KB completion and its type is still unit (or set expr -> set expr if you look at the main loop).

                                                                                                                                                      1. 1

                                                                                                                                                        jq programs are generally endomorphisms on JSON data. Recall that programs don’t have the one single type, but a family of types which are related by their own little Boolean algebra. It is up to our choice of logical formalism to decide which types go where. I could say that my program is a map from categories to graphs, for example, and it would not be any more or less true; it is up to me to explain how the incoming JSON data can be arranged to present a category, not for the data itself to innately be a category in some way.

                                                                                                                                                        My point is that CH is not something upon which rely, but something which happens to arise within these mathematical structures, even if we didn’t want it. And as for practical applications, I think that using CH to produce domain-specific small programming languages is quite practical.

                                                                                                                                                        1. 2

                                                                                                                                                          Recall that programs don’t have the one single type

                                                                                                                                                          That’s debatable, I guess :-). OCaml certainly has principal types (for the core language anyway) and principal type inference outside the extensions like GADTs. When you add a layer of boolean interpretation (which is definitely useful! 100% agree!) then you kind of segue from “writing a program” to “writing a program and verifying properties about it” which as often as not is done with different mechanisms such as Hoare triplets, with classical logic, etc. Idris is probably the closest, in the real world, of the CH style of writing programs and verifying actual properties about them directly by well-typedness; but it’s not the only approach.

                                                                                                                                                    1. 1

                                                                                                                                                      Here’s why Curry-Howard is important to programmers even with concrete types. When we express the properties we want at the type level, we have a mathematical guarantee that things can’t go wrong. That’s the whole point for us–that things can’t go wrong. For example, consider this code (OCaml syntax):

                                                                                                                                                      type person
                                                                                                                                                      type name
                                                                                                                                                      
                                                                                                                                                      val name : string -> name option
                                                                                                                                                      val person : id:int -> name -> person
                                                                                                                                                      

                                                                                                                                                      This code guarantees that a person value can be constructed with any int value as an ID, but only with a valid name value, which can be constructed only by following the rules encoded in the name function. The types enforce that these logical rules must be followed. If you have a name value, you have a proof that it was constructed correctly. And if you have a person value, you also have a proof that it was constructed correctly.

                                                                                                                                                      Simple, everyday code that gives you mathematical proofs that it will work correctly. That’s why C-H is important.

                                                                                                                                                      1. 5

                                                                                                                                                        Why do you need C-H for this? You can constrain input to sets just fine and make assertions over the domain and range of pure functions well enough without invoking C-H. TLA+ after all models algorithms using set theoretic constructions. So what is C-H giving you here?

                                                                                                                                                        1. 1

                                                                                                                                                          It’s giving me a simple model for thinking about my code, using a system (static types) that is mainstream and widely available. If I set up my types correctly, then the programs I construct using them can be provably correct. This is cool because this tool is accessible to working developers today.

                                                                                                                                                        2. 1

                                                                                                                                                          Sure, and I use a ton of these in OCaml! But this is clearly on the “program” side of things. These are not proofs of anything a mathematician would call a theorem. They’re just statements about the program, which helps understanding it and allow the compiler to remove a ton of runtime checks; but nothing more. Trying to coerce OCaml into proving non trivial stuff with its types gives you michelson whose design is heavily informed by what you can and can’t do with GADTs. If you want better proofs for OCaml, use Why3 or the upcoming gospel from the same team.

                                                                                                                                                          1. 3

                                                                                                                                                            The fact that you can have a type system at all is a consequence of C-H. Of course that standard programming languages’ type systems make lousy theorem provers, so what? Similarly, the theorems that arise from “regular” programs are not mathematically interesting, but again, so what? How does this make C-H a scam?

                                                                                                                                                            In the end C-H is more important to mathematicians than programmers, as it allows for things like Coq to exist. I find the idea of C-H not being important very bizarre. Before C-H, the idea that mathematics could be formalized at all was a hypothesis. C-H shows not only that it is true, but also shows you how to do it. It’s one of the most profound mathematical discoveries of the 20th century.

                                                                                                                                                        1. 2

                                                                                                                                                          i think there’s a confusion here – curry-howard is a statement about running programs as proofs, not about programs as such as proofs. of course we can’t have a programming language that expresses first-order logic at the syntactic level; the compilation of the program would be undecidable.

                                                                                                                                                          1. 6

                                                                                                                                                            we can’t have a programming language that expresses first-order logic at the syntactic level; the compilation of the program would be undecidable.

                                                                                                                                                            We have heaps of languages whose complication is undecidable! Any language with macros. C++ templates. Java generics. TypeScript’s Type system …

                                                                                                                                                            1. 1

                                                                                                                                                              Is it? my understanding is that it’s “the program is a proof of its type”, not “running this program gives you a witness” kind of thing (like reflection in Coq could give you).

                                                                                                                                                              There are languages designed for writing verified code, like Dafny or Why3, and they do embed first-order logic; simply it’s in separate code annotations that express Hoare-logic invariants. Compilation remains decidable, but verification/proving is obviously not.

                                                                                                                                                            1. 18

                                                                                                                                                              Okay, I’ll bite, despite the click-baity title (A scam? Seriously? Who’s attempting to deceive anyone? Is there money to be gained fraudulently here?)

                                                                                                                                                              The value in Curry-Howard, like so many things, is not at the extremes - like the example programs here that only prove vague and uninteresting things, or the complex proofs that don’t give you much computational behaviour - but somewhere in the middle. That is, programs that express some lightweight invariant that needs to be maintained, so there is value in expressing it in the type meaning that you have a proof that it is maintained. Here’s an example from the Idris 2 implementation:

                                                                                                                                                              eval : {free, vars : _} ->
                                                                                                                                                                     Env Term free -> LocalEnv free vars ->
                                                                                                                                                                     Term (vars ++ free) -> Stack free -> Core (NF free)
                                                                                                                                                              

                                                                                                                                                              This type says that we have an environment of free variables free, some additional bound local variables vars, and the process of evaluating an expression gives us a normal form which doesn’t refer to the bound variables any more, because they’ve been substituted in. And I know that’s true, because the type says so, and the type checker agrees. Variable scoping is easy to get wrong, so I’ve decided it’s important to prove it’s right throughout.

                                                                                                                                                              Here’s another example, more contrived but I think easier to understand:

                                                                                                                                                              uncompress : RLE xs -> Singleton xs
                                                                                                                                                              

                                                                                                                                                              That’s the type of a program which takes a compressed, run-length encoded representation of a list xs, and gives back the uncompressed representation. It’s both a program which does the uncompression, and a proof that the uncompressed list is the same as the original. Or, maybe you could read it as: “For all run-length encoded lists, there is a way to reconstruct the original list, and this is it.”

                                                                                                                                                              Is Curry-Howard overrated? Probably. I’d even have read the article if that’s what the title said, and I’d probably have largely agreed with it. But even so, it’s a useful way to understand what’s going on in languages with more expressive type systems.

                                                                                                                                                              The internet is already full of articles with clickbaity titles that take an extreme and infer some general negative conclusion from it. Let’s not have more of them.

                                                                                                                                                              1. 2

                                                                                                                                                                The value in Curry-Howard, like so many things, is not at the extremes

                                                                                                                                                                Yup. It allows us to reason about our code in the same way we can reason about mathematical proofs. That’s about it. That’s both extremely powerful and useless, depending on your environment and what you’re trying to do.

                                                                                                                                                                I think a lot of this gets back to what another commenter said: tooling and language choice. The program is not the proof, but the running of the program can work just like a proof if you set it up correctly. That’s an extremely cool observation. Not such a good essay.

                                                                                                                                                                1. 3

                                                                                                                                                                  Yup. It allows us to reason about our code in the same way we can reason about mathematical proofs. That’s about it. That’s both extremely powerful and useless, depending on your environment and what you’re trying to do.

                                                                                                                                                                  But why do you need C-H to do this reasoning? C-H is a much more narrow result, specifically proving a duality between proof and program. Verification of invariants does not require C-H.

                                                                                                                                                                2. 2

                                                                                                                                                                  Author here. I should have titled it “over hyped” or “overrated” indeed (in the conclusion I do acknowledge the click baitiness, but oh well ^^). I do love type driven programming, even from my lowly OCaml vantage point, and Idris is pretty cool. The eval example is impressive.

                                                                                                                                                                  Excerpt which hopefully isn’t too far off:

                                                                                                                                                                  Idris could possibly have some interesting proofs that are also real programs… if it were designed to be a proof assistant and not a beefed-up programming language.

                                                                                                                                                                1. 13

                                                                                                                                                                  Even for IRs, this article seems to say “tagged unions are better and more ergonomic, but you can live without them” (including the exhaustiveness checking mentioned at the end). So it’s not really “overrated”, just “you can write code without them, with more pain” which holds for almost all PL constructs.

                                                                                                                                                                  1. 8

                                                                                                                                                                    Yeah alternative title: “tagged unions are great and you should emulate them in languages that don’t natively support them”

                                                                                                                                                                    1. 2

                                                                                                                                                                      I’ve mentioned this a bunch of times, but for those who haven’t seen it, Oil uses the same DSL as Python to describe “tagged unions”, called Zephyr ASDL.

                                                                                                                                                                      https://www.oilshell.org/blog/2016/12/11.html

                                                                                                                                                                      https://www.oilshell.org/blog/tags.html?tag=ASDL#ASDL

                                                                                                                                                                      Right after I put it into the codebase I saw how much better the code was structured (even without pattern matching). And it continues to grow more useful after 4 years.

                                                                                                                                                                      It can now even express relationships that Rust can’t, i.e. what I’d call “first class variants”: https://github.com/rust-lang/rfcs/pull/2593

                                                                                                                                                                      (and it doesn’t have the ergonomic issues with boxing, etc.)

                                                                                                                                                                      In Oil’s case it compiles to BOTH statically typed Python and C++. It works in both cases. Objects and subtyping are sort of “dual” to sum types.

                                                                                                                                                                      So the bottom line is that you can code in an imperative language (Python, Java, C++), and still structure your compiler nicely. You can have the best of both worlds!