Hi, I (Shuxian) worked with Michael on this project. Happy to answer any questions!
We'll also post a followup next week on formally verifying our unsafe primitives in the style of RustBelt (https://plv.mpi-sws.org/rustbelt), if that interests you.
Wow, I wouldn't have thought that it would be possible to do this (at least, not ergonomically, although now that you mention it I guess I don't see why not). That would be amazing to see.
Combining single-threaded C++ with multi-threaded languages has been a thing for quite some time.
Thanks for the interest; I've never had a post on Hacker News before.
I'm happy to answer any questions.