Even if open source operating systems comply and add such a feature, what's to stop individual people from removing this and blocking the API requests before they install the OS? Or providing dummy responses? They're open source, after all.
Is the government going to require some sort of automated checks that verify every person who connects to the internet has this API on their OS and go after individuals that aren't in compliance?
I thought William Dunham's Journey through Genius: The Great Theorems of Mathematics did a great job of presenting the very real people and world behind several of results from history, from 400 BC (Hippocrates' Quadrature of the Lune) to recent-ish times (Cantor's transfinites).
There's discussions of feuds between mathematicians, how they used to keep results secret and literally duel over ideas (e.g. Cardano's chapter), the historical context and lives of the people who brought theorems into being (like Newton tasting his own chemicals as part of his alchemical research!), etc.
SuccessorML[1], 1ML[2], etc. are pretty close to this in spirit. I've been trying to keep up with the publications around the future of ML, but academic research moves kinda slowly. I'm hopeful we'll see a new definition of Standard ML this decade. I'd tend to agree SML is a great choice -- SML-1997 is still ahead of many languages that came well after it in both features and usability.
Journey through Genius: The Great Theorems of Mathematics - William Dunham
How to Bake Pi - Eugenia Chang
These are all sort of 'pop-math' books -- that is, they're more intended to spark a joy & love for math than teach rigorous mathematics. Great Theorems and A History of Pi include a lot of history (edit to add: in addition to covering the math involved!) -- did you know some mathematicians in history would duel over their theorems? That theorems were a carefully guarded secret instead of something you shared?
Introduction to Graph Theory is specifically intended as an introduction to mathematics for 'the mathematically traumatized'.
In my opinion, after reading these, if you've sparked a joy for the puzzles and fun of mathematics, then I would then suggest branching out into more formal presentations of them relevant to your interests... it's much easier to slog through a book on abstract mathematics when you receive from enjoyment from the puzzles presented.
I think it goes back to the neverending quest to find ways of representing computation that allows of ease of composition, changing implementation details, eliminating classes of errors by construction, etc. Monads have had some success in this arena, but they have notable issues with composition; monad transformers help, but can become unwieldy in their own ways.
An alternative are effects, hypothetically allowing for ease in building programs as separate but composeable components which can then be freely mixed in or swapped out. In practice I have found working with effect systems in Haskell via libraries stresses the type system so much you end up with scoped type variables and type applications everywhere. My understanding is that the theory behind using effects to structure computations comes from category theory's Lawvere theories (see e.g. Pretnar's 2010 dissertation on https://github.com/yallop/effects-bibliography). Lawvere theories give rise to many monads (see Bartosz Milewski's article on it -- https://bartoszmilewski.com/2017/08/26/lawvere-theories/), but with nicer compositional properties.
This is where languages like Effekt, Eff, Frank, and Koka come in -- by writing the entire language and type system to support the theories, a lot of the pain of expressing it in Haskell can be avoided.
So I would say this echoes my experience with it so far -- it is definitely a work in progress! However, I tend to approach Koka as if it were Standard ML with an effect system (up to a point), so the lack of a full imperative API hasn't been felt too much. I am more missing ad-hoc polymorphism than imperative tooling.
I am not sure I understand your comment about mut variables; my understanding is there are two types of mutable variables in Koka -- 'local' and 'ref'. 'local' is a locally mutable variable, and 'refs' are globally shareable. A 'ref' can be shared between functions, 'local' is just to give an imperative API using mutable variables. How 'local' works kind of confuses me so I tend to avoid it altogether in favour of local names (i.e. 'val' rather than 'var') and tail recursion (instead of loops with mutation). 'ref' seems quite usable to me and seems to reflect the SML usage of it.
I have felt the pain of a lack of an array, but I ported over an Okasaki data structure which has served well for a random-update, sequential data structure. Their data structures in the stdlib just have comments that say 'TODO': https://github.com/koka-lang/koka/blob/master/lib/std/data/m... that I am hoping are open to pull requests.
> Edit: Can someone tell me... Is it necessary to have a new type system or could this be done with dependent types?
I played around with trying to implement an effect library (via the research) in dependently typed languages (Idris, Agda) and found type inference issues to be too much to work around. I found I was having to help the type checker along at every step -- explicit signatures on everything and, in Haskell terms, type/proof applications on function calls. On the other hand, I have found Koka -- until I started pushing the type system to its limits -- to require no hand-holding to figure out how to type its set of effects.
I am curious if a dependently-typed wizard could figure out an encoding to make these issues go away, but it was beyond my capability.
How does this compare to other effect-oriented languages like Koka, Frank, and Eff?
I've been doing some work with Koka lately, but I briefly looked into the other three (including Effekt) and it mostly came down to, 'Koka seems most active in development'[1] and 'Koka had the easiest to use documentation for me'[2], which are both kind of subjective ways of choosing between them rather than an objective comparison.
Is the government going to require some sort of automated checks that verify every person who connects to the internet has this API on their OS and go after individuals that aren't in compliance?