roca

Doesn't work if they just paste scanned documents into a multi-modal model, unfortunately.

All I do all day is output byte sequences into a terminal. Therefore I am harmless.

Your focus on "the most cost effective way" is fine in principle but in practice, we don't know ahead of time what bugs exist and what their impact is. Experience has shown that the prevalence and impact of memory safety and data race bugs is very difficult to predict, and the impact has very high variance. There are so many examples of memory safety bugs and races that lie dormant for years and suddenly become very important (e.g. because someone malicious discovered them, or because the software started being used in a different context).

Note that these safety bugs are really different from most other kinds of bugs in that their potential impact is unbounded: they can cause the program to behave in arbitrary ways. Logic errors, even stuff like non-UB integer overflow, have impact that is still constrained by the expected semantics of the programming language.

Given that uncertainty, it makes sense to take precautions. If you have cheap tools to eliminate those bugs, do it just in case. That might even be cheaper than trying to figure out ahead of time how important those bugs are going to be over the lifetime of the software (which is often an impossible task anyway).

> If the gap is 10 orders of magnitude, narrowing it by 1 doesn't have a big impact, unless it were completely free, which it isn't.

It doesn't need to be completely free to have a positive net benefit.

Ah, you seem to think I proposed using formal verification to eliminate 100% of memory safety bugs no matter what the cost. In fact I didn't say that, and I don't recommend that. There will certainly be cases, typically in very large libraries that use 'unsafe', where the invariants you have to prove are very complicated and fragile and difficult to verify, and therefore the cost outweighs the benefit.

What I'm looking forward to is formalisms and tools to pick the "low hanging fruit" --- as I said, verifying the correctness of small libraries that use 'unsafe'. In small libraries, in general, and invariants and proofs are smaller and proof automation is correspondingly more effective.

As a practitioner but also a small-time CS researcher, I don't expect verifying that small Rust libraries use 'unsafe' correctly will "waste my assurance budget".

On the cost side: we don't know yet how hard it will be to formally verify small Rust libraries that wrap unsafe code in safe abstractions. That's partly because we don't even know exactly what the specification is that unsafe Rust code has to satisfy. But once we've settled on that and built good proof assistant tools, I think the work will usually be pretty easy, because most of these libraries are fundamentally quite simple and small, even including all their dependencies.

You correctly identified compositionality as a key issue. Fortunately, verifying correct use of 'unsafe' is inherently compositional: knowing nothing but the code of the library and its dependencies, we must prove that the necessary safety properties hold in all possible contexts.

On the benefit side: proving that libraries do not undermine Rust's safety guarantees is important, and the importance grows with the popularity of the library. And of course those guarantees aren't just "memory safety" but data-race-freedom and the general "mutable-xor-shared" property --- the importance of which is the subject of the OP here!

Indeed, we don't have that model, and we definitely need it. I don't think it's intractable. We've made a lot of progress. I would like to see more focused effort on this particular problem from the academic community.

In six years I wrote a lot of the 200K lines of Rust for Pernosco --- a fairly sophisticated application server for a SaaS debugger. There are 40 instances of the string 'Arc::new(Mutex::new('. A lot of them are shared caches and other innocuous things. There are 22 occurrences of 'RefCell::new('. There are other uses of Arc, and other uses of Mutex, but fundamentally the system has not collapsed into an arbitrary graph of mutable data.

Of course, one's mileage can vary. Most of our system is designed to be stateless at the top level, which helps.

I think it's reasonable to look forward to verifying that small Rust libraries use 'unsafe' correctly. That alone would be really helpful.

In practice, those "undefined flags" are set consistently. In Pernosco we move rr recordings across architectures quite often and those flags have never been a problem.

I remember my wife working remotely and Source "Safe" corrupting the repo when the modem dropped while she was committing her work. Good old days.

Disclosure: I'm a former agnostic, now Christian.

A person could have a well-founded belief in God without seeing him as Abraham did. What if someone in the early church had seen apostolic miracles and talked to an eyewitness of the resurrected Jesus? Would it still be a "leap of faith" for them to believe in God and his promises? I would say not. So I don't think verse 6 "requires some kind of leap of faith" in the sense you're using it.

