I have a somewhat off-topic question: I know there are very few sites that are actually doomsday-proof, but could this lab, being 2400 meters deep in the ground, survive a direct hit from a ICBM (e.g. LGM-30 Minuteman) with a megaton yield?
1,882 karma · joined December 8, 2017
If you compare that with other wealthy countries such as Germany, then you'll see that they have less land, fewer natural resources, haven't had democracy for as long, were divided until the late '80s, and do not have as large a population size.
Therefore, just by sheer numbers, it makes sense that everything in the US is bigger. Moreover, Germany, for instance, has a culture where wealth is accumulated across a large number of medium-sized companies, whereas in the US, wealth is increasingly concentrated at the top (for example, the ones you mentioned). These are, of course, the entities everyone knows and talks about.
I do agree, but that we don't do that in reality is exactly my point.
Abstract logical frameworks are not pulled from thin air. Human brains develop such frameworks with a physical brain that receives sensory input from a physical world, and hence there is a deep connection between the physical world and the abstract logical frameworks in many ways.
"The Last Question" by Isaac Asimov is a seminal science fiction short story that explores humanity's evolution and the quest to overcome entropy over trillions of years. It starts in 2061 with two technicians, Alexander Adell and Bertram Lupov, operating Multivac, a powerful computer. They discuss using solar energy and the finite nature of the sun, leading to the titular question: Can the increase in entropy in the universe be reversed?
The story jumps through various epochs, where different iterations of computers (Microvac, Galactic AC, Universal AC, and finally Cosmic AC) are repeatedly confronted with this question but always respond with "Insufficient data for a meaningful answer." Humanity evolves, colonizes the universe, achieves immortality, and ultimately merges with the Cosmic AC.
At the universe's end, when only the Cosmic AC exists and time, space, and matter cease to exist, the AC finally finds an answer to the question. The story concludes with the words: "LET THERE BE LIGHT! And there was light --" suggesting the cycle starts anew, possibly with a new universe. Asimov's tale is famed for its profound philosophical inquiry and visionary depiction of humanity's future and technology.
"With a budget of €7.5 billion, the LHC is one of the most expensive scientific instruments[1] ever built" - Wikipedia
Perhaps we should invest the next 7.5 billion in an exceptionally large GPT model.
Should you require greater than 99.95% uptime for particularly critical operations, then opting for a multi-region approach, such as using multi-region storage buckets, is advisable. It's also worth mentioning that I have never experienced a full 8 hours of downtime at once in a given year. It has usually been a case of increased error rates or heightened latency due to the inherent redundancy provided by availability zones within each region. Just make sure your network calls have a retry mechanism and you should be fine in almost all cases.
I came to the conclusion that when you factor everything in—the time it takes to maintain such a massive infrastructure operating smoothly across the globe, investment in the further development of cloud services, employing security experts, paying developers competitive salaries, and of course aiming for a profit margin for the company—you end up with the prices that are evident among the major cloud providers. It simply isn't feasible to offer these services for much less (there are a few exceptions people rightly complain about, such as stupidly high egress costs). It has reached a point where Google, for example, has attempted to undercut prices to such a degree that their cloud operations have been running at a loss in the past[^1].
[^1]: https://www.ciodive.com/news/google-cloud-revenue-Q2-2022/62... (read last paragraph)
I'm not suggesting that this isn't a viable solution, but I would prefer to be well-prepared and have a team of experts in their respective fields who are willing to have an on-call duty. This team would include a specialist for Longhorn or Ceph, since storage is extremely important, one to set up and maintain a high-availability PostgreSQL database with an operator and automated, thoroughly tested backups, and another for eBPF/Cilium networking complexities, which is also crucial because if your cluster network fails, it results in an immediate major outage.
Certainly, you can claim that you have sufficient experience to manage all these systems independently, but when do you plan to sleep if you're on call 24/7/365? Therefore, you either need a highly competent team of domain experts, which also incurs a significant cost, or you opt for cloud services where all of this management is taken care of for you. Of course, this service is already included in the price, hence it's more expensive than bare-metal.
This has profound implications, such as for the possibility of a theory of everything. This does not necessarily mean that a theory of everything is impossible, but it does indicate that such a theory might not be able to provide a complete description or prediction of all physical phenomena, which is contrary to the belief of some physicists.
It seems as though the program has been resumed lately.
At least not for state actors, or perhaps well-funded terrorist groups.
So, if only a segment of Haskell's language design is based on Category Theory (CT), and only a fraction of popular programming languages are based on Haskell, then this percentage, possibly in the single digits for a given mainstream language, is too minor for you to consider it a valid application of CT. That's a valid perspective; I'll leave it at that.
> Still, to your last point, the existence of an equivalence doesn't automatically count as an application of all sides of the equivalence. ... The practitioners have to adopt that framing or rely on theorems proved via the math ...
I really don't agree with your definition of application. If I have an equivalence between three different concepts - types, propositions, and objects within CCC, then, in my viewpoint, you don't need to explicitly consider your application of a concept in the other two fields for it to be recognized as an application. To me, that's akin to saying that you can only do math in a certain way, exactly how mathematicians portray it in their textbooks. If you don't know that because you learned math more indirectly, like from programming blogs with code snippets that encapsulate the same definitions, then, according to that view, you won't be doing applied math.
To me, it simply boils down to a different perspective on the term application, one that isn't specifically about CT.
> Automated theorem verification may use category theory (does it?), and I'd love to talk to the main contributors to Lean
I have listen to some podcasts with the main contributors and creators of Lean. Lean is based on (Lean's kernel) homotopy type theory (a flavor of type theory – specifically of intensional dependent type theory).
> most traction among average mathematicians
Yes. Many math graduate students are using Lean to apply concepts from textbook math, such as HoTT, which has a strong connection to Category Theory. Basically, you can't read the HoTT book without knowing CT, and can then apply it in Lean. I think this would even satisfy your definition of applied math.
Since you've mentioned it, one of the inventors of type families is Simon Peyton Jones. He is quite renowned within the Haskell community as he is also a significant contributor to the design of the Haskell language. Now, let's examine what he has to say about Category Theory.
> "I say “surprising” because anything with as exotic a name as “monad” — derived from category theory, one of the most abstract branches of mathematics — is unlikely to be very useful to red-blooded programmers. But one of the joys of functional programming is the way in which apparently exotic theory can have a direct and practical application, and the monadic story is a good example."
https://gist.github.com/dtchepak/3163428
In his own words, "apparently exotic theory [Category Theory] can have a direct and practical application," indicating that you hold a differing view from Simon, fair enough, however I believe that few people on this planet have a deeper understanding of Haskell than he does, which is why I hold his opinion in high regard.
So, what about the other major language designers of Haskell?
Firstly, there's Philip Wadler. For a clearer understanding of his work, you can refer to his presentation titled "Category Theory for the Working Hacker" (https://www.infoq.com/presentations/category-theory-proposit...). The title is quite self-explanatory.
Then there's John Hughes, who is renowned for "Generalising monads to arrows", known as Hughes Arrows. His work has a profound correlation with Category Theory, a fact that John Hughes is fully aware of.
In my view, these examples provide sufficient evidence to affirm that Haskell's language designers are well versed in Category Theory concepts. These concepts, to varying degrees, have informed the design of Haskell. Of course, discussing individual features such as type families can become contentious when determining the extent of Category Theory's influence. For instance, it could be argued that these features are more closely related to Type Theory. However, many argue that Type Theory is the internal language of Category Theory.
> There is a deeper discussion to be had here, along the lines of "does it count as an application of math if none of the people doing the applying think about the math." I think the answer is no
I'd like to introduce you to the topic known as the Curry-Howard-Lambek correspondence, which posits a three-way isomorphism between types in programming languages, propositions in logic, and objects within a Cartesian closed category. You may already be familiar with the term "proofs-as-programs". It's important to note that the type system in Haskell isn't sufficient for theorem proving, but it becomes capable of constructing elementary proofs if you enable features like DataKinds, GADTs, PolyKinds, ScopedTypeVariables, TypeApplications, TypeFamilies, and TypeOperators. In contrast, I've also worked with Coq, which undeniably possesses the strength to prove intriguing theorems. What's particularly notable about Coq is its capacity to output Haskell programs based on its proofs, resulting in a Haskell program that lacks the strong guarantees of Coq. In this sense, you could imagine the resultant Haskell program as a "proof sketch" (which is usually correct if it compiles).
I don't presume that you would refute this isomorphism. However, it's possible that you have again a differing perspective on what isomorphism actually means. To me, it's pretty much equivalence.
I think you missed one level of indirection in my argument. I'm not claiming that language designers employ Category Theory explicitly when designing new language features (although this is indeed the case with Haskell, PureScript, and similar languages). Rather, my argument is that Category Theory features typically debut in these purely functional languages and then you will see on the Wikipedia page of mainstream languages something like: “Influenced by Haskell” (e.g. Rust, +20 others) . Category Theory is very abstract by nature, so I think it is only natural that there is some kind of indirect step through e.g. Haskell where people can see it in action first, before such features land in mainstream programming languages. The language designers would then say, 'Well, I have been influenced by Haskell (and not by Category Theory)', although the concept behind it is truly based on CT.
Many programmers don't keep math books at their workstation. However, they constantly utilize mathematical concepts in their coding. Often, they refer to programming language tutorials where these mathematical ideas are already implemented, for example, in Python or C++. This is as opposed to learning the concepts directly from a book on Algebra, Geometry, or Trigonometry. However, that still qualifies as applied mathematics. Hence, I see no reason why it shouldn't count as applied CT if you borrow concepts from Haskell that are based on CT.