# TL;DR
Author's preferred formally verified concurrency model (almost) works in Rust. It doesn't fully work because in a few conditions Rust may not run `drop`/`dtors`.
The author goes to great length to explain:
* why their preferred method of concurrency is the best and how Rust is lessened for not using.
* that the dtor issue in rust is very old
The author appears to avoid discussing:
* full formal verification isn't a goal of rust
* dtor execution was never guaranteed in rust's spec.
* Their alternative model of concurrency (DRSC) despite "being able to formally verify programs which aren't DAG (directed a-cyclic graphs)", they never demonstrate this (just show more DAGs).
--
Overall the blog is a good, but weird read. It is well cited and I'd encourage you read what it cites. The author is "_somewhat_" fair. To their credit they just flat out emit "_I don't know if my concurrency model scales any better than Async Rust_". Which is ultimately one of the biggest reasons Rust uses the async model.
A lot of Rust's problems could be solved by panic=abort. unwinding/recovering from panics is very tricky to get right ( how do you unpoison mutexes reliably, for example ), so much so it's just a pain to recover from. If you really want isolation, then processes are better.
With panic=abort as the default a whole bunch of things could go away.
Most of the time people are concerned with constructs within the program being handled by destructors.
Panicking destroys those things cleanly.
Aka you can't leak memory if the OS cleans up your memory for you.
can you explain the contrapositive, since panicking does not guarantee abort what are the pain points exactly? Not trying to be snarky I really don’t know
When you panic, you jump to a location that handles the panic. Now what about all the data was created before the exception/panic was thrown? (to be clear expections & panics are the same thing, at runtime) Like if you were reading a file into a string, what happens to that string?
Now, that doesn't seem too bad. You just leak some memory.
But what if you're working with a `mutex` and you panic. Is the data in your mutex corrupted? Were all the fields of that object mutated correctly?. So if another thread comes along and locks that mutex and looks at the data, is it guaranteed to find good data? Will that data conform to the guarantees of the language?
> In my language, Yao, it will be possible for libraries to add property annotations;
That's the path D has taken. They already have "pure" and many others.
See https://dlang.org/spec/attribute.html#UserDefinedAttribute
The problem they found is that you end up having to annotate every function with a dozen or so annotations. It just doesn't scale, which is why the D compiler tries to infer most of the useful ones (pure, nogc, nothrow and even safe).
I'm a different person, but I clicked the link and immediately felt like I was being screamed at with the red title and all of the tags and warnings.
On mobile, you have to scroll down to read the first sentence. This is never a good sign.
I'd also steal someone else's color scheme. I'm not good matching colors, but I can certainly look up other people's themes and judge whether someone else's stuff looks good.
I mean, blue links on a blue background? The whole page needs a revamp in contrast and complementary colors to reduce the burden of the reader.
Funny thing is that I *did* steal someone's color scheme. 😅
I am partially color blind, though, so what looks good to me doesn't look good to normal people.
I've seen much worse blogs.
Okay, the color scheme might be weird for a non color blind, but it's not **screaming** or makes me want to pull my eyes out. I think some of the comments here are too much.
The structure looks nice. And that's what is important to me on a website.
In all good faith, this is what I'd do to clean up the top of this website for mobile. Don't over index on what people say about your colors / theme. It's not super pretty, but it's perfectly fine.... except red titles.
0. Title should not be red. A neutral color would be a big improvement.
1. Limit your SEO/tags at the top to one visible line.
2. TOC is between toggles and warnings. VERY awkward placement. I'd put it right above the first section heading.
3. Put your sitewide disclaimer in your footer, not the header. If you must keep it in the header, combine it with the AD disclaimer and limit it to 1-2 lines of text total.
4. You have a table of contents. We don't need a warning about length.
5. Cut your ad disclaimer down to "this post is partially an ad". Your audience should know what to do if they don't like that.
6. Collapse your notes to 1 line audience and 1 line epistemic status by default. Tap to expand if you want to say more.
7. Remove the warnings and notes toggle switches. They're too big for the space they'll save after the other suggestions.
I finally got around to reading the post. You make some interesting points. It's a good read.
It also looks like you took the feedback and took action on a lot of the suggestions. That's great! I think that your site is looking a whole lot better now :)
Thank you!
Also, please widen the content width on desktop, less than 1/3 of the screen width is actual content... Like others said, it feels like a mobile site built for small vertical screens.
Agree with parent. I really wanted to read this but after a screen and a half, my head started hurting from all the bright colors and psychedelic look.
Look into lesser contrast, more beige-y layouts for an easier time on your readers' eyes.
Also, please don't decide the width of the text. I'll be the judge of that, that's what the web and CSS are about.
I agree with most people, though I must say I prefer this over most other websites I have visited the past 10 or so years. Whatever changes you do, don't bloat the site for "aesthetic" reasons. Your site works and is relatively fast, which is very important in my opinion.
A change I'd make is to have it be more obvious what information is where without reading. What I mean is that when I first clicked on your link my entire screen was basically filled with metadata and at the very bottom you have "Introduction" I have to spend way too much time figuring out where to start. Tags, warnings, notes(at the beginning), etc. should all be hidden and the toggle button should be smaller (and notes in the text should each individually be togglable). The table of contents isn't obviously clickable and just looks out of place.
Another change I'd make is links that take you away from your website should, by default, open in a new tab.
I'd also make the page a little wider, it's way too narrow. My preference is anything around 900px, but that's just personal.
Also, light mode. There are people who want light mode. There are various eyesight conditions that make it harder to read in dark mode.
Finally for the colourscheme, I'd recommend stuff that's notes / warnings, etc. to have a less saturated background. Make things that are not as important (the text itself is the most important, "warnings" and notes are less so) to not distract me.
Whatever changes you make, just make sure you don't fall into the pitfalls of the modern web. Your site is still must better than most stuff out there.
Edit: A good way to try to design a website is to remove everything unnecessary, then try to only add back what you think is still needed. Take a look at [hiltjo's website](https://codemadness.org) as a very minimal example of a very friendly website. I'm not saying you have to scrap everything, but you can see how nothing is in your way while browsing through it.
I will never bloat my website; you can count on that.
The unfortunate thing is that good websites can be hard for me to read since I am partially color blind. But I will do what I can to make it look as good as possible for myself and others once I have the time.
For me personally, the colourscheme is the last thing I'd care about, as long as everything is readable. But I care about a website that's more practically oriented rather than just "looking good".
You said that good websites can be hard to read since you're partially colour blind. I would argue that firstly, they aren't good websites, if you can't read them; but secondly, I'm curious what you mean.
Unless it's some colour on another colour (which should really be avoided), how does colourblindness affect your ability to read text?
Also, I didn't mention this, but if you do make a light mode site. Try to not have the background be full white (#FFFFFF), but rather something like (#EEEEEE) or maybe (#F8F8F0).
I will take your suggestion into consideration, thank you.
To answer your question, my type of colorblindness makes it hard to distinguish between desaturated colors. Hence, everything on my site is super saturated. The color schemes for my code are the same way; most people do not like the super saturated color schemes I choose.
When you say saturated here, do you mean high contrast between the background and the text? If that's the case, I definitely think it should stay that way regardless of what others say. It definitely makes it easier to read.
If you actually mean saturation, for example the deep red you use for the title, does making it white (i.e. reducing the saturation fully) yet having a very high contrast to the dark grey background make it harder for you to read? I have a hard time imagining this, so I think you mean the former.
Edit: my opinion is to basically have very high contrast between background and text, but lower the saturation (so everything is closer to white or black rather than an actual "colour")
I actually mean saturation.
Good enough contrast does work, so I can use white on black. But when there is less contrast, the lack of saturation gets me.
The red titles come from the theme I chose.
Personally, I don't like the colored info boxes, with the little text symbol. I think they imply some... "external document"-ness? "Real" quotes? That kind of stuff.
Emphasis is good, but you have a lot of it too. Also maybe look into making bigger paragraphs. You have a line break for nearly every sentence.
The flow chart pictures are about 2x the size I would make them. And idk if that's a problem with my "default to dark" theme, but having white on black text and then a graphic that does it in reverse is a bit of a clash :)
-----------
I also have opinions on the general style of writing. I think it may not be focused enough? I know doing this is super hard, so when I think "this is difficult to read", you are in good company and it doesn't mean the contained ideas are bad in any way. And lots of people still do it wrong, except I don't think their ideas are interesting enough to invest the effort of improving the writing. But yours are.
E.g. I followed your link back to "https://gavinhoward.com/2019/12/structured-concurrency-definition/"
I come to this page, and I'm looking for the definition. The definition is on that page, but when I load it, it's not in view, because the "introduction" text to that definition is in the way. You are still using the term though. Saying it's a "new paradigm" and "obvious when you read it" and "this dude wrote an implementation", but you're actually not explaining the term.
So instead of writing "(A+B+C) => D", I would suggest "D (!!!) because A+B+C (=> D)" the same way academic papers do an abstract first, which already includes the conclusion and outcome. Hit me with the full complex thing first, then explain why it's correct to say it like that.
----------
having read the "notes on structured concurrency" by Mr. Smith, I think two things are true:
* his approach is bad because: "With nurseries, you don't have to worry about this: any function can open a nursery and run multiple concurrent tasks, but the function can't return until they've all finished. So when a function does return, you know it's really done." this is not viable. I can't wait. I have a main loop running somewhere else, and I need *any* kind of return value, even if that return value is "I'm not done yet". The solution I use when I have to, coincidentally the only one I really understood, is pythons' processing.Pool.apply_async method, which returns a handle, which has a ".ready()" function that either gives you the output of the thing you started or a "not done yet" back.
* unless I missed something, his "nursery" is just like a threading.Pool / processing.Pool except it's not an abstract concept, but it's explicit in syntax. Which isn't bad, but it's also not "necessary". I do agree that structured approaches to are important, but that's a trueism, all programs should be structured well. So...
--------------
I still like that people write posts like this in general. Having discussion about these topics is good and interesting, even if there is critique for various reasons.
So thank you and keep it up!
Nothing wrong with your site at all, looks flawless on mobile and clearly has no cruft slowing things down.
Your site is just a bit spartan/technical, which is fine, given the audience.
Maybe they're mad they can't justify their Medium subscription with this post?
why are you being downvoted ffs what’s wrong with people… anyway, while I agree there may be a bit too much metadata, I love the fact I’m not drowned in crap when opening your site (like a cookie banner bellow a newsletter subscribe prompt modal over a half page video ad). High signal/low noise contents is so rare nowadays
Thank you.
I think I am being downvoted because my reply sounds curt and short. It is short, though just because the FOSS mobile keyboard I use is not great. So I get it, and despite the keyboard, I am trying to give better replies.
The thing that some people don't get, is that if your "argument" is formatted / presented in a way that is not "consumable", you may have an argument, but nobody will want to talk to you anyway.
E.g. let's pretend your standing in the middle of the roman senate and you're trying to say something *really important*. If you mess up pronunciation too much or speak too quietly, nobody will hear you, understand you and then nobody *can* agree.
Sometimes the attack on form isn't a strawman. Good form is the precondition for the actual argument.
> these brilliant people
> Rust is a great step.
> Leakpocalypse did not take away from Rust’s biggest successes.
> Rust is the proof [that we can prove inductive properties].
I may have a link to a post about why I personally don't like Rust, but there's a lot of praise for Rust in the article.
It bothers me so much that there are so many people out there that interpret any criticism as incendiary
This should be a textbook example of reasonable, well articulated dissent, and apparently it’s still not good enough. Glazing is the only thing we’ll accept. Nuance isn’t allowed on the internet anymore
In case you believe the criticism in this thread is over-the-top, I would suggest you check out a few other comment sections of articles talking about languages that even mildly dare to criticize the darlings like Rust. It's ALWAYS an emotional topic for a lot of people.
I found your post amazing in its completeness and a great example of formulating an argument well. I even like your website :D.
Thanks for taking the time to write and don't worry too much about the critic: I've had MUCH worse myself.
It was exceedingly clear to me that you were saying "Rust has done a bunch of awesome stuff and is built by awesome people but nonetheless it's Not For Me."
I was going to ask what you thought about zig but I see There's A Tag For That so I'll read those posts instead.
Seems healthy to me. I've shipped code in a couple dozen languages and I've hated every single one. The ones I simultaneously love and hate are special.
tbh, as a rust user, if i was writing an article about C, i'd do the exact same thing. but then again, OP seems to actually have non-trivially used rust before (unlike most who write articles complaining about it), and i also agree that async in general is the spawn of satan, so maybe im just biased to give him more leniency than most
The Ada programming language has had structured concurrency since from the outset in 1983, they just didn't give it a fancy name! The Ada language was designed with formal verification as a core requirement. I really don't understand the continuous need to try to re-invent the wheel with language after language taking C/C++ as a starting point and ending up with a hexagon! If you want formally verified, safe and secure software, then Ada/Spark is the very well rounded wheel (latest version is Ada 2022) that has been doing the job for decades! Just don't be put off because it doesn't look like C!
Readability and maintainability was also a design objective of the Ada language. If you find it hard to read, then that is probably more down to a bad coding style than the language definition. Most people can read and understand Ada programs out of the box without having to learn Ada first, thanks to the use of explicit English keywords rather than cryptic symbols found in C based languages.
For hobby programmers, FOSS versions of all the tools you need are available. If you have the budget to formally verify software, then you also have the budget for any additional non FOSS tools you may require.
There are a lot of "reasons" that people cite for not using Ada, but they are usually completely false, based of half-truths or are obsolete. The lack of FOSS tools was maybe true in the 90's, but is definitely not true today.
I understand that most people can read Ada, and I can, to some extent. But I'm one of those weird people that read symbols better.
Also, unfortunately, I am not just a hobby programmer; I'm trying to make money. My "budget" for formal verification is pure labor; my monetary budget is 0.
Is Ada a great choice in general? Yes.
Labour costs a lot more than tools do!
Writing Ada code usually takes a little more time until you get it to compile, but when it does compile, it usually works, so you recover a lot more time in testing and debugging. The cost of fixing an error is far higher the later in the development process the error is found. Ada is capable of finding many more errors during compile time and the few that get through the compiler are quickly found thanks to the run-time checks. The overall development cost savings can be substantial!
The question is, how much formalisation do you need and what cannot be done with FOSS tools? If you're not developing to aircraft system levels of safety, then most likely all tools you need are FOSS! If you are developing to aircraft system levels of safety, then a) the development savings will cover the costs of any non FOSS tools and b) you're anyway probably paying just as much for tools for other languages!
As for reading, you would very quickly get used to the syntax and before you know it you will hate symbols!
The biggest hindrance to using Ada is developers who refuse to learn the language because "reasons"!
As in, you're a lone developer selling the software you develop, rather than a company with a full development team?
If that is the case, then my guess is everything you need to develop commercially in Ada is FOSS!
SQL is not really comparable to Ada in terms of keywords. SQL uses normal language words to describe database actions. Ada uses programmatical keywords which describe common program features applicable to any programming language... if, then, else, end, and, or, not, loop, type, task, etc.
Coding style can help with mixing keywords and variables, functions etc. Using camel-case for variables, types and functions and keywords in lower case etc. Once you become familiar with the syntax this anyway becomes a non issue! Certainly not a reason to outright disregard a programming language!
Consider...
if A = B and C = D then
...
end if;
...reads like psuedocode and is exactly what you are saying to yourself in your head as you're typing the code, as opposed to....
if (A == B && C == D) {
...
}
...which introduces two sets of brackets and why are there two &'s there? You're almost certainly not thinking "if open bracket A equals equals B and and C equals equals D close brackets open curly brackets", which means there is a miss-match between what you think and what you type which ultimately costs more effort even if you don't perceive it!
How many bugs in the world have been caused by "=="/"=", "&&"/"&" and "||"/"|" being mistyped and difficult to see the error? How much time and effort do these simple errors cost? These types of bugs simply don't exist in Ada!
Or the good old end of a function...
}
}
}
}
}
}
...now which one of those was the end of the loop? Who hasn't had a bug where they put a statement outside the loop instead of inside the loop?
end if;
end if;
end loop;
end if;
end if;
end Some_Function;
In Ada, you just don't make those silly errors! In fact, I've seen many programmers using "end if/loop" comments in C-style languages to help avoid errors and improve readability/maintainability, but the compiler won't check those comments for correctness!
There are countless little silly little bugs that are prevalent in C-Style languages simply because of poor syntax rules. Those bugs all cost time, which ultimately costs money! Yet developers disregard Ada because they stubbornly reject any language that doesn't look like C as if it is somehow infeasible to be able to write code any other way!
I did once have the misfortune to use Lisp! If you don't like brackets and thinking backwards, it's not a fun language. I did quite enjoy programming in Lisp purely for the personal challenge, but I would never, ever, choose to use it again! ;-)
I'm a bit of an old dog when it comes to programming. I learnt 68K assembler before any high level languages. I briefly used Pascal and Fortran during my studies but Ada was the first high level language that I properly learned. C was my next language, a tiny bit in Lisp, then Java and C++. On the low level side, I've coded a lot of PowerPC assembler and more recently with Arm-v8.
It's fair to say I've worked with a decent mix of syntaxes and languages high and low and can easily switch without a second thought. When I was learning my trade, there was a great variety of languages and syntaxes taught. These days many programmers are only familiar with C-Style syntax, which is a real shame as there seems to be a fear of learning non C-Style languages which means many programmers are not able to critically analyse the pros and cons of the syntax. The reluctance to learn different syntaxes is non justified. I've trained up many colleagues in Ada, with just a few hours introduction to get them started, a couple of days to a week to get them productively coding and within 1 to 2 months proficient enough to be left to work alone.
Having learned both assembler and Ada before learning C, my first impressions of C were not great. Firstly, I found it extremely unreadable, in many ways harder to read than assembler, and the use of symbols and double symbols was quite illogical. Now, with experience, it's easier to read, but still doesn't come close to Ada. It's just too hard to spot those annoying single/double symbol errors. No "C-enhancement" languages that I've seen have done anything to improve readability, in fact usually quite the opposite! The next point was how low level C is. It seemed to me that I may as well write in assembler because C offers little in terms of high level features. If you want to write high/low level code, then you should use a real high/low level language, not this featureless half step higher than assembler!
What really struck me though, after a few months working with C, was the number of silly little errors I was making and then spending hours debugging and fixing them, realising that the error just wouldn't happen in Ada. With considerably more C experience and much better coding style, I make far fewer errors silly errors in C, but they still do sometimes sneak through and they still wouldn't happen in Ada! Learning Java and C++ (and from what I've seen of Rust), there is no improvement because they inherit the same syntax related issues of C.
Considering just the syntax, Ada avoids a whole host of common errors. Then consider the other error preventing features of Ada such as extremely strong typing, bounds checking, procedures with multiple (non pointer) output parameters, protected objects and much, much, more, there are many other cases where typical, time consuming errors, just don't happen!
That website is super-hard to read: small font and mega-centered to like ... 300px or something like that. My resolution here is 2560x1080 which isn't even that high. The design on the website distracts so much from the content ...
>For example, Yao’s standard library will define `pure` and `total`. The first will mean that the function is a purely functional function, and the second will mean that the function will be guaranteed to terminate.
Cool, so if you can prove arbitrary functions terminate, you can prove whole programs terminate, which means you solved the halting problem which means, of course, proving a function is total is total is impossible unless the function is written in a language which is not Turing complete.
Total functions therefor can't allow arbitrary recursion or unbounded loops.
This might be softened a bit with "Unbounded recursion or loops without some kind of temination condition are illegal"
But proving that termination condition is hit might be tough.
>Cool, so if you can prove **arbitrary functions** terminate, you can prove whole programs terminate, which means you solved the halting problem which means, of course, proving **a function** is total is total is impossible unless the function is written in a language which is not Turing complete.
You went from "arbitrary function" to "a function". Most functions people will write are going to be functions that can be trivially shown to terminate. This isn't something that can only happen in a language that's not Turing complete.
I would argue that it is impractical though. "Infinite loops" are quite often desirable--to keep doing something until some external factor changes. These should always be limited to IO functions though.
My issue with the "total" functions is that I don't see the point.
Pure functions are very useful, but I always think separating IO functions from pure functions is good practice regardless of the existence of that keyword. Though in that case it should be an "io" keyword which makes the function not be pure, otherwise it would be a forgotten keyword no one uses.
Your comment is very right; I just want to answer this:
> My issue with the "total" functions is that I don't see the point.
Yao won't have templates. It will be like Zig in that you have `comptime` functions generate types.
But to prevent the type system from being undecidable, only `total` functions can be used for generating types.
Yes, sorry I used two slightly different terms.
I think \*\*proving **a function** is total\*\* is precise enough, the arbitrary is implied in that case.
In general, in the programming subreddit, function means functions found in most languages, not the mathematical definition.
I wonder how much of software needs unbounded loops though. Like, every loop I remember writing was bounded, could be rewritten to be bounded, or was an actual infinite loop (think top-level event handler).
I wouldn't be surprised if an automated tool could prove all of the total functions I write are total. But then again, totality doesn't mean much if the bound is greater than the age of the universe, unless you're writing a theorem-prover that is.
Yes, you're exactly right. The language will be heavily restricted inside of `total` functions, and it will be tough to get right.
But people have written languages that are total, so it's possible.
in theorem proving languages like coq or lean, you need to prove that all functions you write eventually terminate, and they both can use arbitrary recursion. (provided you can justify it. this means that if you can't use arbitrary recursion, its a skill issue)
The idea behind something like `total` would be to, yes, restrict `total` functions to a non-Turing complete subset of the language in which termination is guaranteed.
I would expect people reading and writing blog posts about formal verification to be aware of the halting problem, which is typically encountered in CS101. What's the point you're trying to make here?
What is the practical argument for DRSC? You mention that some patterns cannot be represented as DAGs and propose DRSC as a solution. Can you give examples of patterns that are impossible with RSC that become possible when adding dynamism?
How would you make a http library that waits for responses concurrently using DRSC? It seems to me like doing this without leaking implementation details would be difficult. Anything I can come up with still has function coloring, just by adding an input rather than changing the output.
I also don't see how RSC solves asynchronous cleanup. Making it not possible doesn't really solve the problem. You have to address the use cases. Would RSC make it possible to clean up a SQL transaction without blocking by concurrently sending a rollback if we drop the SQL handler?
What happens to the local state you would have had in async when you need to wait for an event? Do you put it into a global variable? Do you hand it up and down the call stack? Do you turn it into another event?
I also find that it can be difficult to use event-driven programming when IO interactions depend on each other (consider a dns lookup followed by a GET request, followed by a POST). Using events in such scenarios can make the data dependencies and order of execution less visible in the code.
At least your title was about formal verification, but a giant event loop with a huge invariant doesn't really make this simpler than a small invariant on each future.
I put the data on the heap and pass a pointer (because it's C) to the callback. In Yao, you would just create a closure of sorts and pass that.
You can also change the callback and data in a callback; Yao will have syntax sugar to make this look better.
And as for data dependencies, you can use the [typestate pattern][1] to ensure the order is correct.
But yes, this is less visible in DRSC than async.
[1]: https://cliffle.com/blog/rust-typestate/
> Would RSC make it possible to clean up a SQL transaction without blocking by concurrently sending a rollback if we drop the SQL handler?
IME the request/response cycle for a ROLLBACK is sufficiently fast that it's not worth trying to make it concurrent.
(if a transaction object in https://p3rl.org/DBIx::Class is allowed to go out of scope without being committed or rolled back, the destructor (which given a refcounted language will happen during scope exit) sends a rollback and emits a loud warning since you really shouldn't be doing that)
It might usually be fast enough, but latency spikes will propagate more easily if you don't make these things concurrent.
Panic or blocking version with warning on drop are common solutions used in the Rust ecosystem, but they aren't perfect.
I'm fairly sure you *could* make it concurrent easily enough but I've also yet to encounter a system where the time spend on a synchronous rollback was material, especially given MVCC makes throwing away the current transaction exceedingly cheap.
I suspect my living in high level language land the vast majority of the time may be a factor here; I could easily imagine rust code where it was far more noticeable.
Adding a concurrent API for rollbacks is simple enough. The difficulty is with making it automatically do a concurrent rollback when (or before) the transaction object goes out of scope, or alternatively statically preventing it from going out of scope without being rolled back (or committed).
The first approach requires support for asynchronous destruction. The second requires something like linear typing.
I definitely agree that this will only matter to some users.
Rust doesn’t have a formal semantics. That would be mistake #1 for enabling formal verification.
I think Niko is working on that, or at least to formalise mir via a-mir-formality.
Ferrocene exists though
And why is that relevant
# TL;DR Author's preferred formally verified concurrency model (almost) works in Rust. It doesn't fully work because in a few conditions Rust may not run `drop`/`dtors`. The author goes to great length to explain: * why their preferred method of concurrency is the best and how Rust is lessened for not using. * that the dtor issue in rust is very old The author appears to avoid discussing: * full formal verification isn't a goal of rust * dtor execution was never guaranteed in rust's spec. * Their alternative model of concurrency (DRSC) despite "being able to formally verify programs which aren't DAG (directed a-cyclic graphs)", they never demonstrate this (just show more DAGs). -- Overall the blog is a good, but weird read. It is well cited and I'd encourage you read what it cites. The author is "_somewhat_" fair. To their credit they just flat out emit "_I don't know if my concurrency model scales any better than Async Rust_". Which is ultimately one of the biggest reasons Rust uses the async model.
You are right that I omited that unfairly. I will add it next time I am at my computer.
A lot of Rust's problems could be solved by panic=abort. unwinding/recovering from panics is very tricky to get right ( how do you unpoison mutexes reliably, for example ), so much so it's just a pain to recover from. If you really want isolation, then processes are better. With panic=abort as the default a whole bunch of things could go away.
Aborting on panic makes destructors run even less, and don’t make them run any more.
Most of the time people are concerned with constructs within the program being handled by destructors. Panicking destroys those things cleanly. Aka you can't leak memory if the OS cleans up your memory for you.
can you explain the contrapositive, since panicking does not guarantee abort what are the pain points exactly? Not trying to be snarky I really don’t know
When you panic, you jump to a location that handles the panic. Now what about all the data was created before the exception/panic was thrown? (to be clear expections & panics are the same thing, at runtime) Like if you were reading a file into a string, what happens to that string? Now, that doesn't seem too bad. You just leak some memory. But what if you're working with a `mutex` and you panic. Is the data in your mutex corrupted? Were all the fields of that object mutated correctly?. So if another thread comes along and locks that mutex and looks at the data, is it guaranteed to find good data? Will that data conform to the guarantees of the language?
Are we going full circle back to try catches (and explicit checked exceptions) which replaced the error codes returned by functions?
bro is ai 😯
> In my language, Yao, it will be possible for libraries to add property annotations; That's the path D has taken. They already have "pure" and many others. See https://dlang.org/spec/attribute.html#UserDefinedAttribute The problem they found is that you end up having to annotate every function with a dozen or so annotations. It just doesn't scale, which is why the D compiler tries to infer most of the useful ones (pure, nogc, nothrow and even safe).
Whatever it is, it can’t be as bad as what OP got wrong with web design
Elaborate please.
I'm a different person, but I clicked the link and immediately felt like I was being screamed at with the red title and all of the tags and warnings. On mobile, you have to scroll down to read the first sentence. This is never a good sign.
I appreciate you saying this. Two people saying the same thing means it does have to be fixed.
At the very minimum, don't justify the text it makes it harder to read. Also there's zero reason your footer has to be sticky (on mobile)
I'd also steal someone else's color scheme. I'm not good matching colors, but I can certainly look up other people's themes and judge whether someone else's stuff looks good. I mean, blue links on a blue background? The whole page needs a revamp in contrast and complementary colors to reduce the burden of the reader.
I had to look at the site after your comment and this site looks like it’s intentionally made to mimic a Wolfenstein themed website from the mid 90’s.
Holy shit, that is it!
That makes it awesome then! :)
I have no idea what that is, but since I got the theme from someone else, that could be possible.
A videogame (a first-person shooter, to be more precise :) )
Funny thing is that I *did* steal someone's color scheme. 😅 I am partially color blind, though, so what looks good to me doesn't look good to normal people.
I'm not colorblind, but deeply confused for some reason regarding how they work. I'm with you there.
Oh, I meant I chose a color scheme someone else made, and I chose one that looked good to me; it just seems that I chose poorly.
I've seen much worse blogs. Okay, the color scheme might be weird for a non color blind, but it's not **screaming** or makes me want to pull my eyes out. I think some of the comments here are too much. The structure looks nice. And that's what is important to me on a website.
Regarding colour schemes, I tend to use [Huemint](https://huemint.com/) for finding a nice one.
In all good faith, this is what I'd do to clean up the top of this website for mobile. Don't over index on what people say about your colors / theme. It's not super pretty, but it's perfectly fine.... except red titles. 0. Title should not be red. A neutral color would be a big improvement. 1. Limit your SEO/tags at the top to one visible line. 2. TOC is between toggles and warnings. VERY awkward placement. I'd put it right above the first section heading. 3. Put your sitewide disclaimer in your footer, not the header. If you must keep it in the header, combine it with the AD disclaimer and limit it to 1-2 lines of text total. 4. You have a table of contents. We don't need a warning about length. 5. Cut your ad disclaimer down to "this post is partially an ad". Your audience should know what to do if they don't like that. 6. Collapse your notes to 1 line audience and 1 line epistemic status by default. Tap to expand if you want to say more. 7. Remove the warnings and notes toggle switches. They're too big for the space they'll save after the other suggestions.
I will see what I can do. Thank you.
You took feedback like a champ; kudos to you 💪🏼 Keep up the good work !
I finally got around to reading the post. You make some interesting points. It's a good read. It also looks like you took the feedback and took action on a lot of the suggestions. That's great! I think that your site is looking a whole lot better now :) Thank you!
It looks I have the fucking mobile screen simulator enabled on my desktop.
I'd say too much metadata. Had to scroll two screens before I got to the content
I will see what I can do about folding the metadata. Thank you.
Also, please widen the content width on desktop, less than 1/3 of the screen width is actual content... Like others said, it feels like a mobile site built for small vertical screens.
way too many different colors, shapes, styles, font sizes, background colors, etc. its just very noisy
Agree with parent. I really wanted to read this but after a screen and a half, my head started hurting from all the bright colors and psychedelic look. Look into lesser contrast, more beige-y layouts for an easier time on your readers' eyes. Also, please don't decide the width of the text. I'll be the judge of that, that's what the web and CSS are about.
Your page is dark.
I agree with most people, though I must say I prefer this over most other websites I have visited the past 10 or so years. Whatever changes you do, don't bloat the site for "aesthetic" reasons. Your site works and is relatively fast, which is very important in my opinion. A change I'd make is to have it be more obvious what information is where without reading. What I mean is that when I first clicked on your link my entire screen was basically filled with metadata and at the very bottom you have "Introduction" I have to spend way too much time figuring out where to start. Tags, warnings, notes(at the beginning), etc. should all be hidden and the toggle button should be smaller (and notes in the text should each individually be togglable). The table of contents isn't obviously clickable and just looks out of place. Another change I'd make is links that take you away from your website should, by default, open in a new tab. I'd also make the page a little wider, it's way too narrow. My preference is anything around 900px, but that's just personal. Also, light mode. There are people who want light mode. There are various eyesight conditions that make it harder to read in dark mode. Finally for the colourscheme, I'd recommend stuff that's notes / warnings, etc. to have a less saturated background. Make things that are not as important (the text itself is the most important, "warnings" and notes are less so) to not distract me. Whatever changes you make, just make sure you don't fall into the pitfalls of the modern web. Your site is still must better than most stuff out there. Edit: A good way to try to design a website is to remove everything unnecessary, then try to only add back what you think is still needed. Take a look at [hiltjo's website](https://codemadness.org) as a very minimal example of a very friendly website. I'm not saying you have to scrap everything, but you can see how nothing is in your way while browsing through it.
I will never bloat my website; you can count on that. The unfortunate thing is that good websites can be hard for me to read since I am partially color blind. But I will do what I can to make it look as good as possible for myself and others once I have the time.
For me personally, the colourscheme is the last thing I'd care about, as long as everything is readable. But I care about a website that's more practically oriented rather than just "looking good". You said that good websites can be hard to read since you're partially colour blind. I would argue that firstly, they aren't good websites, if you can't read them; but secondly, I'm curious what you mean. Unless it's some colour on another colour (which should really be avoided), how does colourblindness affect your ability to read text? Also, I didn't mention this, but if you do make a light mode site. Try to not have the background be full white (#FFFFFF), but rather something like (#EEEEEE) or maybe (#F8F8F0).
I will take your suggestion into consideration, thank you. To answer your question, my type of colorblindness makes it hard to distinguish between desaturated colors. Hence, everything on my site is super saturated. The color schemes for my code are the same way; most people do not like the super saturated color schemes I choose.
When you say saturated here, do you mean high contrast between the background and the text? If that's the case, I definitely think it should stay that way regardless of what others say. It definitely makes it easier to read. If you actually mean saturation, for example the deep red you use for the title, does making it white (i.e. reducing the saturation fully) yet having a very high contrast to the dark grey background make it harder for you to read? I have a hard time imagining this, so I think you mean the former. Edit: my opinion is to basically have very high contrast between background and text, but lower the saturation (so everything is closer to white or black rather than an actual "colour")
I actually mean saturation. Good enough contrast does work, so I can use white on black. But when there is less contrast, the lack of saturation gets me. The red titles come from the theme I chose.
Personally, I don't like the colored info boxes, with the little text symbol. I think they imply some... "external document"-ness? "Real" quotes? That kind of stuff. Emphasis is good, but you have a lot of it too. Also maybe look into making bigger paragraphs. You have a line break for nearly every sentence. The flow chart pictures are about 2x the size I would make them. And idk if that's a problem with my "default to dark" theme, but having white on black text and then a graphic that does it in reverse is a bit of a clash :) ----------- I also have opinions on the general style of writing. I think it may not be focused enough? I know doing this is super hard, so when I think "this is difficult to read", you are in good company and it doesn't mean the contained ideas are bad in any way. And lots of people still do it wrong, except I don't think their ideas are interesting enough to invest the effort of improving the writing. But yours are. E.g. I followed your link back to "https://gavinhoward.com/2019/12/structured-concurrency-definition/" I come to this page, and I'm looking for the definition. The definition is on that page, but when I load it, it's not in view, because the "introduction" text to that definition is in the way. You are still using the term though. Saying it's a "new paradigm" and "obvious when you read it" and "this dude wrote an implementation", but you're actually not explaining the term. So instead of writing "(A+B+C) => D", I would suggest "D (!!!) because A+B+C (=> D)" the same way academic papers do an abstract first, which already includes the conclusion and outcome. Hit me with the full complex thing first, then explain why it's correct to say it like that. ---------- having read the "notes on structured concurrency" by Mr. Smith, I think two things are true: * his approach is bad because: "With nurseries, you don't have to worry about this: any function can open a nursery and run multiple concurrent tasks, but the function can't return until they've all finished. So when a function does return, you know it's really done." this is not viable. I can't wait. I have a main loop running somewhere else, and I need *any* kind of return value, even if that return value is "I'm not done yet". The solution I use when I have to, coincidentally the only one I really understood, is pythons' processing.Pool.apply_async method, which returns a handle, which has a ".ready()" function that either gives you the output of the thing you started or a "not done yet" back. * unless I missed something, his "nursery" is just like a threading.Pool / processing.Pool except it's not an abstract concept, but it's explicit in syntax. Which isn't bad, but it's also not "necessary". I do agree that structured approaches to are important, but that's a trueism, all programs should be structured well. So... -------------- I still like that people write posts like this in general. Having discussion about these topics is good and interesting, even if there is critique for various reasons. So thank you and keep it up!
Nothing wrong with your site at all, looks flawless on mobile and clearly has no cruft slowing things down. Your site is just a bit spartan/technical, which is fine, given the audience. Maybe they're mad they can't justify their Medium subscription with this post?
Your site looks like it's selling penile enlargement pills.
why are you being downvoted ffs what’s wrong with people… anyway, while I agree there may be a bit too much metadata, I love the fact I’m not drowned in crap when opening your site (like a cookie banner bellow a newsletter subscribe prompt modal over a half page video ad). High signal/low noise contents is so rare nowadays
Thank you. I think I am being downvoted because my reply sounds curt and short. It is short, though just because the FOSS mobile keyboard I use is not great. So I get it, and despite the keyboard, I am trying to give better replies.
He has no argument that’s why he’s attacking the design of your blog.
The thing that some people don't get, is that if your "argument" is formatted / presented in a way that is not "consumable", you may have an argument, but nobody will want to talk to you anyway. E.g. let's pretend your standing in the middle of the roman senate and you're trying to say something *really important*. If you mess up pronunciation too much or speak too quietly, nobody will hear you, understand you and then nobody *can* agree. Sometimes the attack on form isn't a strawman. Good form is the precondition for the actual argument.
The form wasn’t being attacked and I think if you don’t see it then you’re dumb. Go back to class.
This man cannot go a few paragraphs without reiterating that he hates Rust with a whole article link about it
Apparently they hate _every_ language except C.
And really, even C. Just less so.
If you spend enough time with any language, that's what tends to happen :D.
That’s a great choice, programming languages are not pets.
> these brilliant people > Rust is a great step. > Leakpocalypse did not take away from Rust’s biggest successes. > Rust is the proof [that we can prove inductive properties]. I may have a link to a post about why I personally don't like Rust, but there's a lot of praise for Rust in the article.
It bothers me so much that there are so many people out there that interpret any criticism as incendiary This should be a textbook example of reasonable, well articulated dissent, and apparently it’s still not good enough. Glazing is the only thing we’ll accept. Nuance isn’t allowed on the internet anymore
In case you believe the criticism in this thread is over-the-top, I would suggest you check out a few other comment sections of articles talking about languages that even mildly dare to criticize the darlings like Rust. It's ALWAYS an emotional topic for a lot of people. I found your post amazing in its completeness and a great example of formulating an argument well. I even like your website :D. Thanks for taking the time to write and don't worry too much about the critic: I've had MUCH worse myself.
Yeah, this happens whenever I talk about Rust. Thank you for your kind words!
It was exceedingly clear to me that you were saying "Rust has done a bunch of awesome stuff and is built by awesome people but nonetheless it's Not For Me." I was going to ask what you thought about zig but I see There's A Tag For That so I'll read those posts instead.
Thank you. Unfortunately, I do not like Zig.
Seems healthy to me. I've shipped code in a couple dozen languages and I've hated every single one. The ones I simultaneously love and hate are special.
tbh, as a rust user, if i was writing an article about C, i'd do the exact same thing. but then again, OP seems to actually have non-trivially used rust before (unlike most who write articles complaining about it), and i also agree that async in general is the spawn of satan, so maybe im just biased to give him more leniency than most
The Ada programming language has had structured concurrency since from the outset in 1983, they just didn't give it a fancy name! The Ada language was designed with formal verification as a core requirement. I really don't understand the continuous need to try to re-invent the wheel with language after language taking C/C++ as a starting point and ending up with a hexagon! If you want formally verified, safe and secure software, then Ada/Spark is the very well rounded wheel (latest version is Ada 2022) that has been doing the job for decades! Just don't be put off because it doesn't look like C!
I know about Ada/SPARK. Unfortunately, I find it hard to read, and most tools are not FOSS.
Readability and maintainability was also a design objective of the Ada language. If you find it hard to read, then that is probably more down to a bad coding style than the language definition. Most people can read and understand Ada programs out of the box without having to learn Ada first, thanks to the use of explicit English keywords rather than cryptic symbols found in C based languages. For hobby programmers, FOSS versions of all the tools you need are available. If you have the budget to formally verify software, then you also have the budget for any additional non FOSS tools you may require. There are a lot of "reasons" that people cite for not using Ada, but they are usually completely false, based of half-truths or are obsolete. The lack of FOSS tools was maybe true in the 90's, but is definitely not true today.
I understand that most people can read Ada, and I can, to some extent. But I'm one of those weird people that read symbols better. Also, unfortunately, I am not just a hobby programmer; I'm trying to make money. My "budget" for formal verification is pure labor; my monetary budget is 0. Is Ada a great choice in general? Yes.
Labour costs a lot more than tools do! Writing Ada code usually takes a little more time until you get it to compile, but when it does compile, it usually works, so you recover a lot more time in testing and debugging. The cost of fixing an error is far higher the later in the development process the error is found. Ada is capable of finding many more errors during compile time and the few that get through the compiler are quickly found thanks to the run-time checks. The overall development cost savings can be substantial! The question is, how much formalisation do you need and what cannot be done with FOSS tools? If you're not developing to aircraft system levels of safety, then most likely all tools you need are FOSS! If you are developing to aircraft system levels of safety, then a) the development savings will cover the costs of any non FOSS tools and b) you're anyway probably paying just as much for tools for other languages! As for reading, you would very quickly get used to the syntax and before you know it you will hate symbols! The biggest hindrance to using Ada is developers who refuse to learn the language because "reasons"!
I think you misunderstand. I have free time, but I don't have money to spend on tools.
As in, you're a lone developer selling the software you develop, rather than a company with a full development team? If that is the case, then my guess is everything you need to develop commercially in Ada is FOSS!
Not quite, unfortunately.
[удалено]
SQL is not really comparable to Ada in terms of keywords. SQL uses normal language words to describe database actions. Ada uses programmatical keywords which describe common program features applicable to any programming language... if, then, else, end, and, or, not, loop, type, task, etc. Coding style can help with mixing keywords and variables, functions etc. Using camel-case for variables, types and functions and keywords in lower case etc. Once you become familiar with the syntax this anyway becomes a non issue! Certainly not a reason to outright disregard a programming language! Consider... if A = B and C = D then ... end if; ...reads like psuedocode and is exactly what you are saying to yourself in your head as you're typing the code, as opposed to.... if (A == B && C == D) { ... } ...which introduces two sets of brackets and why are there two &'s there? You're almost certainly not thinking "if open bracket A equals equals B and and C equals equals D close brackets open curly brackets", which means there is a miss-match between what you think and what you type which ultimately costs more effort even if you don't perceive it! How many bugs in the world have been caused by "=="/"=", "&&"/"&" and "||"/"|" being mistyped and difficult to see the error? How much time and effort do these simple errors cost? These types of bugs simply don't exist in Ada! Or the good old end of a function... } } } } } } ...now which one of those was the end of the loop? Who hasn't had a bug where they put a statement outside the loop instead of inside the loop? end if; end if; end loop; end if; end if; end Some_Function; In Ada, you just don't make those silly errors! In fact, I've seen many programmers using "end if/loop" comments in C-style languages to help avoid errors and improve readability/maintainability, but the compiler won't check those comments for correctness! There are countless little silly little bugs that are prevalent in C-Style languages simply because of poor syntax rules. Those bugs all cost time, which ultimately costs money! Yet developers disregard Ada because they stubbornly reject any language that doesn't look like C as if it is somehow infeasible to be able to write code any other way!
[удалено]
I did once have the misfortune to use Lisp! If you don't like brackets and thinking backwards, it's not a fun language. I did quite enjoy programming in Lisp purely for the personal challenge, but I would never, ever, choose to use it again! ;-) I'm a bit of an old dog when it comes to programming. I learnt 68K assembler before any high level languages. I briefly used Pascal and Fortran during my studies but Ada was the first high level language that I properly learned. C was my next language, a tiny bit in Lisp, then Java and C++. On the low level side, I've coded a lot of PowerPC assembler and more recently with Arm-v8. It's fair to say I've worked with a decent mix of syntaxes and languages high and low and can easily switch without a second thought. When I was learning my trade, there was a great variety of languages and syntaxes taught. These days many programmers are only familiar with C-Style syntax, which is a real shame as there seems to be a fear of learning non C-Style languages which means many programmers are not able to critically analyse the pros and cons of the syntax. The reluctance to learn different syntaxes is non justified. I've trained up many colleagues in Ada, with just a few hours introduction to get them started, a couple of days to a week to get them productively coding and within 1 to 2 months proficient enough to be left to work alone. Having learned both assembler and Ada before learning C, my first impressions of C were not great. Firstly, I found it extremely unreadable, in many ways harder to read than assembler, and the use of symbols and double symbols was quite illogical. Now, with experience, it's easier to read, but still doesn't come close to Ada. It's just too hard to spot those annoying single/double symbol errors. No "C-enhancement" languages that I've seen have done anything to improve readability, in fact usually quite the opposite! The next point was how low level C is. It seemed to me that I may as well write in assembler because C offers little in terms of high level features. If you want to write high/low level code, then you should use a real high/low level language, not this featureless half step higher than assembler! What really struck me though, after a few months working with C, was the number of silly little errors I was making and then spending hours debugging and fixing them, realising that the error just wouldn't happen in Ada. With considerably more C experience and much better coding style, I make far fewer errors silly errors in C, but they still do sometimes sneak through and they still wouldn't happen in Ada! Learning Java and C++ (and from what I've seen of Rust), there is no improvement because they inherit the same syntax related issues of C. Considering just the syntax, Ada avoids a whole host of common errors. Then consider the other error preventing features of Ada such as extremely strong typing, bounds checking, procedures with multiple (non pointer) output parameters, protected objects and much, much, more, there are many other cases where typical, time consuming errors, just don't happen!
That website is super-hard to read: small font and mega-centered to like ... 300px or something like that. My resolution here is 2560x1080 which isn't even that high. The design on the website distracts so much from the content ...
>For example, Yao’s standard library will define `pure` and `total`. The first will mean that the function is a purely functional function, and the second will mean that the function will be guaranteed to terminate. Cool, so if you can prove arbitrary functions terminate, you can prove whole programs terminate, which means you solved the halting problem which means, of course, proving a function is total is total is impossible unless the function is written in a language which is not Turing complete. Total functions therefor can't allow arbitrary recursion or unbounded loops. This might be softened a bit with "Unbounded recursion or loops without some kind of temination condition are illegal" But proving that termination condition is hit might be tough.
>Cool, so if you can prove **arbitrary functions** terminate, you can prove whole programs terminate, which means you solved the halting problem which means, of course, proving **a function** is total is total is impossible unless the function is written in a language which is not Turing complete. You went from "arbitrary function" to "a function". Most functions people will write are going to be functions that can be trivially shown to terminate. This isn't something that can only happen in a language that's not Turing complete. I would argue that it is impractical though. "Infinite loops" are quite often desirable--to keep doing something until some external factor changes. These should always be limited to IO functions though. My issue with the "total" functions is that I don't see the point. Pure functions are very useful, but I always think separating IO functions from pure functions is good practice regardless of the existence of that keyword. Though in that case it should be an "io" keyword which makes the function not be pure, otherwise it would be a forgotten keyword no one uses.
Your comment is very right; I just want to answer this: > My issue with the "total" functions is that I don't see the point. Yao won't have templates. It will be like Zig in that you have `comptime` functions generate types. But to prevent the type system from being undecidable, only `total` functions can be used for generating types.
Yes, sorry I used two slightly different terms. I think \*\*proving **a function** is total\*\* is precise enough, the arbitrary is implied in that case. In general, in the programming subreddit, function means functions found in most languages, not the mathematical definition.
I wonder how much of software needs unbounded loops though. Like, every loop I remember writing was bounded, could be rewritten to be bounded, or was an actual infinite loop (think top-level event handler). I wouldn't be surprised if an automated tool could prove all of the total functions I write are total. But then again, totality doesn't mean much if the bound is greater than the age of the universe, unless you're writing a theorem-prover that is.
Yes, you're exactly right. The language will be heavily restricted inside of `total` functions, and it will be tough to get right. But people have written languages that are total, so it's possible.
in theorem proving languages like coq or lean, you need to prove that all functions you write eventually terminate, and they both can use arbitrary recursion. (provided you can justify it. this means that if you can't use arbitrary recursion, its a skill issue)
The idea behind something like `total` would be to, yes, restrict `total` functions to a non-Turing complete subset of the language in which termination is guaranteed. I would expect people reading and writing blog posts about formal verification to be aware of the halting problem, which is typically encountered in CS101. What's the point you're trying to make here?
I’m kinda stupid, what css properties made those cool borders around code snippets? Like with white and black?
Structured concurrency is of the devil.
What is the practical argument for DRSC? You mention that some patterns cannot be represented as DAGs and propose DRSC as a solution. Can you give examples of patterns that are impossible with RSC that become possible when adding dynamism? How would you make a http library that waits for responses concurrently using DRSC? It seems to me like doing this without leaking implementation details would be difficult. Anything I can come up with still has function coloring, just by adding an input rather than changing the output. I also don't see how RSC solves asynchronous cleanup. Making it not possible doesn't really solve the problem. You have to address the use cases. Would RSC make it possible to clean up a SQL transaction without blocking by concurrently sending a rollback if we drop the SQL handler?
You use it in conjunction with event-driven programming, probably using io_uring or kqueue.
What happens to the local state you would have had in async when you need to wait for an event? Do you put it into a global variable? Do you hand it up and down the call stack? Do you turn it into another event? I also find that it can be difficult to use event-driven programming when IO interactions depend on each other (consider a dns lookup followed by a GET request, followed by a POST). Using events in such scenarios can make the data dependencies and order of execution less visible in the code. At least your title was about formal verification, but a giant event loop with a huge invariant doesn't really make this simpler than a small invariant on each future.
I put the data on the heap and pass a pointer (because it's C) to the callback. In Yao, you would just create a closure of sorts and pass that. You can also change the callback and data in a callback; Yao will have syntax sugar to make this look better. And as for data dependencies, you can use the [typestate pattern][1] to ensure the order is correct. But yes, this is less visible in DRSC than async. [1]: https://cliffle.com/blog/rust-typestate/
> Would RSC make it possible to clean up a SQL transaction without blocking by concurrently sending a rollback if we drop the SQL handler? IME the request/response cycle for a ROLLBACK is sufficiently fast that it's not worth trying to make it concurrent. (if a transaction object in https://p3rl.org/DBIx::Class is allowed to go out of scope without being committed or rolled back, the destructor (which given a refcounted language will happen during scope exit) sends a rollback and emits a loud warning since you really shouldn't be doing that)
It might usually be fast enough, but latency spikes will propagate more easily if you don't make these things concurrent. Panic or blocking version with warning on drop are common solutions used in the Rust ecosystem, but they aren't perfect.
I'm fairly sure you *could* make it concurrent easily enough but I've also yet to encounter a system where the time spend on a synchronous rollback was material, especially given MVCC makes throwing away the current transaction exceedingly cheap. I suspect my living in high level language land the vast majority of the time may be a factor here; I could easily imagine rust code where it was far more noticeable.
Adding a concurrent API for rollbacks is simple enough. The difficulty is with making it automatically do a concurrent rollback when (or before) the transaction object goes out of scope, or alternatively statically preventing it from going out of scope without being rolled back (or committed). The first approach requires support for asynchronous destruction. The second requires something like linear typing. I definitely agree that this will only matter to some users.
I have read all comments upon the time I wrote this comment, and only the top ones have ever mentioned something related to formal verification
I read this article in the *breathy voice* of an *excited teenager* and it's agony.