14 Oct 2026

feedPlanet Mozilla

Niko Matsakis: What agents mean for Rust (and vice versa)

Sheldon breathing into a paper bag.
Me, calmly assessing the implications of LLMs for programming language design(ers).

As someone who has made a career of programming language design, I definitely have moments of existential dread about the rise of LLMs. I started coding in 5th grade on an x861 that ran at 5MHz, had something like a 5MB hard-disk and 512K of RAM2. Computers were really, really different back then. But honestly, programming wasn't. For all the advances in IDEs and programming languages and so forth, the basic act of entering code into a file has remained surprisingly constant3 - right up until a few years ago, when everything kinda turned on its head. That's been exciting and empowering at times4 but also scary and disorienting. Will my skills in programming matter? What about my skills in programming language design (such as they are)? This blog post is my attempt to answer those questions.

So as not to keep you in suspense, let me just give you the conclusion. In short, yes, I believe there will still be a role for humans in programming. And yes, I think that programming language design is still relevant. And, naturally, I also happen to think Rust is a really good fit for agentic development - but that's not to say we can't make it a better fit. And that's what this post is ultimately about: what makes Rust and agentic development work well, and where we could double down on those strengths.

This is a kind of "blog post companion version" of a talk I gave this week at REBASE, part of SPLASH. You might also enjoy the slides from the talk I gave at IWACO, IWACO and Rust: hidden links revealed, which was a bit more of a retrospective (no soundtrack for those, though). In any case, this turned out to be a great conference! Jack Huey presented on the Rust Vision Doc and, quite to my surprise, Steve Klabnik and Dorian Scheidt presented "LLMs as Collaborators in Language Specification and Design", talking about their process in building out Rue. It was fun to see Steve again. On top of that, there was a ton of great research presented at IWACO in particular. I was particularly taken by the work on Reachability Types and Information Borrowing. I also really liked learning about Hylo Lang, particularly their approach to projections. Clever and cool.

Rust is popular in the agentic era

Meme dialogue: “I wrote this in Rust!” “Be honest.” “I am being honest!” “An agent wrote it.” “Thank you.”
From the most important Slack channel at Amazon, #aws-memes.

Rust is popular right now. Very popular:

Stratospheric among the breakout languages is TypeScript, cropped from the chart and sitting currently at +1200% growth from the prior year. [..]

The second most rapid recent growth is in Rust. Meta engineers have written twice as much first-party Rust code so far this year than in the previous 9 years combined.

- David Tolnay (emphasis mine)

Some of that is because agents make it very easy to try out new things. And some of that is because Rust has a reputation for being performant and, if it's just as easy to pick any language, why not pick one that will yield faster execution times?

But I think Rust is popular for another reason: because Rust happens to be a really good fit for agentic coding6. Of course, I would, wouldn't I? The point of this post is (1) to argue for why that is and then (2) to discuss what we might change about Rust to make it work even better.

Foundational Software construction with agents

It seems to me that an effective "software factory" will have three pillars:

None of these pillars are solved, but some have made more progress than others.

Rust and optimization: fast by default, knobs when you need 'em

Rust is designed to give "good performance by default", making the idiomatic thing typically also be the fastest thing. But another key part of Rust is that you have the knobs to eke out better performance when you need it. You control when something is stack- or heap-allocated and where pointer indirection occurs. If you want to, you can force the layout of your structs to be done in a particular way, or decide where to introduce boxing into your async stack frames. In the limit, you can put in inline assembly.

In the past, learning how to "tune the performance knobs" could be a bit of a black art: but agents are making that much easier.7 It turns out that agents are really good at fine-tuning the performance of existing code. For example, people who work on super high-performance cryptographic algorithms used to do so by hand-tuning assembly code. But those people tell me that they are now turning to agents for that same job. More prosaicly, a lot of people building network services are finding that, using a profiler like dial9, agents can quite effectively diagnose async performance pitfalls, like long polls or blocking.

Therefore, I think the task for Rust is clear. We keep on with our goal of "low-level enough for a kernel, high level enough for a GUI". If anything, I think the shift around agents means we can tolerate a bit more "noise" in the form of explicit calls to clone() or share() - but not too much, since we still want the "happy path" of the code to be clear and evident8, even as we surface details that are important in specific scenarios (like tracking precisely how many clones you have of a channel endpoint). Combined with a profiler, you get an effective feedback loop to get your code running fast:

flowchart LR
    Code -- Benchmark --> Profile
    Profile -- Analyzed by --> Agent
    Agent -- Propose --> PR
    PR -- Improve --> Code

Reliability is king, as always

As usual though, while a reputation for good performance is what brings people to Rust, what makes them want to stay is a sense that using Rust "just seems to work better". The basic theory is that Rust's type system and guardrails help keep agents on track:

I think there's truth in that: languages like Rust, Ocaml, or Haskell all share this "if it compiles, it works" feeling, and I think that agents will benefit from that.

Testing is not enough, type systems help

Testing can show the presence of bugs, but not their absence.

- Edsger W. Dijkstra, 1970

A woman presents a lopsided cake with the words “Nailed it!”
Agents presenting their work.

Writing tests has never been enough to show that your program is correct - but, with agents, it's not even close. It happens so often that my first few tests seem great and then the next one goes completely bonkers. Usually bonkers in a way where I cannot even imagine how that bug could have come about. Then I dig in and I realize the agent completely missed the boat on the logic I was trying to express.9

This is where a type systems really shines - particularly an advanced one like Rust. Type systems give you some guardrails that keep the agent on track. In Rust, those guardrails extend beyond simple stuff like "do all fields have the correct names" and to stuff like never having to close a socket.

Type systems are not enough either

Type systems can show the absence of bugs, but not the presence of correctness.

- Me, failing to coin a phrase of equal eloquence10, 2026

So yeah, type systems are helpful! But they have inherent limits. A type system is a simple set of rules that, if you follow them, make sure that you avoid (certain kinds of) mistakes. But they don't tell you that you do the right thing - only that you don't do (certain kinds of) wrong things. If you want to go further, you need a proof system - something that will let you show that richer properties are actively true, not just that you're avoiding bugs.

