My first impressions from a few weeks with Lean and Coq

We should always be supporting each other, but it feels particularly important right now. An election just finished in the US, which means that half the country lost and has to face the coming changes. In particular, this is a scary time for many folks who have been targets in the past couple of years, with escalating legislation against access...

When pairing with my friend Emily, we had a choice of what to implement in her project: start a new feature, or add a command line argument parser? We opted for the latter, because it had to happen eventually and it was more well bounded. It ended up having a lot of depth! We wrote it from scratch to learn more, rather than pulling in a library1....

If you have a blog, you've probably gotten those emails that want to "collaborate" on a guest post—which often means "let us post sketchy links for SEO purposes." Recently, I got one which was a little different flavor than the usual spam, so I bit and replies. The end result was at the same time fascinating, unsurprising, and deeply...

My wife's alarm clock has been acting up lately. Sporadic at first but then every day, it wouldn't blare in the morning at the set time. Instead, when it was supposed to go off it would... reset itself. The time would start flashing in that "I'm confused because the power went out" sort of way. Not very useful. You want the alarm to wake you up,...

I was talking to a friend recently, and zie1 lamented that a Rust web framework uses YAML for its configuration. I'm far from one to defend YAML2, but dug in a little to understand zir issues with it: is it the trauma here, or is it something else? Ultimately, zie wanted something that I also seek in Rust: compile time errors over runtime errors....