I think such a person would still need faith, per verse 6, to put their justified belief into action in critical moments, e.g. at a moment when they're facing persecution for following Jesus.

Now, how much of a "leap of faith" is required given the evidence really available to believers then and now... that's the big question about which we presumably disagree.

> none of which did what they did or believed the way they do because of anything describable as what would count as evidence in science, or a court of law.

Abraham is in that list, and is elsewhere described as the paragon of faith. Yet in Genesis 18/19 Abraham is said to have met and talked with God, and discussed the destruction of Sodom, which Abraham then witnessed immediately. Abraham's faith was not a belief in a God he had never seen.

Likewise Cain, Abel and Noah are in the Hebrews 11 list but Genesis says they spoke with God before they exercised their faith.

In Hebrews 11 the "things unseen" are elaborated as the creation of the universe and the future fulfillment of God's promises (almost entirely the latter). They're unseen not because there is no evidence for them, but simply because the faithful people did not live to see them fulfilled.

"Faith is belief without evidence" is a trope widely believed by Christians and atheists, but that's not the faith being promoted in Hebrews.

Doesn't cite TimesFM for some reason. Maybe the latter was published after this paper went camera-ready? https://blog.research.google/2024/02/a-decoder-only-foundati...

Microsoft's TTD handles multiple threads on multiple cores, because they instrument reads. But that's high overhead.

I'd like to know more about what the embedded tools do. I see SourcePoint supports multicore x86, but the data volume looks high so I suspect they can't handle workloads that run for minutes or hours. Also it's not clear to me which of these tools can reproduce the state of memory at every point in the past.

Basically I don't think you can do low-overhead record and replay without hardware support like Intel's QuickRec project. "Capture all memory traffic" is not going to scale.

My favourite novel.

There's a clear difference between "omniscient" debugging and "time travel" debugging. The latter almost always refers to debuggers that let you move backwards in time but only let you access state at the "current point in time", and moving forward or backward has a noticeable cost. Omniscient debuggers (e.g. Pernosco or Lewis' work) give you approximately instant access to states at different points in time.

rr and Undo are about the same here: they support multiple threads but run all threads on a single core.

Surely it's "vias ferrata".

Maybe. But I'm wary of the argument "we need to lean into the existential threat of AI because of those other existential threats over there that haven't arrived yet but definitely will".

It all depends on what exactly you mean by those other threats, of course. I'm a natural pessimist and I see threats everywhere, but I've also learned I can overestimate them. I've been worried about nuclear proliferation for the last 40 years, and I'm more worried about it than ever, but we haven't had another nuclear war yet.

I wonder if AI is going to change the equation here --- by making it much cheaper to run spam campaigns against thousands of different small forums.

We live in a golden age. Worldwide poverty is at historic lows. Billions of people don't have to worry about where their next meal is coming from or whether they'll have a roof over their head. Billions of people have access to more knowledge and entertainment options than anyone had 100 years ago.

This is not the time to risk it all.

We will soon find that story generation is easily automated.

Your version of history entirely ignores the fact that Russia recently grabbed Donbas and then Crimea.

> NATO (the US) is using Ukraine to fight Russia to the last Ukrainian

So you believe that most Ukrainians actually want to surrender to Russia?

TeX/LaTeX don't compete on performance and don't handle dynamic document updates. Browser text layout is a much harder problem.

Got a reference for that?

To be clear: I've never heard of any such thing. I happen to work for Google, but I'm open the possibility that this happened and I didn't hear about it.

Also, this is a great example of a recurring problem: successful organisations venerate their culture, so that every part of it is assumed to be essential to their success until very painful experiences prove otherwise.

Another example: Linux developers thinking that managing patches by email is the best approach ever, because Linux is dominant.

This was a terrible way to run a company then and now. It leads to an incoherent product strategy. It doesn't provide the persistence required to pursue strategies that take many years to eventuate. Google succeeded in spite of this culture, not because of it; they found an immensely profitable niche, which enabled them to hire huge amounts of incredible talent, which covered up their cultural problems.

[Disclaimer: I work at Google.]

There are a lot of high profile Rust adoption stories where the developers involved are C and C++ experts. E.g. Rust in the Linux kernel, Rust in the Windows kernel, Rust in Firefox, Rust in Android.