My top interest is AI safety, followed by reinforcement learning. My professional background is in software engineering, computer science, machine learning. I have degrees in electrical engineering, liberal arts, and public policy. I currently live in the Washington, DC metro area; before that, I lived in Berkeley for about five years.
I wanted to highlight the Trustworthy Systems Group at School of Computer Science and Engineering of UNSW Sydney and two of their projects, seL4 and LionsOS.
We research techniques for the design, implementation and verification of secure and performant real-world computer systems. / Our techniques provide the highest possible degree of assurance—the certainty of mathematical proof—while being cost-competitive with traditional low- to medium-assurance systems.
seL4 is both the world's most highly assured and the world's fastest operating system kernel. Its uniqueness lies in the formal mathematical proof that it behaves exactly as specified, enforcing strong security boundaries for applications running on top of it while maintaining the high performance that deployed systems need.
seL4 is grounded in research breakthroughs across multiple science disciplines. These breakthroughs have been recognised by international acclaimed awards, from the MIT Technology Review Award, to the ACM Hall of Fame Award, the ACM Software Systems Award, the DARPA Game changer award, and more.
They are building a modular operating system called LionsOS:
We are designing a set of system services, each made up of simple building blocks that make best use of the underlying seL4 kernel and its features, while achieving superior performance. The building blocks are simple enough for automated verification tools (SMT solvers) to prove their implementation correctness. We are furthermore employing model checkers to verify key properties of the interaction protocols between components.
Core to this approach are simple, clean and lean designs that can be well optimised, use seL4 to the best effect, and provide templates for proper use and extension of functionality. Achieving this without sacrificing performance, while keeping the verification task simple, poses significant systems research challenges.
It seems like a catastrophic civilizational failure that we don't have confident common knowledge of how colds spread.
Given the context above (posted by bhauth), the problem seems intrinsically hard. What would make this a civilizational failure? To my eye, that label would be warranted if either:
in alternative timelines with the same physics and biological complexity, other civilizations sometimes figured out transmission. If the success rate is under some threshold (maybe 1%), it suggests variation in civilization isn’t enough to handle the intrinsic complexity. (This option could be summarized as “grading on a multiverse curve”.)
deaths from the common cold (cc) met the criteria of “catastrophic”. The cc costs lives, happiness, and productivity, yes, but relative to other diseases, the “catastrophic” label seems off-target. (This option is analogous to comparing against other risks.)
Are you positing an associative or causal connection from increased intelligence to decreased listening ability or motivation to those who are deemed less intelligent? This is a complex area; I agree with statisticians who promote putting one’s causal model front and center.
A browser doesn't count as a significant business integration?
It seems to me the author's meaning of business integration is pretty clear: "profitable workplace integrations, such as a serious integration with Microsoft office suite or the google workplace suite." -- integrations tailored to a particular company's offerings. A browser is not business-specific nor workplace-specific.
I don't usually venture into LessWrong culture or "feels" issues, but the above comment seems out of place to me. As written, the comment seems more like something I would see on Hacker News, where someone fires off a quick quip or a zinger. I prefer to see more explanation here on LW. I'm in some ways a HN refugee, having seen too many low-effort ping-pong sniping contests.
Asking even a good friend to take the time to read The Sequences (aka Rationality A-Z) is a big ask. But how else does one absorb the background and culture necessary if one wants to engage deeply in rationalist writing? I think we need alternative ways to communicate the key concepts that vary across style and assumed background. If you know of useful resources, would you please post them as a comment? Thanks.
Some different lenses that could be helpful:
“I already studied critical thinking in college, why isn’t this enough?”
“I’m already a practicing data scientist, what else do I need to know and why?
“I’m already interested in prediction markets… how can I get better?”
“I’m not a fan of parables, can you teach me aspiring rationality in a different way?”
“I would never admit this except to close friends, but weird or fringe movements make me nervous, but as do think of myself as a critical thinker, help me ramp up without getting into uncomfortable areas.”
“I would never admit this to others — and may not even recognize it in myself — but my primary motivation is to use evidence and rationality as a cudgel against my opponents. Can you teach me how to be better at this?” (And this reminds me of Harry teaching Malfoy in HPMOR with an ulterior motive!)
It seems retroactive if-then commitments could be one mechanism for mitigating the Boiling Frog or Camel's Nose metaphors.
I’m interpreting your comment as fitting into a kind of “game theory for rationalists who want to effect change in the real world.” This is complex and situational, and I’m skeptical I can say much that is interesting, actionable, and generalizable. Still, the following statements seem true to me, but I haven’t vetted them:
A strategy of aiming for high epidemic standards has many advantages:
However, this might:
There’s something peculiar about the motte and bailey fallacy compared to many other fallacies. The former requires change (often via the passage of time) whereby one sneakily changes the contents of their Central Claim box*, hoping others won’t notice.
I have a theory: the motte and bailey fallacy would be harder to perpetrate if one’s argument had to be written out visually. This would freeze it in time and help people to detect Central Claim box shenanigans.
* originally instead of “box” I was going to say variable in the programming language sense, but I didn’t want to get into the semantics of mutable versus immutable variables, which might lead to Rich Hickey’s famous talk on identity and state.
To varying degrees, people immersed in the study of economics may adopt more than just an analytical toolkit; they may hold some economic concepts as moral foundations.
To give some context, I have bolded two parts from Teaching Economics as if Ethics Mattered (2004) by Charles K. Wilber:
I have spent the past thirty-five years as a professor of economics. Over the course of my tenure at The American University, in Washington, DC (1965-75) and the University of Notre Dame (1975 present), however, I became ever more disenchanted with the capacity of traditional economic theory to enable people to lead a good life. I found myself unable to accept the values embedded in economic theory, particularly the elevation of self-interest, the neglect of income distribution, and the attempts to export these values into studies of the family, the role of the state and so on. As a result I started researching and writing on the nature of economics and the role of ethics in economic theory.
This work has led me to three important conclusions. First is the conviction that economic theory is not value-free as is so often claimed. Rather, it presupposes a set of value judgments upon which economic analysis is erected. Second is the realization that the economy itself requires that the self interest of economic actors be morally constrained. Third is the recognition that economic institutions and policies impact people's lives requiring that both efficiency and equity be assessed. Teachers of economics need to make use of these insights.
Though Wilber (above) focuses on neoclassical economics as entangled with libertarianism, there are other couplings across different flavors of economic history: Marxism, Keynesianism, Development Economics, and more.
I have a working theory, which I have reflected on imperfectly: mentioning the difference between an analytical toolkit (aka modeling approach) and a value system goes a long way towards orienting myself in a discussion with someone I don't know well. In some ways, it can be a test balloon to assess someone's awareness of the complexity of economics.
I composed this poem by myself (except for the final 4 lines):
Sonnet 4.5 tells me: