Nathan Taylor

thank’s

Man this post took forever to get out the door but I think I have cornered the market on “formal modelling of pre-i386 memory addressing in Lean” blog posts https://ntaylor.ca/posts/lean-ltl-6/

Boy I’d be embarrassed to have graduated from this department if I’d managed to graduate from this department

new blog series: get in, losers, we're doing reactive programming and temporal logic in lean https://ntaylor.ca/posts/lean-ltl/

(draft, feedback welcome!)

And it's done! I did not expect to write *checks `grep | xargs wc -w` 28,000 words about dependently-typed Fizzbuzz, but here we go. Time to find a more interesting thing to work on in the evenings (debating between doing some Alive-style translation validation in Dafny and embedding LTL in Lean...)

The whole series: https://ntaylor.ca/posts/proving-the-coding-interview-lean/

New blog post: finally got to the point where I can write the words "curry-howard", please clap https://ntaylor.ca/posts/lean-ltl-4/

Seattle folks: anyone else going up to UW for Mike Dodd’s DLS talk this afternoon?

New blog post: good gravy we finally made it to LTL - God this one took FOREVER to write and I still haven't gotten to FRP yet https://ntaylor.ca/posts/lean-ltl-3/

Wild that Jane Street’s new formal methods team is calling out refinement types as something they want experience with- anybody know if there’s someone in particular driving that?