As it happens, there are a lot of interesting proof tools for Rust, like Verus, Creusot, Aeneas, and Kani. As a starting point, you can prove that your code is panic-free, which will eliminate a lot of bugs, though it is still fundamentally a "type-checker-like" property (i.e., you avoid doing things wrong). But you can also go further and add assertions that show your code is computing the results you expect.

Strong guardrails give better performance

Deplying proofs is not just good for getting code right - it's good for getting code fast. This is somewhat counterintuitive, but it's true. Earlier I mentioned how optimized cryptographic algorithms were now being written by agents. Part of what makes that possible is that cryptographic algorithms have a very clear mathematical definition. This means that you can basically tell the agent "do whatever you want, as long as you can prove that the code still computes the correct result". These proofs can be done with theorem provers like Lean or Rocq. The blog post "Why Lean is faster than Rust" makes the point quite well.

For Rust, a good example of this would be around unsafe code. Right now, people are sometimes reluctant to deploy unsafe code even if it might make their code faster because it's not worth the risk of getting it wrong. And I applaud that effort. But what if you could use a prover to show that your unsafe code is, in fact, safe (i.e., incapable of causing undefined behavior)? Then you'd be free to optimize to your heart's content.

If we are going to prove things, do we need type systems?

You might wonder: if we're deploying a proof system on our code, do we still need type systems? I think the answer is definitely yes. Type systems are infinitely simpler to work with, which is why they are much more popular. Using a type system lets you rule out all kinds of annoying bugs so that you can focus your "proof energy" only on the important stuff.

As a simple example of this, consider the following Java code:

void setFoo(Bar bar) {
    this.foo = bar;
    assert this.foo == bar;
}

Without seeing more code, it is impossible to prove whether this assertion is true or not! This is because there could be any number of other threads running around mutating this. In contrast, the following Rust code must be true (at least, so long as the Eq operator is reflexive for Bar):

fn set_foo(&mut self, bar: Bar) {
    self.foo = bar;
    assert_eq!(self.foo, bar);
}

We know this because the type system of Rust guarantees that &mut self implies a unique reference.

This is in fact exactly how Verus works. By trusting the Rust borrow checker to track uniqueness etc, it simplifies the job of the SMT solver, making proof checking must faster and more reliable than it would be otherwise.

Where I think Rust should go on reliability

So my take is that Rust should double down on if it compiles, it works. As expressive as Rust's type system is, there are plenty of things that it cannot capture. This includes fairly common things, like this method only reads one particular field or internal references, but also fancy things like "no logging of personally identifiable information". We should work to lift those limits, giving agents room to prove more complex properties.

We also need to improve the experience of integrating a proof tool by working towards an extensible compiler. As cool as the existing Rust-based proof tools are, using them is a janky experience involing annoying macros and pinned compiler versions. We can do better.

A north star: No more unsafe code

I'd like to propose a north star for Rust: no more unsafe code. By that, I don't mean that we never use the unsafe keyword. Rather, I mean that we have the power to prove that all the unsafe code we write is correct and cannot cause undefined behavior. Don't get me wrong: knowing exactly what code needs to be vetted is a huge step forward, as is normalizing the idea that libraries need to be responsible for protecting their users from undefined behavior via safe API boundaries11. But given agents' ability to find vulnerabilities, I think we need to up-our-game if we want to stop the steady stream of CVEs.12

Design is an open problem

But before you go about proving things or optimizing them, you need to have a clear idea of what you are building. As far as I can tell the state of the art here is basically variations on "markdown-driven-development", developing docs and hoping that agents pay attention.

I don't know how much of a role for Rust there is in this space. I think there are some steps we might wind up taking that could be helpful here - for example, having ways to separate out interface from implementation so that it's easier to review the interface in isolation or to see when the agent made changes there.13 Or perhaps just providing betters tools to review that.

I also think there's space for dedicated "modeling languages", something that let you iterate quickly with agents on the high-level designs and invariants without having to get into the weeds and read the code. I have more thoughts on this but it merits many blog posts all of its own. For the moment, I'll start by pointing you all at this post by Kari Wilhelm, "Principles of Anchor Engineering", which I think does a nice job of describing what it means to pull out the key elements of a design and drive the coding from there.

Conclusion

We covered a lot of ground here, so let me put this all together. What makes Rust a good choice for developing with agents?

And what could make it better, from a language design perspective? Overall, I think it's very similar to what we were doing, except that the way we weight the tradeoffs is tweaked to account for agents doing the code authoring, and humans focused more on code comprehension:

As a final close, let me point you at this interesting article by Marc Brooker, "What's easy now? What's hard now?". He posits that the more it is possible to clearly specify success criteria for a task, the easier it is, and that we may find that tasks we traditionally think of as 'hard' (e.g., building out an efficient implementation of a cryptographic algorithm) may soon become automated, whereas tasks that we have thoght of as 'easy' (e.g., making a unique, compelling website) may become more valued.

