← Feed

Posts

• Post #2334009

  I generally subscribe to a loose version of Penelope Maddy’s notion of mathematical naturalism on philosophical questions in mathematics. If someone wants to debate whether 0 is a natural number or flavours of finitism, but they don’t have any connection with mathematical practices (new or old), then it has no cash value, and I have no interest in discussing it

• Post #1135067

  Wrote a post on Kripke and Beth semantics in lean 4, and added some features to my blog so that you can see the proof state on hover: https://boarders.github.io/posts/beth.html

• Post #1125797

  IEEE Has a Pseudoscience Problem: http://deevybee.blogspot.com/2025/02/ieee-has-pseudoscience-problem.html

• Post #801937

  If anyone is interested in joining a cat theory reading group in NYC: https://bsky.app/profile/kirancodes.me/post/3mcsk7skqfs2n

• Post #801936

  @krismicinski@types.pl the end point of the academy as exclusively free (read: very expensive) job training is that eventually the important decisions are all made by bean counters

• Post #801935

  finished up an old post I had on well-founded relations and induction principles in agda: https://boarders.github.io/posts/well_founded_induction.html

• Post #713466

  wrote a blog post, mostly to try to get back in the habit of public writing and to resurrect my blog. It uses agda-categories to give show semantics for STLC in a CCC. The very end has a few things that I will return to finish, but wanted to his publish in any case: https://boarders.github.io/posts/stlc-semantics.html [apologies for the bad taste and quite hacky agda syntax highlighting, it is on my TODO list to do something better]