Interesting take on enforcing state machine rules using a proof system. I'm interested in this space, and have been developing a new programming language to enable typestate / state-machine representation at the type system level[0].
I don't know where it will end up on the spectrum of systems languages; it may end up being too niche or incomplete, but so far I think I'm scratching the right itch, at least for myself.
I miss the days when "API" meant any programming interface - not just web/rpc - and good API design was about providing the right level of abstraction and making doing the right thing easy and the wrong thing hard, not just CRUD.
I figured that it would be something like that. But it's been so frequent that I expect the leadership to act decisively towards a long-term reliability plan. Unfortunately they have near monopoly in this space, so I guess there's not enough incentive to fix the situation.
How frequent? I think the obsession with uptime is annoying. If GitHub is down, if there’s something so critical, then you need some more control of the system. Otherwise take a couple hours and get a coffee or an early lunch.
Yeah that is pretty bad I guess. For decades 99% has been achievable for many orgs. 92% phew.
But “waste” is arguable. If folks have literally nothing to do when GitHub is down, I question that a bit. For example, design, administrative work (everyone has that), lunch. You know?
Critical CI/CD can use Jenkins, but in that case folks might end up with 89% uptime!
> If folks have literally nothing to do when GitHub is down, I question that a bit.
It's not about a single person. I work at a company with over 10k employees, most of them rely on GitHub one way or another. It's not just about PRs and issues; there's a huge amount of automation, workflows, and integrations that depend on GitHub, round the clock. With this kind of uptime it has material impact on productivity of the company as a whole.
I believe we (humankind) have been transitioning to a phase of what I call "time compression." Everything is happening too fast compared to say 40-50 years ago. You can attribute it to many things (tech in particular), but primarily it's the fact that everyone has a terminal in their hands where they can access information, people, news, etc. at a whim. It's affecting both our mental health and our collective social fabric. I think humans were not meant to be overwhelmed this way; our mental capacity hasn't increased, but the stimuli have increased by orders of magnitude.
I don't have a solution to this problem. But one thing I've been trying is to immerse myself in a hobby I enjoy, and ignore most of the noise around me. I closed most of my social network accounts 9 years ago, and it has improved my mental health significantly. I still read the news, but I skim the headlines and go back to what I was doing. Yes, it does affect me, but I try to minimize its impact and focus on things that compensate their effect.
There's no silver bullet. Just know that you're not alone. Unfortunately time compression is here to stay (and it will probably get worse), and those of us who fight it back will hopefully stay sane.
Several years ago we had a data processing framework that allowed teams to process data incrementally, since most datasets were in the range of terabytes/day. The drawback is that it's append-only; i.e. you can't update previously processed output; you can only append to it. One team had a pipeline that needed to update older records, and there was a long discussion of proposals and convoluted solutions. I took a look at the total size of the input dataset and it was in the range of a few gigabytes only. I dropped into the discussion and said "This dataset is only a few gigabytes, why don't you just read it in full and overwrite the output every time?" Suddenly the discussion went quiet for a minute, and someone said "That's brilliant!". They only needed to change a few lines of code to make it happen.
I'm no expert myself, but is this the same as Russell's type hierarchy theory? This is from a quick Google AI search answer:
Bertrand Russell developed type theory to avoid the paradoxes, like his own, that arose from naive set theory, which arose from the unrestricted use of predicates and collections. His solution, outlined in the 1908 article "Mathematical logic as based on the theory of types" and later expanded in Principia Mathematica (1910–1913), created a hierarchy of types to prevent self-referential paradoxes by ensuring that an entity could not be defined in terms of itself. He proposed a system where variables have specific types, and entities of a given type can only be built from entities of a lower type.
I don't know that much about PM but I from what I read I have the impression that for the purposes of paradox avoidance it is exactly the same mechanism but that PM in the end is quite different and the lowest universe of PM is much smaller than than that of practical type theories.
I don't know where it will end up on the spectrum of systems languages; it may end up being too niche or incomplete, but so far I think I'm scratching the right itch, at least for myself.
[0] https://github.com/khaledh/machina
reply