Looking at it from a PL point-of-view, I think Marc's point reinforces my sense that the biggest action is going to come from design languages, things that let you capture the architecture and intended behavior at a very high-level. The goal would be to let humans intuitively specify a design that gets translated into effective guardrails, whether that's type system checks, lints, or theorems to be proven. Agents would then take on the task of translating the design into code written in a traditional PL like Rust, with humans looking at it only rarely. This doesn't make the design of traditional PLs less interesting, but it definitely makes the tradeoffs very different than they were before.

  1. Secretly I have always been jealous of people that coded using punchcards and stored things on gigantic rolls of tape or whatever. I just want to be world weary so badly! I am kinda delighted that I'm finally old enough that I can say things like "I remember when we had to edit CONFIG.SYS before we could play a computer game!" and younger programmers will gasp in horror.5 But I still feel like I must sound like a silly kid to folks who were around "back in the day". ↩︎

  2. I still remember when my dad told me he had bought me a 10MB disk and secretly he had bought a 40MB disk to surprise me. It seemed absurdly large. "I'll never need a new disk again!" ↩︎

  3. I mean my god, we're even using vi again! My first editor! ↩︎

  4. I built an electron app! And it was so easy to do! And reading weird papers and things is so much more accessible now that I can ask an LLM to translate all the math jargon for me. ↩︎

  5. I remember once trying to tell Alex Crichton how I used to "order shareware from a paper catalog by putting a check in the mail" and he was like "I do not understand any of the nouns in that sentence". Highlight of my life, right after Rust 1.0. Oh, and maybe the birth of my child and getting married. I guess. ↩︎

  6. I'm not saying Rust is the only language that's a good fit. I'm not even saying that the way that Rust is a good fit is the only way to be a good fit. I have heard for example that Go is a really good fit for agentic coding and I believe it: I think it hits a different sweet spot, one that helps agents iterate quickly (although I do suspect agents will let data races and subtle bugs slip through that Rust would have prevented). ↩︎

  7. The fact that agentic development makes more room for knobs is good for Rust performance, but it is quite likely an even better fit for performance in other languages. Tuning a GC has traditionally been a job that really requires a GC expert, but agents can likely fill that role pretty well these days. ↩︎

  8. On this pont, I'm even more convinced of the importance of ergonomic RC now that I work with agents. Agents are good at introducing the extra clones and things you need to deal with capturing around async tasks, but the resulting code is so annoying to read, it really hides what's going on. ↩︎

  9. "Claude, this is not what we talked about!" - me, all too often. ↩︎

  10. So close though, right? I just .. couldn't land the plane. ↩︎

  11. All too often, C++ libraries consider it adequate to tell users "you're holding it wrong" - i.e., that they are responsible for causing undefined behavior by misusing the API. Rust takes a clear position that a safe API has to protect its users, no matter how much they abuse it. ↩︎

  12. To be fair, if Rust is encountering a stream of CVEs, other languages like C++ and Java are encountering a veritable flood, since they lack the protection of Rust's type system. st takes a clear position that a safe API has to protect its users, no matter how much they abuse it. ↩︎

  13. The revenge of .h files? ↩︎

14 Oct 2026 4:19am GMT

13 Oct 2026

feedPlanet Mozilla

Firefox Tooling Announcements: Happy BMO Push Day! (20261013.2)

Github Link

The following changes have been pushed to bugzilla.mozilla.org:

Discuss these changes in the BMO Matrix Room

1 post - 1 participant

Read full topic

13 Oct 2026 10:21pm GMT

Firefox Developer Experience: Firefox WebDriver Newsletter 158

With the WebDriver related release notes part of the MDN developer release notes and having a 2-week cycle for new Firefox releases now we are going to stop publishing this newsletter. This one will be the last one of the series of blog posts that we did since Firefox 114.

Thank you to everyone who followed these posts and provided feedback over the past releases.

WebDriver is a remote control interface that enables introspection and control of user agents. As such, it can help developers to verify that their websites are working and performing well with all major browsers. The protocol is standardized by the W3C and consists of two separate specifications: WebDriver classic (HTTP) and the new WebDriver BiDi (Bi-Directional).

This newsletter gives an overview of the work we've done as part of the Firefox 158 release cycle.

Contributions

Firefox is an open source project, and we are always happy to receive external code contributions to our WebDriver implementation. We want to give special thanks to everyone who filed issues, bugs, and submitted patches.

In Firefox 158, multiple WebDriver bugs were fixed by contributors:

WebDriver code is written in JavaScript, Python, and Rust, so any web developer can contribute! Read how to set up the work environment and check the list of mentored issues for Marionette or the list of mentored JavaScript bugs for WebDriver BiDi. Join our chatroom if you need any help to get started!

All Changes

A complete list of developer-facing changes included in this Firefox release is available in the MDN Firefox 158 Release Notes.

13 Oct 2026 6:02pm GMT

Firefox Tooling Announcements: Firefox Profiler Deployment (October 13, 2026)

The latest version of the Firefox Profiler is now live! Check out the full changelog below to see what's changed:

Highlights:

Other Changes:

Big thanks to our amazing localizers for making this release possible:

Find out more about the Firefox Profiler on profiler.firefox.com! If you have any questions, join the discussion on our Matrix channel!

1 post - 1 participant

Read full topic

13 Oct 2026 3:10pm GMT

The Mozilla Blog: Mozilla introduces Firefox Enterprise

Institutions are recalculating who controls the technology they rely on. Mozilla has an independent option to offer.

For years, organizations consolidated technology around a small number of providers to make things simpler. Fewer systems. Tighter integrations. More economies of scale. But that consolidation went well beyond technology. It consolidated dependency, too. The resulting risks have been debated, studied, and challenged along the way, but concentration continued. More work, data and critical infrastructure kept moving to the same few providers, while credible alternatives narrowed.

The deeper that dependency runs, the harder and more costly it becomes to change course. When something fails, changes or falls outside an institution's control, that dependency becomes a risk for CIOs and CISOs to manage.

Nowhere are these stakes more visible than in Europe. Now institutions are re-assessing. Governments are pushing for greater digital autonomy, while regulated industries face growing pressure to find and manage their dependencies.

There's a name for much of this debate about technological control: "sovereignty."

What digital sovereignty means in practice varies. Across Europe, governments are investing in the security and resilience of critical IT infrastructure, reducing strategic dependencies and putting technological autonomy higher on national agendas. Different approaches, same underlying concern. Strip away the regional policy definitions and industry distinctions and a pretty practical, universal question emerges: how much technological dependency should we risk?

And a very specific, very important layer has been largely missing from that conversation: the browser.

The overlooked layer of modern business

The browser. Applications run there. Employees authenticate in it. Sensitive data transits through it. Files are uploaded and downloaded and AI tools are increasingly used through it. That raises the same questions of dependency and control: whose browser technology are you relying on, and who controls the infrastructure used to manage it?

Introducing Firefox Enterprise

Firefox Enterprise is built for organizations with strict security, governance, and compliance requirements. It pairs the Firefox browser, built on Mozilla's independent Gecko engine, with a management console organizations can run on their own infrastructure. From that console, IT teams can centrally manage browser policy and access, govern how data moves through the browser and set controls around AI use.

