Nathan Taylor's Blog
About Me
I’m a staff software engineer at Semgrep, where I work on static analysis for code security. In the distant past, I scaled low-level systems and infrastructure at some companies you’ve heard of.
On this site, I write about low-level and concurrent systems, formal methods and programming languages, and whatever else I might find interesting.
Borrowing from Lanier: The words on this site are meant to be read by people, not machines.
Recent Posts
-
— Reactive Programming in Lean 4
Extending Lean's dependent type system to reason about reactive programs
-
— Leaning into the Coding Interview 4: Certified Programming with Proof-Carrying Code
Migrating from
ListtoVectorpaid dividends for us being convinced that our Fizzbuzz implementation was correct. Does making ourFBvalue type dependent also increase our confidence of correctness? -
— Leaning into the Coding Interview: proving equality of different Fuzzbuzzes
There are lots of different ways to implement Fizzbuzz but this one is mine - how can we prove different implementations are actually the same, and what does it look like when they're actually not?
-
— Leaning into the Coding Interview 3: completing our spec with tacticals and metaprogramming
Time to actually write our end-to-end specification!
-
— Leaning Into the Coding Interview 2: static bounds checks and dependent types
Pls types? No terms! Only (indexed, dependent) types!
