Viewing profile — isaac21259

I was considering this for my programming language but I will most likely not use it because it makes optimisations and garbage collection harder, and the C would not be human read…

Exponentials come up quite naturally from differential equations because it's often suprisingly useful to talk about something's rate of change in terms of itself. As far as I know…

To clarify where I live limits are introduced in high school, irrational numbers just much earlier.

That's a pretty far departure from the original "multiplication is just repeated addition". Regardless, I don't think any student would find it helpful to hear "Multiplying two rea…

What about irrational numbers? There's no neat way to view multiplication of two irrational numbers as repeated addition. And even if there were a way I don't think it's a useful w…

Dependent type systems don't deal well with non termination. In general you can't prove a program will or won't terminate. The solution is to disallow recursion except through a fe…

The Little Typer by Daniel P. Friedman and David Thrane Christianse. It's basically one long book of examples building on each other to show the semantics of a dependently typed pr…

Se also: https://tech-blog.capital-match.com/posts/5-the-reverse-stat...

Everyone here has been talking about how blog comments add little value. On many blogs they are right. But John D Cook's blog regularly has interesting comments, some of which he'l…

I was also considering writing some introductory stuff about HoTT but I don't think it's possible to avoid talking about topology, homotopy theory, and category theory in depth lik…