IT and security teams get more control over their data, IT infrastructure and browser environment - helping strengthen technological independence and operational resilience.

"If all your options are built with the same technology underneath, 'choice' is a lie. So is control," said Anthony Enzor-DeMeo, CEO of Mozilla. "We built Firefox differently. And we're bringing its independent architecture to institutions that are ready to rethink their dependencies and risk."

Bringing the browser under control

We're starting with the browser because we see it as a key, but under-governed, layer. Firefox Enterprise gives institutions more control over the browser and the infrastructure managing it.

And because Firefox runs on Gecko, the only major browser engine developed outside Google and Apple, institutions have another path towards reducing dependence on a single architecture.

Finally, Firefox Enterprise is built to live alongside the systems that IT operations already use. Keep your identity provider. Keep your SIEM. Keep your MDM. Just add a browser whose management infrastructure you operate, so you decide where data lives and have greater visibility into how it moves.

For us, supporting the goal of technological sovereignty comes down to four things: More control. More transparency. More choice. More resilience.

Learn more about Firefox Enterprise.

A big bet on familiar ground

We know this territory. Independence isn't a new direction for Mozilla. We've spent more than 25 years building and securing browser technology that intentionally works outside of the dominant architecture of the day. Firefox is used by roughly 200 million people every month and is already deployed across thousands of organizations.

That independence has always mattered to the web. Now it has practical value for institutions looking to reduce technological concentration - and dependency - in their own environments.

This is the beginning

Our ambition is big but simple: make technology independence practical.

That means putting institutions in real control of the infrastructure and data they depend on, without asking them to rebuild or start over. Closing blind spots. Defining where policies, access and data live. Keeping core management within the institution's environment. And bringing an overlooked layer - the browser - under institutional control.

Firefox Enterprise is unveiling across Europe with an initial sales focus on France, Germany, Austria and Switzerland, with more markets to follow. Thunderbird Enterprise is also in development, extending this customer-controlled approach to email and communications. We'll have more to share as that work progresses.

If your organization wants greater control over its browser infrastructure, we'd like to work with you.

The post Mozilla introduces Firefox Enterprise appeared first on The Mozilla Blog.

13 Oct 2026 4:01am GMT

10 Oct 2026

feedPlanet Mozilla

Niko Matsakis: Why 'externalized' proofs of cyclic trait impls does not work

For this post, I wanted to talk about two different approaches to handling supertraits. I'm calling them modular proofs vs external proofs. The key idea of this post is that, if we want to have cyclic trait impls, we really need to use a modular proof strategy, where the impl establishes all supertraits hold. Previously we had considered an external strategy, where the piece of code using the impl has the obligation to prove the supertraits hold. Modular proofs always seemed better but I did not think they were workable in the past. But I have become convinced that external proofs are incompatible with Rust as designed, and hence modular proofs are really the only option1. This post dives into that reasoning, and also gives a bit of explanation of what I mean by proofs in the first place.

Traits and supertraits

So what do I mean by modular vs external proofs? Well, it all comes down to who is responsible for proving that supertrait obligations hold. Consider a trait like Magic:

trait Magic: Copy { }

The supertrait declaration means that, whenever X: Magic for some type X, it should be true that X: Copy. We make use of this in generic functions:

fn is_copy<T: Copy>() {
}

fn is_magic<T: Magic>() {
    // Legal, because `T: Magic` implies `T: Copy`
    is_copy::<T>();
}

The trick is that the compiler has to make sure that this implication holds - i.e., for every type X that implements Magic, X also implements Copy. So how does it do it?

Modular proofs: the impl must show supertraits hold

The obvious answer is to make proving supertraits part of deciding whether an impl is valid. For any impl of Magic, we can require that the Copy supertrait holds. So an impl like this would be illegal:

// In a modular system, this impl is *illegal*
impl Magic for String { }

This impl is illegal because it would require that String: Copy, and that does not hold. Seems good.

Modular proofs are a bit tricky

I am calling these proofs modular because the idea is that we can prove an entire program is valid by proving each part of it separately. In "programming language" theory, this is typically called a "modular" check, as it works by breaking up the entire program into modules that can be independently checked.

The idea with a modular proof is that we can trust impls to show that the supertrait relationships hold, we don't have to go and re-prove them over and over. If the impl is wrong, the impl will be invalid, but our code is fine. So if we have impl Magic for String, that implies the rest of the program can prove that String: Magic:

fn string_is_magic() {
    // Legal, because there is an impl for `String: Magic`:
    is_magic::<String>();
}

In fact, since we know that Magic implies Copy, the rest of the program can even rely on impl Magic for String to conclude that String: Copy:

fn string_is_copy() {
    // Legal, because there is an impl for `String: Magic`,
    // and `Magic` implies `Copy`:
    is_copy::<String>();
}

So long as impl Magic for String is invalid, none of this poses a problem to soundness, since the program overall doesn't type-check.

Comparison with functions

An easy way to understand the idea of modular checks is to think of functions. Imagine you have a function like this one:

fn compute_sum(a: i32, b: i32) -> i32 {
       format!("{a} + {b}") // <-- Error
}

Clearly, this function is not legal. It takes two integers and promises to return a third integer, but in fact it returns a String. So the function is illegal. But if you have a call to that function from elsewhere, we consider that other call to be legal:

fn use_sum() {
    let c: i32 = compute_sum(2, 20); // OK
}

Here, use_sum is relying on compute_sum to obey its contract. It's not the job of use_sum to check that, it can just assume it is true.

The catch: how do we decide the impl is invalid

There is a bit of a catch though. How do we decide if the impl is invalid? The basic idea was that impl Magic for String would have to prove that String: Copy. But we just saw that it could, in fact, do that by using itself. In other words, if we aren't careful, we can provide a proof that String: Copy like…

and then we would (incorrectly) conclude that the impl is valid. So clearly we need to do something to rule that out. We need a rule that says, when we are proving that an impl is valid, that proof cannot recursively rely on the impl itself.[^termination] I'll come back in a future post to ways we might do that, but for now, I want to explore another alternative.

