U+23BE..U+23CC DENTISTRY NOTATION SYMBOLS

The Unicode Standard has its fair share of mysterious and sometimes unexplained characters. The story of the Farsi symbol (U+262B ☫ farsi symbol) is one of the more well-known ones. Many blocks, especially the “miscellaneous” blocks, have smatterings of rather arbitrary character sets grouped together only by history. One such block is Miscellaneous Technical, which contains completely unrelated groups of characters, including keyboard symbols, APL symbols, electrotechnical symbols, UI symbols, drafting symbols, and of particular interest in this blog post, dentistry notation symbols. Here they are, all 15 of them:

⎾⎿⏀⏁⏂⏃⏄⏅⏆⏇⏈⏉⏊⏋⏌

The first two and last two are part of Palmer notation for denoting human teeth by their position. What are the rest for?

Notes on W Types and Inductive Types

Notes on Untyped Conversion

Cedille Usage Notes

An Analysis of An Analysis of Girard's Paradox

While it’s rather difficult to accidentally prove an inconsistency in a well-meaning type theory that isn’t obviously inconsistent (have you ever unintentionally proven that a type corresponding to an ordinal is strictly larger than itself? I didn’t think so), it feels like it’s comparatively easy to add rather innocent features to your type theory that will suddenly make it inconsistent. And there are so many of them! And sometimes it’s the interaction among the features rather than the features themselves that produce inconsistencies.

It's not all it's cracked up to be

Friday, 22 October 2021, 10:30 am. Cold, rainy, wet. From inside Joyce–Collingwood station I spotted the R4, just as it was closing its back doors. My first mistake was hope: The front door was not yet closed. My second mistake was hubris: I will make it to the bus if I run. And so I ran, but my normally-grippy sneakers slipped on the sidewalk slick with rainwater, and I ended up landing hard on my ass right in front of the bus driver.

It was a miracle I ended up mostly physically unscathed. I instinctively shot out my arms underneath me and I could have broken a wrist or two. I could’ve landed on my tailbone wrong and broken that too. But it seemed the only damage was a light bruise on my sacrum (had to look up the word for that) and to my ego. Not even a scratch on my palms! Then I sat down, took out my laptop, opened it, and discovered the large crack from the bottom left corner, reaching longingly to conquer the entirety of the screen.

How to Use Sized Types?
Let Me Count the Ways

This post is inspired by this thread from the Agda mailing list.

Because Agda treats Size like a first-class type, there’s quite a bit of freedom in how you get to use it. This makes it a bit unclear where you should start: should Size be a parameter or an index in your type? What sizes should the constructors’ recursive arguments’ and return types have? Here are two options that are usually used (and one that doesn’t work.) The recommended one is using inflationary sized types and Size<.

The State of Sized Types

Sized types hold great potential as a very practically useful way to do type-based termination checking, but sufficiently expressive sized types in dependent type theory come with a host of problems, mostly related to its incompatibility with the infinite size found in most simpler or nondependent type systems. This post attempts to describe some potential but ultimately unsatisfying solutions.

Notes on Propositional Equality

Adding LaTeX to your Jekyll Site

As it turns out, adding support to render LaTeX in a Jekyll blog isn’t all that hard, because other people have done most of the heavy lifting. There are two main ways to do this:

• Client-side rendering: After the page loads, a JS script is run to transform LaTeXy parts of the page to lovely, styled HTML.
• Build-time rendering: After Markdown files are compiled to HTML, a Jekyll plugin further transforms those LaTeXy parts to HTML as well. Here’s how you do either using $\KaTeX$.

Tips on Developing Rocq

N.B. These notes date back to before the name change to Rocq.

The following is a grab bag of tips on developing Rocq itself, from writing plugins for it to modifying the trusted kernel.

Thulium: Disk Failure

On 24 December 2020, my home server Thulium went down. Usually the cause of downtime is my home’s public IP address changing, and I need to update the DDNS record with my domain name provider. This time it wasn’t; when I tried to SSH in through the domain, I reached something, but it wouldn’t let me in. I managed to SSH in through the local IP address and tried to reboot, but I got a segmentation fault, of all things. In the end, I rebooted the server manually by walking over to the other room and holding down the power button. I could then SSH in, my Docker containers were up, all was well.

On 27 December 2020, it happened all over again. This time, I could SSH in again, but everything was painfully slow. I checked htop: CPU and memory were doing fine. I checked my internet connection: that was fine too. It must be, then, a disk issue (obviously, since that’s the title of this post).