People keep asking me what the "Rust for hardware design" would look like. Those who know their PL history know that, before we could build Rust, we had to define ideas like "Memory Safety".

A hopefully uncontroversial take is that Memory safety defines a class of *logical errors* that pointer-manipulating programs suffer from. By defining this category, we were able to create dynamic and static mechanisms to eliminate it.

Building a "Rust for hardware design" requires the same so I spent the weekend writing a 2-page paper defining a criteria for "safe hardware description languages (HDLs)". Instead of competing with heavyweight formal tools, safe HDLs should complement them by eliminating a category of bugs that exist in *all hardware designs* and let the formal tools focus on design-specific properties.

Would love to hear what people think: https://people.csail.mit.edu/rachit/files/pubs/safe-hdls.pdf

Hardware design should be SAFER!

Memory-safe software languages changed the world and allowed to us to build massively larger systems. At their heart, memory-safe languages eliminate a category of bugs that pointer-manipulating programs suffer from.

Hardware design needs its own safe programming models but instead of memory, the problem is time! Synchronous hardware design needs to deal with a clock signal which creates discrete time steps. Every hardware module needs to think about how time affects its own logic and everything it communicates with. Getting it wrong leads to all sorts of logical bugs: reading meaningless values and using resources that are unavailable.

Our work on Filament (https://filamentHDL.com) defined a criteria for safe hardware description languages (HDLs) and showed that you can enforce it using a type system and introduce no overheads. Safe HDLs have become an interesting area of research and this year's ASPLOS features two papers exploring different threads:

- Lilac (https://arxiv.org/abs/2401.02570): Builds upon Filament applies its safety guarantees to parameterized designs. A cool outcome of this work was to show that, in addition to helping with verification, safe HDLs enable the design of fundamentally new abstractions!
- Anvil (https://arxiv.org/abs/2503.19447): Explores how Filament's verification abstractions can be applied to a higher-level, message-passing HDL and enforce safety properties!

I'm really excited to see where this line of work goes and what we can build with it! If you're around at ASPLOS and interested in this kind of work, come say hi and go watch the talks!!

do people have favorite readings that motivate different styles of formal semantics?

i find it easy to motivate operational semantics to non-experts ("it's just an interpreter!") but motivating denotational and axiomatic are less obvious.

I have a long-running beef with the word "transpiler" so I wrote another post trying to (1) formalize the various definitions of "transpiler" people give me, and (2) describing why they don't work (for me): https://people.csail.mit.edu/rachit/post/transpiler-formal/

(My real purpose is to get people to read the linked Felleisen paper which is one of my all time favorite papers)

Becoming an advisor is learning to value all of the awesome teaching resources your colleagues make!

I cannot imagine what I would do if large swathes of PL and Compiler course curricula were not open-source!