External proofs: the user of the impl must show supertraits hold

When we first looked at this problem, way back in 2018 or so, we thought of another approach. What if we said that an impl is not responsible for proving supertraits. Instead, the idea would be that impl Magic for String is not enough to say that String: Magic. It only says that Shallow(String: Magic) - i.e., String implements Magic in a shallow way, but not in a deep way that includes the full supertraits. To prove that String: Magic, we have to show that Shallow(String: Magic) and Shallow(String: Copy):2

Shallow(String: Magic)
Shallow(String: Copy)
---------------------------- Magic fully implemented
String: Magic

This has the somewhat counterintuitive implication that impl Magic for String is actually legal in an "external proof" approach:

// In an external system, this impl is LEGAL
// (but unusable)
impl Magic for String { }

The saving grace is that, while this impl is legal, you can't actually use it. This function for example does not compile:

fn string_is_magic() {
    // NOT legal in an external system:
    // * We can prove that `Shallow(String: Magic)`
    // * We CANNOT prove that `Shallow(String: Copy)`.
    is_magic::<String>();
}

Here, String: Magic doesn't hold even though there is an impl of Magic for String, because the caller also has to check that String: Copy is implemented, and it is not. Huh, interesting.

Comparison to functions: external is awkward

the "external proof" approach for impls is clearly a bit awkward. If we make the comparison to functions, it's as if the caller has to double check that the callee's body matches its return type, it can't actually trust the declared signature. But, awkward or not, it does resolve our problem: given impl Magic for String, we cannot prove String: Copy, and hence we cannot prove that String: Magic. We can only prove that Shallow(Magic: String), which doesn't imply that the supertraits hold.

But external doesn't work with unsafe traits

Based on the above, for a long time, I was working with the assumption that, weird as they are, we would go with the "external proof" approach. However, as Ralf Jung and lcnr pointed out to me recently, this is very challenging to reconcile with unsafe traits. Consider an unsafe trait like Nullable:

// A type that can be safely transmuted from `0_usize`.
unsafe trait NullWord { }

The way that Rust works, when we write an unsafe impl, it is the job of that impl to prove that the unsafe conditions hold. Other parts of the program get to trust the impl. So if I write a function like this one, it should be considered safe:3

fn foo<T: NullWord>() -> T {
   std::mem::transmute(0_usize)
}

Now imagine that I wrote an invalid impl like this one:

// INVALID: We are asserting that `Box` can be null,
// which is not true!
unsafe impl<T> Nullable for Box<T> { }

Given this program I could clearly call foo::<Box<u32>>(), but that would "go wrong" (cause "undefined behavior"). I think we would all agree that the fault lies in the impl. And yet, that is inconsistent: we say that the impl alone cannot be trusted to figure out if the supertraits are implemented, but it can be trusted to figure out if the unsafe impl is valid?

Conclusion

I definitely believe that we want to treat the "extra conditions indicated by unsafe" as a more general version of the other obligations that an impl has to establish to show that the trait holds- and therefore that we must have modular proofs. That's kind of a relief, because something always felt wrong about external proofs, but it was hard to put my finger on a concrete problem. In the next post in this series (whenever that may be…), I expect to cover the approach to coinductive modular proofs that I landed on. Then I expect to talk about an alternative that was proposed to me that I find quite appealing.

  1. I think this was obvious to Ralf Jung from the start. But it took me a bit. ↩︎

  2. This notation is called an inference rule. The conditions above the line are the premises and the bottom line is the conclusion. It says that, if you know the premises are true, you can infer that the conclusion holds. ↩︎

  3. In point of fact, I believe this will not compile because of special rules about unsafe, but that's not relevant to the point I'm trying to make. ↩︎

10 Oct 2026 3:23pm GMT

09 Oct 2026

feedPlanet Mozilla

Firefox Tooling Announcements: Firefox DevTools MCP 0.10.5 released

New release of Firefox DevTools MCP. Available on npm at https://www.npmjs.com/package/@mozilla/firefox-devtools-mcp

Fixed

Changed

Full changelog: Release v0.10.5 · mozilla/firefox-devtools-mcp · GitHub
Repository and issues: GitHub - mozilla/firefox-devtools-mcp: Model Context Protocol server for Firefox DevTools - enables AI assistants to inspect and control Firefox browser through WebDriver BiDi · GitHub
Public chatroom: https://chat.mozilla.org/#/room/#firefox-devtools-mcp:mozilla.org

1 post - 1 participant

Read full topic

09 Oct 2026 2:03pm GMT

08 Oct 2026

feedPlanet Mozilla

Mozilla Open Policy & Advocacy Blog: Canada’s bill C-22 threatens encryption, users’ privacy and the security of digital economies

Encryption is woven into everyday digital life. It protects our messages and passwords, but also banking and payments, health data, government services and the digital infrastructure societies rely on every day. Yet across jurisdictions, governments are increasingly considering laws that expand lawful access to data for law enforcement and national security purposes. In practice, this can mean requiring companies to create new ways to access encrypted data, introduce technical capabilities that bypass existing protections, or make otherwise secure systems insecure. These measures can weaken the very security encryption is designed to provide, with consequences for cybersecurity, privacy, fundamental rights and the wider economy. Canada's Bill C-22 is the latest example of this trend, raising serious concerns about the security and privacy consequences of expanding government access to data.

For Mozilla, protecting that security is fundamental to both the products we build and the principles we advocate for. One of the foundational principles that guide Mozilla's mission and work holds that individuals' security and privacy on the internet are fundamental and must not be treated as optional. Protecting people's privacy and security is not an aspiration for us, but shapes the products we build every day: Firefox blocks trackers, protects you from profiling via cookies and fingerprinting, comes with malware protection and a built-in VPN, offers HTTPs-only mode and protects your passwords and credit card information by encrypting them.

