Can a Compiler Prove Your C Code Is Safe?

There's a particular kind of audacity in a three-minute and fifty-second lightning talk that opens with "it's my first time at CppCon" and then immediately pivots to proposing new inference rules in the theory of dependent types. Raffaele Rossi—tech lead at Maven Securities by day, compiler researcher by night—pulled it off at CppCon 2025 in Aurora, Colorado, and the idea he's working on is worth sitting with longer than the applause allowed.

The backdrop is one you've been reading about in government memos and industry post-mortems for a few years now: C and C++ have a memory safety problem. Buffer overflows. Dangling references. The NSA has nudged organizations toward Rust. The White House has weighed in. The C++ community, to its credit, hasn't buried its head—CppCon itself has become a venue for wrestling with this publicly. Rossi's project, DepC, is one particular answer to one particular part of that problem, and it comes from a direction most systems programmers haven't thought much about: type theory.

What Proof Searching Actually Means

Most developers have an intuitive feel for type checking—you give the compiler an expression, it tells you whether the types line up. Rossi flips that: proof searching asks the compiler to go the other direction. You give it a type, and the compiler tries to find a value that inhabits that type.

"If this is searching a value, is it not called value search? Why is it called a proof search?" Rossi asks in the talk, almost preemptively fielding the question every developer in the room probably had. The answer—Curry-Howard correspondence, the deep mathematical relationship between type theory and formal logic where types are propositions and values are their proofs—is genuinely one of the more interesting rabbit holes in computer science. He's right that you should Google it.

But you don't need to go that deep to follow what DepC is doing in practice. Here's the concrete example Rossi walks through: a simple C program using argc/argv. You want to access argv[1]—the second element of the argument vector. In standard C, nothing stops you from doing this even if the user ran the program with zero arguments. You just get undefined behavior, and maybe a security vulnerability, and maybe a CVE years later.

In DepC, the type system encodes array lengths. Accessing argv[1] requires a proof that 1 is within bounds—that argc > 1. If you write the bounds check explicitly, the compiler's proof searching algorithm finds the proof automatically inside the if branch. The arithmetic is there; the compiler can see it; the access is verified. No annotation tax beyond the check you should have been writing anyway.

What happens when you don't want to write the check? Rossi is refreshingly direct about this: "if you're lazy or if it is too hard to prove things, you can just cheat and ask the compiler to believe you." He notes that in type theory terms, this escape hatch has the same type as the function absurd—a function that takes a proof of falsehood and produces anything. The name is the joke: "it is absurd to trust the programmer." And if your claim turns out to be wrong, you get the same undefined behavior you'd get in vanilla C/C++. No free lunch. But now—and this is the part Rossi clearly finds delightful—you can grep for the escape hatch in your codebase. Every trust-the-programmer override is an explicit, searchable marker in the source. That's a meaningful operational difference from the status quo, where unsafety is invisible by default.

The Undecidability Problem Is Real

Here's where I want to add something Rossi's lightning talk format didn't have time to fully unpack, because it matters for evaluating what DepC can and can't be.

Proof searching in dependent type theory is, in the general case, undecidable. Rossi acknowledges this plainly: "if you know anything about type theory, this thing is undecidable. So you're not guaranteed to find a solution." The compiler spawns tasks and subtasks, applying multiple tactics, working through the proof search space. Sometimes it succeeds. Sometimes it doesn't. And when it doesn't, Rossi has built in a trace mode—"I can turn on a trace [to see] exactly all the things that I tried and explain why it didn't find a proof that I hoped it would find."

That trace-on-failure feature is good tooling instinct. One of the recurring complaints about dependently typed languages like Idris or Agda from systems programmers who've poked at them is that when the type checker fails, the error messages are often cryptic in ways that make iteration painful. A trace that explains the proof search failure is the kind of developer experience detail that separates a research prototype from something usable.

But the undecidability ceiling is worth thinking about carefully. In practice, most of the bounds checks that matter in real systems code are not exotic—they're simple arithmetic relationships of exactly the kind Rossi demonstrated. The question for DepC's viability is whether its proof search tactics cover enough of the common cases to be useful without requiring programmers to become type theorists. Rossi's demo suggests the simple cases work. The harder ones—pointer arithmetic through multiple functions, complex data structure traversals—remain an open question for the project.

The Bigger Picture: This Isn't Rust

It's worth being precise about what DepC is and isn't, because the memory safety conversation often collapses into "just use Rust" in a way that obscures genuine technical tradeoffs.

Rossi notes in the video description that Rust's borrow checker addresses the other major class of memory safety error—dangling references—but "its approach is unique and does not reconcile with Dependent Types." These are genuinely different formal tools addressing overlapping but distinct problem domains. Rust's ownership model is a specific kind of type system discipline; dependent types are a more general mechanism for encoding arbitrary invariants in types. Combining them is an active research area, not a solved problem.

DepC's bet is that you can bring dependent types to a C/C++-like language and get meaningful safety guarantees—specifically around buffer overflows—without requiring developers to adopt an entirely new language and ecosystem. That's a bet worth watching, because the ecosystem costs of migration are real and often underweighted in conversations that focus purely on language properties.

What Rossi is building isn't a Rust competitor and probably shouldn't be evaluated as one. It's closer to asking: what if the C compiler could reason about your runtime invariants, instead of just trusting you got them right? For a language where "undefined behavior" has caused decades of security vulnerabilities, the question is genuinely non-trivial.

The Side-Project Reality

There's something I keep noticing at conferences like CppCon, and Rossi's talk crystallizes it: some of the most interesting language and tooling research is happening in the margins of people's professional lives. Rossi describes working on DepC "in my spare time." The formal systems research that underlies what he's doing has been developed across decades by academics who often weren't paid to do it either.

This isn't romantic. It's a sustainability question that the open source community hasn't resolved. The proof searching algorithm Rossi described took real work to implement. The tactics engine, the trace output, the integration with dependent type inference rules—that's not a weekend hack. When tooling that addresses critical infrastructure security problems lives in someone's evenings and weekends, the question of what happens to it when life gets busy is legitimate.

The applause at the end of Rossi's talk was warm and deserved. Whether DepC goes anywhere probably depends less on the elegance of its type theory than on whether it finds a community, a funding path, or an institutional home that makes sustained development possible.

"It is absurd to trust the programmer," Rossi says—and he means it as a joke about type theory. But there's a version of that observation that applies to the whole enterprise of memory safety: we've been trusting individual developers to get it right for fifty years, and the CVE database is the evidence of how that's gone. Whether the answer is Rust, or dependent types, or some formal verification layer we haven't built yet, the compiler knowing more than it currently does seems like the right direction. What remains genuinely open is which path gets us there.

---

Dev Kapoor covers open source software, developer communities, and the politics of code for Buzzrag.