nextos

What treatment did your wife receive? Did she improve?

Did doctors confirm Ehlers Danlos with genome sequencing?

I think firmware updates and even map routes can be uploaded offline by mounting the watch as a USB mass storage device?

I wish Casio, Polar, Suunto and others provided this functionality.

There is some community software for Polar that enables offline data exchange, but it is a bit hacky, and OFC no firmware updates.

Suunto used to have a really good offline solution, but they discontinued that and moved to the cloud.

Garmin can be used completely offline?

AFAIK, they even have some watches with no radio hardware so that they can be used in sensible environments.

> a rolling release like NixOS is exactly the opposite of an LTS distro

NixOS is not rolling release. This is a common misconception. You can use the unstable channel, which is a rolling release, or the regular channels which get released twice a year. These are really stable and move very slowly. You can also mix and match, running software from different channels.

> I actually wonder what would happen to a NixOS installation frozen in time for 5 years that then you want to update to latest all of a sudden

I have done this recently as I kept an airgapped machine, which I decommissioned, connected to the Internet and updated to the latest channel. Everything worked just fine. I just had to change a couple of options in my configuration which had become outdated. Nix is functional, so it's much less prone to all stateful issues that plague other package managers.

I would say NixOS, where it is trivial to switch across releases, run software from different releases, and perform rollbacks.

I have been running NixOS on several servers for more than a decade. No reinstalling, upgrading, or any breaks whatsoever.

I am also considering to buy 3-4x RTX 6000 Pro 96GB plus some Ryzen workstation with a grant.

Is this the best general-purpose choice as of 2026 with $50k for training, fine-tuning and running large open models?

That might emerge as one of the main tasks of future software engineers, writing formal specifications by hand.

It could be the case that Tony Hoare was right, just too early.

Good clothes can be definitely stitched. Some brands even offer free or reasonably priced repairs. Patagonia or Citizen Wolf are two examples that spring to mind, and it's even more common once you cross a certain price point. Same applies to good hardware, but you need to do some research before buying.

I am afraid Google's business model is incompatible with this approach as they have almost no customer service because it doesn't "scale". Actually, what they are doing is turning customer service costs into externalities, i.e. environmental waste.

This is happening in large parts of the EU as well. It's pretty mind blowing. Since the mid 2010s, the new build construction rate has slowed down to alarmingly low levels. A few years before that, there was an oversupply, yet they kept building. It's totally intentional.

Unsurprisingly, affordability is so bad. In lots of major cities, a one-bed rental takes around 50% of a mid-career post-tax salary. You have become an indentured servant for whatever real estate fund owns your property. Lots of regulatory capture behind the scenes.

Ironically, some parts of the UK, including Home Counties, are now much better than most EU, including Scandinavia, with lots of shared ownership and affordable housing schemes. It's really easy. Increasing the supply of homes, in particular first homes, and preventing predatory tactics to constrain supply.

uBiome is probably the biggest one: https://ycombinator.fyi/exhibit/ubiome

A shame, because the idea was good. And, with a bit of patience, it was doable.

> languages really don't matter. Just pick up the details for the paradigm

True. The best programming books also reflect this ethos. Some people think Introduction to Functional Programming (1989) by Bird & Wadler is the best programming book ever.

The language-specific details (Miranda) are limited to a three-page appendix! The rest of the book is language agnostic, provided that your target language is functional.

IB questions require at least a mid-range calculator to obtain e.g. the ccdf of chisq, t, and other distributions.

In the exam, you'd also be at a disadvantage without advanced graphing.

Dafny and F*, which competes directly with Lean but is more guided towards SWE, are definitely worthy of consideration.

I agree granting processes permission to read any file is unsustainable.

In Linux, sandboxing with Firejail or bwrap is quite easy to configure and allows fine-grained permissions.

Also, the new Landlock LSM and LSM-eBPF are quite promising.

Seconded. All the Haskell people from Chalmers have produced very interesting work. Another example is Agda.

Different methods find different things. Personally, I'd rather use a language that is memory safe plus a great static analyzer with abstract interpretation that can guarantee the absence of certain classes of bugs, at the expense of some false positives.

