The goals and some of the syntax here remind me of Haskell, a lovely little language I've not had a chance to use practically outside of academia, that is nearly impossible to make mistakes with. Personally my background is primarily in microprocessor design, semiconductor physics, and close-to-the metal programming so these extremely abstract languages are long way off my formal educational background(Besides the pure mathematics that underpins it all) but since I've been programming for around a decade now long before formal education and kinda nailed it qualification wise imo(Top percentile of grades in Britain woo, basically got me my position at uni given I was raised in poverty) before I went to uni I've always loved the abstract programming side of things as a way of getting my more pure mathematically minded friends to enjoy the same stuff as me as a kid(These friends are now physicists so far far smarter than me lol). Though nowadays I have to use a lot C#(Very similar and using the same framework as VB.net taught in most British high schools), far more abstract and simple than even C++ but amazingly useful for modern user application development and probably my third most used language after C (Since everyone wants to control their microcontrollers with their smartphones nowadays) so I still have to dabble in OOP despite of course having to customarily consider it heretical abstraction coming from my background, to p off all my lowly software """engineer""" friends

.
For work atm I do more programming in close to the metal languages(Assembly languages & ANSI C are my bread and butter) than the more abstract OOP types since I do most of my work on hardware(Although they're easier to work with a language as abstract as C++ becomes abit useless with low resource realtime embedded systems, you lose the 1:1 correlation between its compiled assembly/machine code and have to trust the memory management system).
Traditional programmers often view loops as a fundamental part of programming(Almost true, recursion is truly fundamental), but anyone with more of a background in the mathematics side of things will often find they're essentially used to mimic vector operations most of the time, and many languages like this or Haskell has made strides by throwing out the old hardware derived programming paradigms and moving to more abstract mathematical ones which have of course been perfected by nature and thousands of years of academia(As I'm sure you can guess Al-gebra and Al-gorithms are concepts derived from Muslim academia).
If you've ever wondered what a loop looks like in Assembly, basically any type will translate to a branch statement like GOTO/JUMP, which without a good predictor that means you're likely to have to flush the processors pipeline, stack & cache which of course incurs significant performance penalties. This means basically, if you want to optimise code for simple low resource hardware, you have to start unrolling loops(Which has the adverse affect of increasing memory size) and get deep into the analysis of which ones do what on a hardware level to avoid pipeline bubbles(Modern compilers for abstract languages will often unroll loops automatically).
Loop invariants are a lovely little trick you can use for all sorts of tasks, but ultimately these kinds of tricks are a perfect example of something that's almost too abstract for humans to use reliably, these are exactly the kind of things we should avoid in future abstract languages(I'll leave mutable states and reference equality to someone more into the OOP side of things incase I leave out something important if you want someone to go into those since I've already ranted too much sry).
Basically, this whole thing is about creating a language where you can look at a line and see what it does, without having to know whether a random variable 1000 lines down might affect it, while removing these unnecessary abstract concepts that are particularly error prone once thrust into the hands of humans is the key to these new wave programming languages.
I don't think they're necessary for teaching stuff to kids, I'm sure many can grasp Python or VB just fine, but the things you learn with traditional languages could easily be considered useless with the modern shift of paradigms towards unbreakable code, so personally I think this more academia routed approach is far better for pedagogic programming.