Some of these protections are being threatened by Canada's Lawful Access Act, also known as bill C-22. Part two of the bill, the "Supporting Authorized Access to Information Act" (SAAIA) would introduce sweeping new powers to require electronic service providers to build and maintain capabilities that facilitate government access to information. If passed in its current form, companies could be asked to introduce vulnerabilities, build backdoors, bypass, weaken or otherwise defeat encryption, access data before encryption or decrypt encrypted data to provide access to law enforcement. Service providers could also be compelled to retain and access data they have purposefully chosen not to collect.

Let us be clear: there is no safe way to create exceptional access to encrypted data that only the intended actor can use. An access mechanism created for law enforcement can also be discovered, exploited or abused by potentially bad actors.

Such vulnerabilities and backdoors do not only undermine people's fundamental rights to privacy and data protection, but also the trust and security premises societies everywhere depend on. The same encryption that protects a private conversation also protects financial transactions, sensitive health information, business systems and critical digital services.

Expanding capabilities of AI systems are only exacerbating these risks - governments should encourage the disclosure and patching of vulnerabilities, not compel companies to introduce insecurities deliberately. Only trustworthy and transparently governed digital infrastructures can be the basis for digitally sovereign societies.

We are also concerned by C-22's scope, which does not stop at Canadian services or users. C-22 expansive surveillance capabilities and data retention obligations would undermine people's privacy and security everywhere, and the bill's confidentiality requirements would make it impossible for services to inform their users about security breaches or backdoors introduced.

Guided by our Surveillance Principles for a Secure, Trusted Internet, we call on Canadian policymakers not to rush the legislative process to take experts' feedback into account in amending C-22 to protect everyone's security and privacy. Canada's interests are best served by regulation that protects encryption, strengthens cybersecurity and emphasizes transparency, checks and balances.

The post Canada's bill C-22 threatens encryption, users' privacy and the security of digital economies appeared first on Open Policy & Advocacy.

08 Oct 2026 9:35am GMT

The Mozilla Blog: Firefox partners with Anschutz Entertainment Group at the Uber Arena and Uber Eats Music Hall in Berlin

Firefox is teaming up with AEG and taking to the main stage at Berlin's biggest and best indoor arenas. Starting this October, as the indoor music scene heats up and the basketball and ice hockey seasons are in full swing, fans flocking to the Uber Arena, Uber Eats Music Hall, and Uber Platz will see Firefox highly visible around the venue. They may even bump into our very own mascot, Kit, who will be on hand to help them skip the main queues courtesy of Firefox.

We know that the experiences people care about often begin online. The internet is the gateway to how they discover, plan, and navigate their way to concerts, sports events, and nights out before they happen in real life.

Firefox's presence will help make every step of that journey simple and smoother, starting at the door.

People with Firefox downloaded on their phone will have access to a dedicated Firefox Fast Lane that allows them to skip the main line at the Uber Arena. To ensure the smoothest possible entry, a QR code for downloading Firefox will also be available at the Fast Lane.

"People who use Firefox tend to choose things deliberately, their browser, their music, their nights out. This partnership is for them. A first for Firefox. Most browsers want more of your time online. We want you at the show, faster. Berlin is where we are starting, right across the river from our office. See you there," said John Solomon, Mozilla-Firefox Chief Marketing Officer.

We are excited to bring what we stand for to Berlin's premier entertainment venue - choice, control, and a better experience to the moments that people want to enjoy and truly care about.

The post Firefox partners with Anschutz Entertainment Group at the Uber Arena and Uber Eats Music Hall in Berlin appeared first on The Mozilla Blog.

08 Oct 2026 7:00am GMT

07 Oct 2026

feedPlanet Mozilla

The Mozilla Blog: Jambu Palaniappan and David Parry-Jones join the Mozilla Corporation Board of Directors

Today, we are very pleased to announce two new additions to the Mozilla Corporation Board of Directors: Jambu Palaniappan and David Parry-Jones.

As we build the next chapter of Mozilla, we've been focused on bringing people onto our Board who combine deep operating experience with a real commitment to the values Mozilla stands for. Jambu and David bring deep experience building and leading technology businesses, and each brings a unique perspective to our Board.

Jambu Palaniappan is the Chief Executive Officer of Checkatrade, where he drives the company's mission of Powering Great Work. The home improvement platform connects consumers across the UK with quality tradespeople - every year, Checkatrade improves millions of homes and delivers billions of pounds of work to small and medium-sized businesses.

Before joining Checkatrade, Jambu was Managing Partner and Head of Europe at OMERS Ventures, where he invested in and supported high-growth technology companies. Earlier in his career, he spent several years at Uber and Uber Eats, joining as one of the first 100 employees and leading expansion across Europe, the Middle East, and Africa. Jambu holds a degree in Public Policy and Economics from Vanderbilt University.

David Parry-Jones is a board director and former Chief Revenue Officer (CRO) with more than 30 years of experience scaling technology businesses internationally. Most recently, he served as CRO at DeepL and previously held senior leadership roles at Microsoft, VMware, and Twilio. He has led large teams across diverse markets and cultures, working with both early-stage companies and global enterprises.

As a board member and adviser, he brings a practical perspective on growth, international expansion, and building strong teams that turn strategy into results.

Please join me in welcoming Jambu and David to the Mozilla Corporation Board of Directors.

The post Jambu Palaniappan and David Parry-Jones join the Mozilla Corporation Board of Directors appeared first on The Mozilla Blog.

07 Oct 2026 6:37pm GMT

The Mozilla Blog: 100 days later: Microsoft still steers Windows and Copilot users to Edge, everywhere the law lets it

One hundred days ago, Mozilla released Over The Edge 2.0, the second independent report from leading experts on deceptive design Dr. Harry Brignull and Cennydd Bowles, on how Windows, Edge, Bing, and Copilot are designed to steer people away from the browser they chose.

We published the report, and the researchers published the evidence for anyone to analyze.

Browsers are a powerful tool. So it's no surprise that the history of the web has many examples of powerful platforms trying to deny people browser choice. Now, as AI reshapes our online experiences, the stakes couldn't be higher. Browsers are a key distribution layer for AI tools and services, while still determining many of the privacy and security functionality people rely on every day. Steering people toward one browser can therefore shape which AI services reach users and the protections that come with it.

We also shared the report with Microsoft and talked to them about the issues raised in the report. We knew that an immediate change was unlikely, but we hoped that, when faced with independent evidence of harmful design practices impacting Windows users, they would also want better for people.

Instead, it became clear that Microsoft will respect user choice only when it is forced to. It is important to think about what that means for a company whose operating system runs on more than a billion machines. Microsoft's standard for respecting people's choices is legal compliance. Not what's best for its users. Not its own published principles. Not what's technically feasible. Not even what it already does for users in Europe.

That's the most shocking part. Not that Microsoft engages in such tactics - we've seen that before. It's the fact that a better version of Windows already exists, and it is already available today - but only if you live in the European Economic Area (EEA), where the Digital Markets Act (DMA) forced the issue. If you live in the United States, India, the United Kingdom, or most other locations around the world, your experience and your freedom to choose for yourself are worse.

One hundred days later, here is what people outside of the EEA still get:

And people in the EEA also deserve better:

Most of the 2024 patterns are still there. The 2026 patterns are worse. Microsoft is using new surfaces like Copilot and the migration to Windows 11 to further undermine user choice.

Our ask has always been simple: First, give all Windows users the fairer designs that are live in the EEA - regardless of where they are located. Second, stop the remaining harmful design practices that persist in the EEA. That means:

The Mozilla-commissioned report has never been about intent. It's about accountability and Microsoft's responsibility to stop undermining people's choices. The practices we documented need to change. Statements about intent are not a substitute for action.

In the past 100 days, we've stopped waiting for Microsoft to act. Instead, we've stepped up public pressure on the company to respect people's choices.

We are also taking the report's findings to regulators and policymakers. In Europe, the DMA is the only thing that has moved Microsoft. Everywhere else, the lesson is the same: Microsoft ships only when a regulator requires fairer design.

We hope that regulators in the US, the UK, India, and Brazil are paying attention.

Microsoft can do better. It already has, for people in the EEA.

Until it does the same in all jurisdictions, we will keep pointing out the company's choices and the impact they have on hundreds of millions of users who want something different.

The post 100 days later: Microsoft still steers Windows and Copilot users to Edge, everywhere the law lets it appeared first on The Mozilla Blog.

07 Oct 2026 10:00am GMT

This Week In Rust: This Week in Rust 672

Hello and welcome to another issue of This Week in Rust! Rust is a programming language empowering everyone to build reliable and efficient software. This is a weekly summary of its progress and community. Want something mentioned? Tag us at @thisweekinrust.bsky.social on Bluesky or @ThisWeekinRust on mastodon.social, or send us a pull request. Want to get involved? We love contributions.

This Week in Rust is openly developed on GitHub and archives can be viewed at this-week-in-rust.org. If you find any errors in this week's issue, please submit a PR.

Want TWIR in your inbox? Subscribe here.

Updates from Rust Community

Official
Foundation
Newsletters
Project/Tooling Updates
Observations/Thoughts
Rust Walkthroughs

Crate of the Week

This week's crate is karatepe, a statically typed localisation language and library.

Thanks to miro for the self-suggestion!

Please submit your suggestions and votes for next week!

Calls for Testing

An important step for RFC implementation is for people to experiment with the implementation and give feedback, especially before stabilization.

If you are a feature implementer and would like your RFC to appear in this list, add a call-for-testing label to your RFC along with a comment providing testing instructions and/or guidance on which aspect(s) of the feature need testing.

No calls for testing were issued this week by Rust, Cargo, Rustup or Rust language RFCs.

Let us know if you would like your feature to be tracked as a part of this list.

Call for Participation; projects and speakers

CFP - Projects

Always wanted to contribute to open-source projects but did not know where to start? Every week we highlight some tasks from the Rust community for you to pick and get started!

Some of these tasks may also have mentors available, visit the task page for more information.

If you are a Rust project owner and are looking for contributors, please submit tasks here or through a PR to TWiR or by reaching out on Bluesky or Mastodon!

CFP - Events

Are you a new or experienced speaker looking for a place to share something cool? This section highlights events that are being planned and are accepting submissions to join their event as a speaker.

If you are an event organizer hoping to expand the reach of your event, please submit a link to the website through a PR to TWiR or by reaching out on Bluesky or Mastodon!

Updates from the Rust Project

653 pull requests were merged in the last week

Compiler
Library
Cargo
Rustdoc
Rustfmt
Clippy
Rust-Analyzer
Rust Compiler Performance Triage

A relatively quiet week, but a very positive one nonetheless. Highlights are a 3.1% improvement in rustdoc speed from not using the metadata based crate_hash for rustdoc runs, a 0.5% improvement from a new fast path in the trait solver, and a 0.4% improvement from a cache for the parents of SpanData.

Triage done by @JonathanBrouwer. Revision range: c1070d69..cc9a14f7

Summary:

(instructions:u) mean range count
Regressions ❌
(primary)		 0.6% [0.4%, 1.0%] 12
Regressions ❌
(secondary)		 0.4% [0.1%, 0.9%] 26
Improvements ✅
(primary)		 -1.1% [-6.2%, -0.2%] 212
Improvements ✅
(secondary)		 -1.9% [-15.7%, -0.1%] 208
All ❌✅ (primary) -1.0% [-6.2%, 1.0%] 224

4 Regressions, 3 Improvements, 1 Mixed; 5 of them in rollups 33 artifact comparisons made in total

Full report here

Approved RFCs

Changes to Rust follow the Rust RFC (request for comments) process. These are the RFCs that were approved for implementation this week:

Final Comment Period

Every week, the team announces the 'final comment period' for RFCs and key PRs which are reaching a decision. Express your opinions now.

Tracking Issues & PRs

Rust

Compiler Team (MCPs only)

Language Reference

No Items entered Final Comment Period this week for Rust RFCs, Cargo, Language Team, Leadership Council or Unsafe Code Guidelines. Let us know if you would like your PRs, Tracking Issues or RFCs to be tracked as a part of this list.

New and Updated RFCs