The problem is that these tools, such as Astrée, are incredibly expensive and therefore their market share is limited to some niches. Perhaps, with the advent of LLM-guided synthesis, a simple form of deductive proving, such as Hoare logic, may become mainstream in systems software.

Also Claude owes its popularity mostly to the excellent model running behind the scenes.

The tooling can be hacky and of questionable quality yet, with such a model, things can still work out pretty well.

The moat is their training and fine-tuning for common programming languages.

Even small brand new apartments tend to have their own sauna, which is quite impressive.

That's a very fair point. There are some publications showing lower performance for languages with less training data. I imagine it also applies to different paradigms. Most training code will be imperative and of lower quality.

It should be better for the reasons explained in the article. Pure functions require no context to understand. If they are typed, it's even simpler. LLMs perform badly on code that has lots of state and complex semantics. Those are hard to track.

In fact, synthesis of pure Haskell powered by SAT/SMT (e.g. Hoogle, Djinn, and MagicHaskeller) was already of some utility prior to the advent of LLMs. Furthermore, pure functions are also easy to test given that type signatures can be used for property-based test generation.

I think once all these components (LLMs, SAT/SMT, and lightweight formal methods) get combined, some interesting ways to build new software with a human-in-the-loop might emerge, yielding higher quality artifacts and/or enhancing productivity.

I think LLMs are great at compression and information retrieval, but poor at reasoning. They seem to work well with popular languages like Python because they have been trained with a massive amount of real code. As demonstrated by several publications, on niche languages their performance is quite variable.

You have a point but current LLM architectures in particular are very fragile to data poisoning [1,2].

[1] https://www.anthropic.com/research/small-samples-poison

[2] https://arxiv.org/abs/2510.07192

Interesting, thanks for your replies.

You should consider publishing a patient case report somewhere, as I believe there are lots of valuable conclusions to be extracted from your work.

This is very impressive, top labs doing research often don't have experimental designs that are this elaborate. Was the TCR and BCR-seq you conducted helpful to design cell therapies, neoantigen vaccines, and monitor progress?

Given that you carry the HLA-B*27:05 allele, you might have been blessed by being predisposed to a better response. But probably you want to keep an eye on future autoimmunity issues. Talking from experience...

Previous discussion: https://news.ycombinator.com/item?id=47550016

> the reason it has been limited to those cases is drug development, today, is constrained by commercialization.

That's a good observation, but I think it's an incomplete picture. Another important constraint is often regulatory inertia and historical baggage.

The UK pioneered small classical and adaptive trials using Bayesian methods, and there were some promising results. A lot of modern Bayesian methodology was, in fact, developed at the MRC BSU Cambridge with this goal in mind. For example, the probabilistic programming language BUGS (1989).

Given that most drugs fail, the industry is highly incentivized to use Bayesian methods to fail faster. These models allow for more rapid dose-finding and the ability to distinguish promising leads using interim data, which is vital given the massive cost of any trial, especially late-stage failures.

But for Bayesian methods to make a dent, they'd need to be applied to a large number of trials, and change doesn't happen overnight. Lots of big pharma players, e.g. GSK, are becoming interested in moving to Bayesian methods in order to leverage prior information and work better within small-data regimes.

You don't need an app if you don't want one.

In a CLI, oath lets you calculate a TOTP.

But it's maybe a bit more insecure if you use the same machine.

The problem with mRNA vaccines for cancer is effectiveness. Vaccines already work well for prevention of relapses in e.g. tumors that have been surgically removed.

They might also be great combined with early-stage detection via ctDNA.

But in late-stage patients, the effectiveness is limited because the host immune system is compromised.

Several landmark mRNA cancer vaccine trials by BioNTech and others have pointed in this direction.

In vivo reprogramming of T cells might be the next frontier. In fact, the BioNTech founders are moving to a new venture, but it's unclear what their thesis is.

Exactly, see what is happening in Hungary.

Controlling Hungary is enough to veto some support for Ukraine.