Rust NYC

Join us on Tuesday, April 21 at Datadog Times Square. Doors open at 6:30 p.m. to give attendees plenty of time to grab pizza and socialize, and the talk begin at 7:15 p.m. Following the success of the UnConf we've absorbed all of your feedback and have two awesome speakers!

Tynan Daly – CEO at High Dimensional Research
Verifying Your Rust, Formally.

Tynan Daly studied mathematics at Bates College with a focus in algebraic topology before spending a decade in ML research, where he productionalized one of the first transformer models in 2018 for dynamic pricing. He is the founder of High Dimensional Research, where he builds formal verification tools for coding agents, translating Rust into Lean specifications for correctness proofs. As coding agents write more of our software, Tynan believes the tooling to verify that software needs to keep pace. He brings a mathematician's instinct for rigor to the practical problem of trusting code at scale.

As coding agents produce more of the code we ship, the volume is outpacing what review alone can catch but in systems where failure matters, "trust but don't verify" isn't an option. This talk explores how formal verification can close that gap. Tynan will introduce Lean as a proof assistant and explain why, despite its power, rewriting your Rust codebase in Lean isn't the answer. Instead, he'll walk through how tools like Hermes and Aeneas bridge the two languages, letting you write Rust and verify it against Lean specifications. He'll demo what this looks like in practice and make the case that formal verification is the same bet Rust developers already made with memory safety: accepting upfront rigor to eliminate entire classes of bugs before your code ever runs.

Bob McNaughton – Director of Engineering at UBS
Use a Rust SAT Solver to play pickleball!

Bob's career began last century, writing C++ and assembler for what was then Australia's only telecom company. Somehow, he ended up writing Go for financial companies in New York. He also managed to pick up degrees from Universities on both continents. He is not sure what the next step will be, but it looks like it will involve Rust. His self assessed USA Pickleball Association skill rating is probably somewhere around 2.5.

Many years ago, when I was an undergraduate CS student, my professor informed me that the Boolean Satisfiability problem was NP-Complete. I took this to mean it was not something I should waste any time thinking about or expect to be a useful tool in the future. Then, many years later, I was attending a Meetup involving some live coding, and the presenter casually imported a SAT solver library, fed it some boolean variables and conditions, and out popped a solution! Then, several weeks later at a Rust meetup, a different presenter equally casually imported a CSP library, and used it to solve a challenging scheduling problem.