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.
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.
Others have handled the appropriate construction of irrational numbers. The claim here is not that every student needs to know irrational numbers are a limiting sequence but this is exactly how mathematicians think of it. So it is strange to hear another mathematician claim that repeated addition is somehow lying. At some point, people kind of just accept that it is just something you punch into your calculator and don't even think about it anymore.
Your example is quite bad because sqrt(2)*sqrt(2) = sqrt(2*2) = sqrt(4) = 2. So repeated addition works fine. Let's focus instead on pi*pi. The way calculators do this is precisely as some type of limiting sequence depending on how much precision you want. Because, one cannot "calculate" pi*pi exactly because it is irrational. So, you have 3*3, then 3.1*3.1, then 3.14*3.14, etc. which are all repeated additions with some division (e.g. 314*314/(100*100)). In reality, when multiplying two irrational numbers, we just use enough decimal points for floating point precision and then chop off any potentially erroneous digits after the multiplication.*
Irrational numbers are limits of sequences of rational numbers.
Multiplying two real numbers is simply taking the limit of a sequence of multiplications between rational numbers that converge to the two real ones.
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.
Multiplication outside of positive integers is not "repeated addition".
It took us thousands of years to properly define real numbers. High school students can live without a perfect explanation, or we can just teach limits before college since they are the fundamental concept if calculus.
Multiplication is repeated additions is the informal way of stating the distributive property of multiplication and addition.
Probably you were taught how to multiply irrational by the property of powers (a^b * c^b = (a*c)^b etc.).
You were not taught a grand unifying theory of multiplication, you were taught how to manipulate operations to turn them into more useful operations.
Teaching these laws also prepares you for when a and b are just symbolic reals with no structure and those laws are the only thing you can use to manipulate them.
You don't need a rigorous notion of limits to informally notice that irrationals have arbitrarily close rational approximations, e.g. by adding successive digits.
It's a kind of generalization of repeated addition. Once you've been taught about π, you know that 2π lies between 23 and 24, without being told about limits. It may not be rigorous, but it's a good start.
You can't teach "the truth" (whatever you hold that to be). It would set back education instead of advancing it. In this case too, perfect is the enemy of good.
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.
> In general you can't prove a program will or won't terminate.
As a point of clarity for folks who come to this (the commenter clearly knows this) one can’t _automatically_ prove for an arbitrary program whether or not it terminates. It’s definitely possible to prove this manually per program and most dependently typed languages will do the work for you as a matter of sound over approximation as long as one of the arguments is shrinking in an obvious way.
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.
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.)
I don't think it's an easy journey—not because the material is intrinsically difficult, but because almost all resources are written for mathematicians and computer scientists. I think a "homotopy type theory for programmers" book/blog/playlist could be a big hit. I've been considering putting something like that together.
I view the relationship between HoTT and topology as similar to that of functional programming and category theory: you don't need to know the latter to learn the former, but having that extra background can certainly help.
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.
As already has been done with category theory, you need to target a specific audience, whether it is programmers, scientists, engineers, or mathematicians, and illustrate the concepts by giving examples from their area of expertise, if possible.
[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.
Bingo. The better ones will only accept scantags if you scan the "enter config mode" within 30 seconds after power-on, for instance. Or yes, a hidden button on the underside of the checklane.
That's rare though, and sometimes the installer disables it for convenience while they're debugging the system and never re-enables it. So the vast majority of scanners in the wild will happily accept an enter-config-mode at any time.
I personally do. A "just works" configuration will be ideal for me. Anytime I install linux on a new computer, I find myself spending too much time tinkering with configuration settings to make basic things like adjusting keyboard brightness and volume control work with the respective keys.
You don't have to do any of that with a Framework and Ubunut/Pop. The only real thing to adjust was getting the fingerprint sensor working, which really was copy/pasting a script. Everything else worked perfectly out of the box.
You can fix the battery drain issue by changing one line in a config file. The issue is from how Intel chips handle hibernation w/ Linux, so not a Framework specific issue though.
I don't, and I suspect that people who would want Linux preinstalled don't have much experience in it, and being lost would hate it, badmouth it, and badmouth the company for making it an option. Installing Linux is quick and of trivial difficulty, and if you're afraid to do it you should probably work on that fear at a different time than when you're also breaking in a new computer.
I would say that installing Linux is like being able to tune your guitar or a chef being able to sharpen their knives, but it's an order of magnitude easier than either of those things.
Agree with sibling that maintaining preinstalled Linux is a good sign that all the guts and peripherals are compatible, although that might be a perverse incentive to use a bleeding edge kernel/distro to accommodate flashy hardware. If anything, they should install a boring LTS/Debian Stable, completely stock other than a custom wallpaper.
I want to know that the hardware will work with linux, and will continue to work with linux.
A pre-install option is just one way to advertise and convince the user that you've tested the hardware to work on linux
Yes. The linux market is extremely diverse. The sheer amount of distros and DEs is pretty good evidence of this. It doesn't even have to be different people.
For personal laptops/desktop I don't care if it's preinstalled for me or not since the very first boot is going straight into my usb installer since it's extremely unlikely that they checked all the boxes I will check (especially getting my LUKS passphrase correct!!). But for my wife or parent's laptop that's exactly what I want. If dad runs linux I can help him out a ton more, even SSHing into his machine to set things up or install updates, etc, but I'd prefer he be able to turn the thing on and connect it to his wifi and start using it without me having to be there.
In terms of relying on tested and supported infrastructure lots of these projects use llvm.