PL
Verifying Constant-time
Ways to verify constant-time. Intro Constant-time is an important property of cryptographic implementations, and it plays a crucial role in defending against side-channels. Especially in this … Read more →
SMT/SAT: From Zero to 0.1
I’ve recently been learning about SMT/SAT solvers. Here’s a brief summary. Concepts SMT: Satisfiability Modulo Theories; wiki SAT: (Boolean) Satisfiability; wiki SMT can be viewed as a … Read more →
Symbols and Interpretation
After nearly a month of being tortured by Coq, I have finally, finally finished Logic Foundations. As the lead title of the Software Foundations series, it really is something. Here I just want to … Read more →
Hacking Together a Compiler from Scratch
This year I got an itch and signed up for an Implementation of PL course, where you build a compiler with your bare hands. I’m jotting down the process here. Honestly, this might be one of the … Read more →
Dark Magic in Computing — Rust Pitfalls
As I once said: My life is a lifelong battle with the Rust compiler. —Me And also: When you think Rust has a problem, it’s not because Rust has a problem— it’s because you have a problem. … Read more →
Rust Study Notes
I recently got into Rust out of nowhere because its little crab mascot is adorable, so I started reading The Rust PL to see what all the fuss is about. Turns out Rust is a genuinely sane, pleasant … Read more →
Programming Language Review
Review what I learned from programming language, a fundamental course of CS. The code is mainly in typed racket, a dialect of scheme. The code here is mainly from Weixi Ma’s lecture notes and my … Read more →