This RFC will appear in the Call for Testing section of the next issue (#) of This Week in Rust (TWiR). You may remove the call-for-testing label. Please feel free to leave the call-for-testing label in place if you would like this RFC to appear again in another issue of TWiR.

Upcoming Events

Rusty Events between 2026-10-07 - 2026-11-04 🦀

Virtual
Asia
Europe
North America
South America

If you are running a Rust event please add it to the calendar to get it mentioned here. Please remember to add a link to the event too. Email the Rust Community Team for access.

Jobs

Please see the latest Who's Hiring thread on r/rust

Quote of the Week

There ain't no rules here in Quote of the Week - it's survival of the wittest

- Simon Buchan on rust-users

Thanks to Jonas Fassbender for the suggestion!

Please submit quotes and vote for next week!

This Week in Rust is edited by:

Email list hosting is sponsored by The Rust Foundation

Discuss on r/rust

07 Oct 2026 4:00am GMT

06 Oct 2026

feedPlanet Mozilla

Firefox Tooling Announcements: Happy BMO Push Day! (20261006.1)

Github Link

The following changes have been pushed to bugzilla.mozilla.org:

Discuss these changes in the BMO Matrix Room

1 post - 1 participant

Read full topic

06 Oct 2026 9:43pm GMT

The Mozilla Blog: Strengthen your online security for free with Firefox

Every October, Cybersecurity Awareness Month reminds us the importance of protecting our digital lives.

The theme for 2026 is 'Don't Make It Easy for Them,' with the National Cybersecurity Alliance (NCA) and the Cybersecurity and Infrastructure Security Agency (CISA) providing simple, actionable steps users can take to make it harder for cybercriminals to attack.

Everyone wants to be safe online, but one of the most common excuses we hear is "I don't have the time or the money to invest in it right now." Well, we have good news: you can improve your online security easily, for the low price of $0.

Firefox provides several free features designed to make it easier to protect your online life and harder for cybercriminals to target you.

Password manager: Use a unique password for every account

Reused passwords are one of the easiest ways attackers break into multiple accounts. If one site is breached, your login details could be tested on many others.

Firefox's free password manager can generate and securely store a strong, unique password per site, which is the single highest-leverage fix against password stuffing. For convenience, Firefox can automatically fill in your saved login information the next time you access a previously visited site. However, you still have the option to turn off password saving for specific websites, or completely if you're using a shared device or simply prefer to enter it each time.

You can manage your stored logins on a singular device at any time. To get a head start, you also have the option to import passwords saved on several other popular browsers. In addition, you can create a free Mozilla account to safely sync them across your signed-in devices.

VPN: Privacy built into the browser

Imagine you're settling into a corner table at a bustling airport cafe, checking some emails on your phone before you board your flight. Or perhaps you took your laptop to the campus library to finally start that research paper you've been putting off. Maybe you're polishing off that last presentation slide between sessions at an out-of-state conference.

While these moments are routine, connecting to public Wi-Fi anywhere can open a small window of risk - as your IP address, approximate location, and browsing activity can be more exposed on networks you don't control.

That's where Firefox's free built-in, browser-based VPN steps in. While Firefox already encrypts your traffic with HTTPS, the built-in VPN feature routes your browsing traffic through a proxy network, hiding your IP address before it reaches a website. This means the sites you visit will see a proxy IP address instead of your own. It offers an industry-leading 50 gigabytes of free VPN-browsing each month, with no extension or extra app to install. Simply sign in, turn it on, and start browsing.

Firefox's free built-in VPN first launched on desktop in March, later expanding to Android in July. Unlike a standalone or full-service VPN, it's designed specifically to protect your browsing traffic within Firefox, not your entire device. This means apps, downloads, and other system traffic are not routed through the browser-based VPN. For people who need broader, device-wide VPN protection, Mozilla also offers a separate paid VPN service.

You can check the full list of regions where built-in VPN in Firefox is currently available here, and learn more about the differences between Firefox's free built-in VPN and Mozilla VPN here.

Relay: Contain the damage of any one breach

Think about how often you give out your personal email address - for an online purchase, RSVPing to an event, or signing up to a new app. Each time, you trust the site owner will protect your information, but, spam piles up and breaches can still happen - even when you think you're being careful.

Firefox Relay gives you a smarter way to share. Instead of handing out your real email address, this feature provides secure, random email masks to use any time a website, store, or app asks you for your information. It forwards messages to your real email, while keeping your identity hidden to senders. This means if one service gets compromised, your other accounts stay safe.

You can also use Relay in the U.S. and Canada to shield your phone number, so you can receive calls and texts through masks and reply without exposing your real number.

The best part? To make protecting your privacy even easier, Firefox increased its limit to 50 free email masks earlier this year, allowing you to shield dozens of logins at no cost.

Browse freely: Firefox protects you by default

Even if you sometimes forget to use Firefox protection tools like password manager, VPN, and Relay, there are multiple always-on features operating within the browser to help keep your session secure and private. These include enhanced tracking protection to block hidden scripts and known trackers that follow you across the web, browser fingerprinting protection to prevent sites from building a unique profile of your device, and warnings about deceptive or malicious websites.

Together, Firefox's individual and always-on security features work to help keep your browsing safe and your data private. So, this Cybersecurity Awareness Month, take a moment to build new habits, try out our free cybersecurity tools, and make life more difficult for cybercriminals. Small steps add up, and we are here to help. Stay safe, stay smart, and keep exploring the web with confidence on Firefox.

The post Strengthen your online security for free with Firefox appeared first on The Mozilla Blog.

06 Oct 2026 4:00pm GMT

Ryan Hunt: Wasm Stack Switching in SpiderMonkey

WebAssembly stack switching in SpiderMonkey is the most complex feature I've ever implemented.

It's one of those projects where you get lost and start rethinking the basics, like "what is the stack even really?"

It was fun to give a talk on it. Check out the recording below, or on YouTube.

06 Oct 2026 3:00pm GMT

05 Oct 2026

feedPlanet Mozilla

Mozilla Data YouTube Channel: Towards a Telemetry Taxonomy

Leif Oines talks about an effort to define a more complete taxonomy for Mozilla's data.

05 Oct 2026 6:47pm GMT