HN user
Welcome to my Hacker News profile. You can find out more about me at http://www.michaelmcthrow.com.
I’m an noob to Lean myself, but my best explanation is that asserts are checks that happen at runtime. Imagine compile-time asserts, where the compiler is able to determine the validity of assertions without needing to run the program. Formal verification techniques make this possible. In Lean, it is possible to write a proof that, if true, guarantees that the code works.
I’m out of the loop these days in systems research since I largely focus on programming languages and AI these days (though I still love systems) and I treat research more as a side hobby rather than a full-fledged career. It’s disappointing to hear about toxic systems labs. There’s also the “funding-or-perish” and “publish-or-perish” pressures of academia. This is one of the reasons why I teach at a community college, where 8 months of the year I focus on teaching, leaving me 4 months of break per year where I could do research without having to worry about my tenure chances or about funding, though it would be nice to be able to pay some students to help with research projects, and it would also be nice to have the funds to buy expensive equipment such as GPUs with large amounts of RAM.
I may be biased since I interned at Google in 2013 and 2014, but Google in the 2000s and early 2010s felt downright magical as someone who wanted to pursue a career in systems software research. They made impressive technologies that still hold up today, like MapReduce, BigTable, and Spanner. They hired many legends of computer science and software engineering, such as Rob Pike and Jeff Dean.
I’m concerned about the power that Google and other Big Tech companies have, but from a technical point of view Google has a lot of impressive technologies, and from a workplace standpoint, it seemed idyllic back in the early 2010s, though I’ve heard the work culture has changed in the past decade, and I may have rose-colored glasses from only being an intern there, never a full-timer.
I’ve been thinking about this over the past few days. There was an exciting keynote at PLDI 2026 by MIT professor Saman Amarasinghe where he talked about the intersection between compilers and machine learning, including LLMs. One of the works discussed during the keynote was the use of Claude Code by his colleague Martin Rinard to implement a compiler known as a credible compiler that outputs both compiled code and a proof that the output code correctly matches the input.
I'm a professor at a community college in Silicon Valley, and my students use online textbooks. I try to use Creative Commons or other libre textbooks, but sometimes I use paid textbooks when they are heads-and-shoulders better than their libre alternatives. Some e-textbooks can be accessed on a subscription basis. I admit I prefer non-subscription materials, but a colleague advised me that often the book that students learn from is different from a good reference book that students can use once they've already learned the material. For example, my colleagues and I have had great success with an online, interactive textbook for discrete math. While the subscription is unfortunately only valid for the duration of the course, once students have learned discrete math, they could buy a used copy of Rosen's discrete math textbook as a reference.
The nice thing about e-textbooks is not needing to carry around a bunch of heavy books. I remember the tomes I had in my college days, such as Stewart's Calculus.
I may be naïve or completely uninformed, but given the federal government’s vast resources, including supercomputers, national laboratories, the NSA, and many talented employees, why does the federal government need OpenAI or Anthropic for that matter when it has the resources to build its own LLM, even one exclusive for government use? The federal government has a long history of technical feats, such as the atomic bomb, the ARPANET, and the moon landing. Couldn’t it build its own state-of-the-art LLM?
When you have monopolistic or near-monopolistic control over platforms and other key pieces of software such as office suites, taste is irrelevant since people are still buying licenses out of necessity. Now, Microsoft is capable of writing impressive, tasteful software; I have fond memories of the Windows 95-2000 era, and I also enjoyed Office 97 and Visual Basic 6.0. Even Internet Explorer wasn't bad when it was competing against Netscape Navigator. The problem is Microsoft has a tendency of getting complacent and lazy once acquiring dominance, which breeds bad software.
Apple is more tasteful, IMO, but Apple also has a tendency to abuse its users, taking the attitude, "What are you going to do? Switch to Windows or Android?" Adobe has taken a similar attitude since the Creative Suite became subscription-only. "What are you going to do? The GIMP? Seriously?"
Come to think of it, modern cars have a lot of electronics such as touchscreens, cameras, and sensors. It wouldn’t surprise me if new car prices are not immune to what’s happening with RAM and storage prices.
This pressure works for pure software companies that don’t depend on hardware sales and that have competition. Unfortunately not all software vendors will respond to inflated RAM and SSD prices, since there are many important software vendors who have a vested interest in having users upgrade their hardware frequently. Microsoft still makes a good deal of money on OEM Windows licenses, Apple’s App Store and services revenue is built on regular sales of Apple hardware, and Google benefits from the sale of Android devices. The software needs to perform well enough on new hardware to not cause bad reviews, but sluggish enough (or with enough missing features) to motivate users to upgrade their hardware.
Additionally, software is often chosen based on market effects and not necessarily based on quality. If my colleagues use Zoom, then I need to use Zoom to avoid being difficult. If they use Microsoft Office and take advantage of features that LibreOffice and other competitors can’t support well, then I’m pressured to also use Microsoft Office for compatibility reasons.
The only silver lining I see is that these price hikes will effectively freeze current software requirements in the near future, since purchasing power has been diminished. The MacBook Neo has set 8GB of RAM as the standard for casual users. I’ve found that I don’t have a good time on Windows 11 with 8GB of RAM, but 16GB provides more breathing room and 32GB is great. I don’t expect software companies to revert to the days where they needed to squeeze every kilobyte of RAM like back in the 80s and 90s, but I do expect them to be more mindful of the fact that a lot of people will be using 8GB and 16GB configurations through at least the end of the decade.
The only other event I could remember in the history of Apple that is remotely comparable is the release of the original Power Mac G4 towers in 1999. They were originally going to have 400MHz, 450MHz, and 500MHz models, but due to issues regarding processor availability, Apple lowered the specifications by 50MHz for each model, but without lowering the prices.
https://lowendmac.com/1999/power-mac-g4-yikes/
I have a 350MHz model that I purchased used for $40 back in 2009.
I’ve never seen across-the-board price hikes from Apple that were not accompanied with some type of upgrade.
That’s terrible. I purchased my M4 Mac Mini (base 16/256 model) two months ago because I wanted an ARM Mac for a software project. I feared that the M5 Mac Mini would have a price bump, but I would’ve never guessed that Apple would dramatically hike prices for existing models.
I have some choice words for Sam Altman for destroying the personal computing marketplace by cornering the memory market…
Rob Pike of Plan 9 and Go fame lamented this back in 2000 in his “Systems Software Research is Irrelevant” talk:
http://herpolhode.com/rob/utah2000.pdf
I’d love to see a new operating system that explores radically different APIs for applications. The trouble is writing an operating system is a large effort. Barring market effects, OS has to be heads-and-shoulders better than existing ones in order to convince application developers to write software for it. Windows, macOS, and Linux are good enough for most people, even techies. Additionally, it is often easier to modify an existing operating system such as Linux than to go through the trouble of writing a brand new operating system.
XP also introduced activation, which is one of the reasons I prefer Windows 2000 to XP.
I feel the exact same way. I was a Ron Paul Republican from 2007 (when I became old enough to vote) until 2016, when I changed my registration to “no party preference” in the aftermath of the GOP primary results. It hasn’t gotten to the point that I started donating to Democrats, but I’ve found myself voting for Democrats in recent elections. My stance these days is that as nice as it would be to have libertarian governance, rule of law and maintaining our liberal institutions is much more important, and if it means voting for Democrats, then I’d rather deal with a bigger government than I’d like than the chaos we’re seeing now.
I’m not optimistic about the near future. It seems that the post-WWII order in the developed world is disintegrating. It seems that the political and business elites of America and some other developed countries have forgotten the concept of noblesse oblige, that elites have a responsibility to serve the general public. Greed and power have gone unchecked. This has negatively affected the lives of many in the developed world, and many are justifiably angry. Unfortunately, anger can either devolve into uncontrollable rage or be misdirected as a controlled weapon. Demagogues have been able to capture some of this anger and use it for their own aims, which is making matters worse by increasing the number of angry people.
Rising inflation, especially in housing prices, is demoralizing, where one’s efforts to save is quickly evaporated thanks to a combination of bad fiscal/monetary policy and housing regulations that benefit existing homeowners over prospective ones.
Personal computing was one of the nice bright spots of modern society. I grew up during the rise of the personal computer, the Web, and mobile computing. Computing felt liberating, empowering, and enjoyable. Unfortunately major players have been able to gain oligopoly power over computing. Enshittification is the norm in modern software, and it’s difficult for upstarts to compete against entrenched oligopolies. The generative AI boom and the massive run on the RAM and storage markets have caused massive price hikes, which now threaten to price us out of personal computing. The one area that has long resisted price inflation has succumbed to it. It seems like we are getting priced out of living.
Germany has both the Autobahn and rail.
Pre-Carly Fiorina Hewlett-Packard was a great example of an old-school Silicon Valley company, long before the era of “move fast and break things” and of Zuck, Elon, and Altman. I used to work for a Japanese company until I left a few years ago to teach, and when I read about the HP Way, it reminds me in many ways of life at my former employer:
https://www.hp.com/hpinfo/abouthp/histnfacts/publications/me...
Unfortunately marketing helps sell OS upgrades and new PCs, and one way to market a new OS is to advertise its “new and improved” UI. OS UI used to be more utilitarian and rooted in HCI principles, notably the classic Mac OS and Windows 95/98/NT/2000.
Ironically Apple got the ball rolling with fashionable UI when it released Aqua in early Mac OS X, though Aqua was well-executed, having style while still being rooted in HCI principles. Unfortunately the industry took the wrong lesson; competitors responded to Aqua’s style without providing UIs of substance. Sadly even Apple has slipped once Steve Jobs passed away; its UIs have increasingly become more style over substance. Apple has long abandoned the days of Bill Atkinson, Larry Tesler, Bruce Tognazzini, and Don Norman, and unfortunately Jony Ive was less effective when Steve Jobs was no longer around to provide critical feedback. macOS 26 is one of the biggest UI regressions in the entire history of the Mac, though thankfully it’s not unusable and it appears that macOS 27 will be a big improvement thanks to user and reviewer feedback.
Unfortunately when you live in a place (like most American cities) where they’re largely built under the assumption people will drive everywhere, a car is essentially required. It’s expensive owning and maintaining a car, but it also feels demoralizing dealing with limited public transportation and neighborhoods that aren’t walkable. There are walkable metro areas in the United States, but they tend to be very expensive, sometimes more expensive than living in a suburb or exurb and dealing with the cost of commuting. I grew up poor; dealing with hour-long bus waits, late buses, multiple transfers, and limited choices is a powerful motivation to save up for a car.
I love Tokyo (I spent eight months in Kawasaki in 2010), but I can see the appeal of living in a smaller place in Japan (though I’d personally be hesitant to live in a small, isolated town with little or no public transportation). Crowded trains and long lines can get tiring after a while.
I spent last summer in Toyohashi in Aichi Prefecture; I was a visiting researcher at Toyohashi University of Technology. While Toyohashi is not a small town by any means, it is far smaller than Tokyo. I found it nice for day-to-day living. Not crowded at all, and I found the bus service to be good; not world class, but comprehensive and ran frequently enough to be useful. It had plenty of grocery stores and department stores for everyday living. If I needed something unavailable in Toyohashi, Nagoya wasn’t too far away, and if I needed to be in Tokyo, I could get there in 90 minutes on a Hikari train on the Tokaido Shinkansen. I’d do it again; in fact, I’m going back to Toyohashi in a few weeks for another monthly stay.
This is a description of Alan Kay’s STEPS project:
https://worrydream.com/refs/Kay_2007_-_STEPS_2007_Progress_R...
This is the final report:
Not disputing any of the statistics cited, but there is one advantage of being homeless in California compared to other places: favorable weather, especially along the coast. Snow is a once-in-a-generation event outside high-elevation areas, and while it does freeze on some winter nights, it’s rarely below 30 F. There are many parts of the country where temperatures sometimes get low enough to be life-threatening for those with inadequate shelter, heating, and clothing. The coastal areas of California also typically don’t get too hot. Heat is more of an issue inland, particularly the Central Valley and the desert.
I doubt that most computer users have more than 16GB of RAM in their systems. There are plenty of users on 8GB systems and some still on 4GB. Even when considering bloated Web apps, 8GB of RAM is passable and 16GB is plenty.
I think people who need more than 16GB of RAM are power users with higher memory requirements, such as those using local LLMs, those who frequently use virtualization, and people doing tasks such as video editing.
Apple did openly court Unix users during the early days of Mac OS X. As a teenager during this era, Macs of this era were my dream machines due to Mac OS X, and I was so happy to buy an 2006 MacBook the summer after my freshman year of college with money earned from a summer research internship.
Here's a Titanium PowerBook G4 ad that says "Sends other Unix boxes to /dev/null": https://www.reddit.com/r/vintageunix/comments/b4kojo/sends_o...
Here's a snapshot of the software solutions page for the aluminum PowerBook G4 from November 2004, proudly touting Unix and even X11:
https://web.archive.org/web/20041126011836/http://www.apple....
Some quotes from the Power Mac G5 page (https://web.archive.org/web/20041126015955/http://www.apple....) from the same era:
"With the Power Mac G5, a researcher can now run both productivity applications and high-performance UNIX applications on a single system. Mac OS X Panther includes 64-bit optimized system math, vector and image libraries that take maximum advantage of the 64-bit G5 processor."
There was also a cluster in Virginia made of Power Mac G5s, which Apple also touted.
When I was in high school in California more than 20 years ago, SAT math alone was insufficient for admissions to STEM programs at mid-ranked and top-ranked universities. I was required to take the SAT Math IIC subject test, which went up to pre-calculus. We were also strongly encouraged to take calculus in high school. There are two AP Calculus exams: AB (which covers the first semester of university calculus) and BC (which covers the first two semesters).
Wow, this is very insightful and I haven’t looked at saving for retirement as a type of debt before! Thanks for sharing!
I would love to see a follow-up series that covers the dot com bust, the revival of Silicon Valley’s tech industry thanks to mobile and cloud tech, and the modern AI boom, starting with deep neural networks ran on GPUs and culminating with large language models.
In my opinion, it’s been a problem for a long time. Sure, the titans of industry are very interested in the profitable applications of science, but they are generally less interested in investing in science, let alone the science itself. Science is seen as a cost center, and research is inherently risky. Even in the glory days of Bell Labs and Xerox PARC, both were backed by monopolies (the Bell System was the phone monopoly, and Xerox had patents in xerography). The former was subject to special government rules due to AT&T’s constant anti-trust troubles, and the latter’s culture was heavily influenced by ARPA due to ex-ARPA people like Bob Taylor.
I am reminded by this quote from an email exchange between Bret Taylor and Alan Kay, published in 2017:
“As I pointed out in a previous email, Engelbart couldn't get funding from the very people who made fortunes from his inventions.
“It strikes me that many of the tech billionaires have already gotten their "upside" many times over from people like Engelbart and other researchers who were supported by ARPA, Parc, ONR, etc. Why would they insist on more upside, and that their money should be an "investment"? That isn't how the great inventions and fundamental technologies were created that eventually gave rise to the wealth that they tapped into after the fact.
“It would be really worth the while of people who do want to make money -- they think in terms of millions and billions -- to understand how the trillions -- those 3 and 4 extra zeros came about that they have tapped into. And to support that process.”
https://worrydream.com/2017-12-30-alan/
The titans of industry not understanding the importance of science beyond its profitable applications doesn’t surprise me at all.
This is cool news. Given Apple’s history, there’s something rather interesting about Haiku, a BeOS clone, running natively on Apple Silicon, like stepping into an alternate universe.
On another note, while I’m grateful for Asahi Linux, Haiku, and other efforts to bring alternative operating systems to Apple Silicon, I wish Apple provided more documentation. It took the Asahi Linux team tremendous effort to get its OS running on M1 and M2 Macs, and it’s still going to be a while until we see M4 and M5 Macs run alternative operating systems. macOS is a great desktop OS, but it’s nice having diversity, especially when the hardware eventually gets unsupported by Apple.
NeXT became an enterprise software company when it shut down its hardware division around 1993. At first it only sold its operating system, which got ported to x86, PA-RISC, and SPARC. Then, NeXT started selling development tools and libraries. The OpenStep API was developed as part of a joint project with Sun. OpenStep is an Objective-C API that is based on NeXTstep’s libraries, but made to be portable. OpenStep was the native API for the OPENSTEP (note the capitalization) operating system and was also available for Sun Solaris and even for Windows. I have a CD named OPENSTEP Enterprise, which is installable on Windows NT and Windows 95. There was also Portable Distributed Objects, which was NeXT’s take on distributed objects, which was big in the 90s (like CORBA). Finally, NeXT had a web server named WebObjects that had major customers such as Chrysler in 1996.
At the time Apple purchased NeXT, NeXT was definitely an enterprise software company. The black workstations were gone, the operating system was not marketed to casual users but to developers and others who needed software that used the OpenStep API, and it sold various developer tools.