New comment by kite42 in "Developing provably correct Rust code with Verus"

kite42 — Thu, 17 Sep 2026 03:37:23 +0000

All it does is dispatch proof obligations to an SMT solver like Z3. There is nothing special about Verus, it works in the same way other program verification frameworks like Dafny and Frama-C work - except it's for Rust. Most of this article presents nothing unique to Verus and is more of an advertisement for the authors research work and the other work AWS is doing.

New comment by kite42 in "Bits of Advice for 30 Years"

kite42 — Fri, 17 Nov 2023 16:39:52 +0000

Some of this stuff isn't really insightful.

> It’s only awkward if you make it awkward.

Or THEY make it awkward.

> Don’t make your problems other people’s problems.

Well, yea... Also don't attack other people, and don't steal from other people, ...

> Help others succeed, and they’ll help you succeed in the long term.

Hard no. Many will take advantage of your time and advice, and never return the favor. Choose wisely who you help succeed.

> Don’t let your expenses rise as fast as your income.

Once again, very generic. Don't spend more than you make.

On the other hand, some of this stuff is actually never mentioned but useful

> Keep a brag document

> Under-promise and over-deliver.

Hacker News: kite42

New comment by kite42 in "Developing provably correct Rust code with Verus"

New comment by kite42 in "Bits of Advice for 30 Years"