I came across the following YouTube video a while back which uses a strange trick to accurately approximate square roots. I suggest watching at least the first minute where the presenter explains how it’s done:

Let’s do an example. Approximate to 2 decimal places: 

First, YouTube tells us to find the nearest perfect square that’s less than 40, that’s 36, and take the root, giving us 6. So our answer is, obviously, 6 point something. That something is a fraction, where the numerator is the difference between 40 and 36, and the denominator is 2 times 6. So we have:

So what’s the actual answer to 2 decimals? It’s 6.32. That’s what I like to call: pretty darn close. Naturally, there are a few catches to this technique: you need to know your perfect squares, you need to know your fractions, and things tend to get hard with larger numbers.

But still, I thought this was surprisingly effective for such a simple piece of arcane trickery.…

Hello Internet. In this blog post we are going to learn some type theory, which is a field that lies in the intersection of mathematics and computer science. We are eventually going to learn the variant called Martin-Loef Type Theory, or MLTT for short. To motivate it, we are going to try answering the question, “What is a valid program?”

Not every program makes sense, for example what would a program consisting of the single expression x + 2 mean? If we don’t know what x is, then we don’t know what the meaning of that expression is. More importantly, a program can combine expressions that are incompatible with each other. For example, if + is the usual operation that adds two numbers then an expression like "abc" + 5 can’t be given a meaning. To avoid such meaningless programs, we should talk about the different kinds of data and the valid operations on these pieces of data.…