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.
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.
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 programming language. It inspired me to learn some type theory and made me interested in mathematical logic more generally.
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'll make posts addressing later. Maybe it's because he has a bigger blog or maybe it's something else but blog comments are capable of adding a lot of value.
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 like you can with, say Haskell and category theory. This is because the stuff that makes HoTT so cool cannot be separated from it's mathematical foundations. How would you explain truncated types without going fairly deep into the math? Or the circle type? Sure both of these could be explained as instances of higher inductive types but that explanation is missing a lot.
Curious how approachable you think homotopy type theory is to people who think they know better than researchers? Simple type systems would be understandable (Haskell has type systems similar to System F and rust has an affine your system) but if anything being a programmer may add obstacles to understand HoTT since programmers (generally) have never had the opportunity to learn topology or anything else that HoTT builds on. Also not everything in HoTT has a clear computational interpretation, notably the univalence axiom.
That said I encourage everyone who's interested to investigate this but I don't think it's realistic without having a solid foundation in mathematics.
(And I also agree with the sibling comment that HoTT isn't really used as a foundation of mathematics.)
[1] Is what (I believe) they were talking about. Rather than configuring these in a sane way you just scan configuration barcodes. I didn't see anything on the list that was too dangerous but you could change the maximum input length or allow full ASCII encoding which could be dangerous if the programmers assumed that the barcode reader returns a fixed length string of numbers.
I would assume that it manages it the same way every other impure functional language manages side effects. I assume common lisp would be quite similar to ML, Ocaml, and Scheme in the way it manages side effects. Those languages don't make side effects part of their type system and more or less leave it up to the programmer to not make mistakes. Note that I've never done anything of significance in common lisp so this is just a best guess.
Have you considered nix os? I personally don't use it but I think it could fulfill your needs. You could have a work user with the home directory encrypted and a seperate personal user. Then you can install packages in a user independent way and you won't have any cross over between your users.
Sorry but you cannot implement this in a day. I've written my own language very similar to this and from my experience it takes way longer. Implementing type checking for just lambdas, pi types, universes, unit, and absurd would take a day or two on it's own. Not to mention Sigma types, co-product types, w-types, identity types, natural numbers, and lists. You also have type inference and evaluation. Also the time spent coming to grips with what all of this means. It's a really cool project but I expect it would take a week minimum to implement this and have a solid understanding of everything you've done.
The text to speech goes through speech dispatcher which by default probably uses espeak. I believe there are better text to speech engines like festival which you should be able to have speech dispatcher use quite easily but I've never tried this.
In terms of relying on tested and supported infrastructure lots of these projects use llvm.