Inside the V8 Sandbox Notes on V8's sandbox threat model, attack boundary, and the browser code that still has to treat sandbox data carefully. Learning Lean as a Programmer Learning Lean from the perspective of a programmer: types as propositions, proofs as programs, and raw induction machinery. Bitcoin From the Top Down Languages: EN / ZH A top-down walkthrough of Bitcoin's data model, from peer-to-peer state to transactions, UTXOs, and script validation.