> Starlark is intended to be simple. There are no user-defined types, no inheritance, no reflection, no exceptions, no explicit memory management. Execution is finite. The language does not allow recursion or unbounded loops.
That has some pretty useful properties for a config language that I'm not sure TypeScript helps much on. That said, Lean also has these properties too as an alternate language with good IDE support, and it would be pretty fun to write proofs of your build scripts.
> AMA is not the main culprit in supply of doctor's, that would be available spots for residents
The AMA has actively lobbied to lower the number of residency spots.
> In 1997, the AMA lobbied Congress to restrict the number of doctors that could be trained in the United States, claiming that, "The United States is on the verge of a serious oversupply of physicians."[12] The AMA successfully lobbied Congress to cap how much Medicare could reimburse hospitals for resident physicians
It was not my intention to defend the AMA, and organization I generally don't like (though I don't think they are villainous either).
I will note that you're referencing 30-year old legislation, which I don't think necessarily speaks to the AMA's role or position now. The AMA is not de facto against increasing slots. Please refer to this position from the president of the AMA penned last year: https://www.ama-assn.org/about/leadership/more-medicare-supp.... They have consistently asked members to support legislation increasing funding for GME positions.
But ultimately, their opinion is just that. Advanced medical education required congress to act, and expanding availability of trained professionals requires either:
1) Increasing slots for advanced training one way or the other, which will almost necessarily carry increased costs or
2) Allowing more US-trained immigrants to stay in the US after their education or
3) Creating an easier pathway for trained foreign doctors to practice in the US
Do you think there's ANY chance of #2 or #3 happening? In 2021 Congress funded 1000 new positions, the first expansion since 1997. They added 200 more spots in 2023. I imagine we'll be waiting awhile for the next expansion that the AMA actively desires.
It's not just that they didn't care, but they had a better framing and RLHF helped quite a bit. Galactica got released at a similar time to ChatGPT and got castigated, in a large part due to a poor framing of it being for science and not more of a fun thing.
Yeah, high bandwidth requirements still remaining. Over the past year, more research has looked from fully async to restrained cases that allow for geographically distributed compute. Async Local-SGD goes for a more standard training objective comparable with a lockstep training, https://arxiv.org/abs/2401.09135. imo technique is looking better.
This approach likely scales to top models. There was a thought for a while among researchers that scaling up Hogwild / LocalSGD to more parameters would be less convergent, but it seems to be that things actually converge a bit better with larger models, especially if a MoE split is used.
The intuition is that smaller models are figuring out things like grammar where the whole model comes into play, but larger models, especially in the back half of training, have localized knowledge updates that can merge easier in the AllReduce
Adding in a 100k iteration or so busyloop to the beginning of the food segment should do the trick and only add a few bytes. You could do something fancy with the clock interrupt, which is a bit more portable and stable, but might cost a few more bytes.
You can model types as a set and sets as types in many ways, so a number of the basic set theory axioms are pretty simple to express as lemmas from type axioms. IIRC you get constructive set theory easy, but do have to define additional axioms typically for ZFC.
I recall that you really need the "C" from ZFC or you'll end-up with a much less comfy realm of mathematics.
So the "C" from ZFC is "challenging" for type theory? Because, and I think I am not that much overshooting, fundamental axioms are really, really simple, even the "C" from ZFC, and if is "challenging" to express it using some fundamental theory, well, not good omens for that theory, or they can rebuild the realm of classic maths with their own "C"??
The axiom of choice entails the law of excluded middle, i.e. it takes you out of constructive mathematics. Mathematicians seem to really like the extended world of ZFC.
I expect there's an equivalent addition to constructive type theory that yields non-constructive type theory. Adding more axioms isn't necessarily making systems better though.
