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 readable (just look at the output of the chicken compiler for an example) so there's not a huge benefit. C-- could be an option but it isn't very active or well used.

In terms of relying on tested and supported infrastructure lots of these projects use llvm.

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 there's no similar connection with tetration.

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 real numbers is simply taking the limit of a sequence of multiplications between rational numbers that converge to the two real ones". In my country irrational numbers are introduced two or three years before limits so you couldn't teach it in schools effectively either.

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 way to think or teach after the first couple years because it makes obvious things like √2×√2 = 2 seem weird and mysterious.

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 few eliminators which do recursion in a well founded way that is guaranteed to halt.

The reason they don't work well with recursion is you could have something like: false :: _|_ false = false

Where false is a function we are defining of the uninhabited type.

For more complicated versions stuff like this see Girard's paradox.