nextos

It's sadly becoming harder. I've been playing that game for quite long and hope to stick to web apps, but still.

Some banks limit functionality on web apps, which is annoying.

More importantly, many refuse to provide a decent 2FA other than push notifications inside the app or SMS, which is insecure and EU has mandated its phaseout.

The thing that works for me is to pretend to be clueless and get an old hardware OTP generator, but those are susceptible to impersonation attacks on the bank side.

And he effectively killed the last EU platform. Will we ever see another one?

I miss these simpler times when devices were made to serve users, and not the other way round.

I think this is the real problem. I am sympathetic towards automated code synthesis.

But without formal verification and a human reviewing specifications to ensure alignment, I think code will end up being broken in unexpected ways or drift away from the original intent.

Exactly, and it sold really well despite that.

It was Kafkaesque, discontinuing a product before release.

Discussed in HN many times, but worth restating once more. The N9 was fantastic. A joy to use, and in many ways the best design, both hardware and software, I've ever handled. Everything had been designed with care and some UI elements remain unmatched.

I think I was one of the first developers that got an N770 engineering sample (the first product in the N770-N9 saga) and it was really clear that they were onto something. Sadly, internal politics won over company and consumer interests. It took them extremely long to let this be a phone, not just an "Internet tablet". It was bizarre.

The same team is now behind Jolla/Sailfish. It's pretty remarkable how far they've got, but it's obviously not a perfect product given how small they are compared to the other mobile juggernauts. However, it's usable as a daily driver and, with a critical developer mass, it could get somewhere. There are already quite a few indie apps.

Crucially, I think it's the only platform that has the potential to set you truly free. GrapheneOS is the other alternative I can also endorse and tolerate, but it has a different set of compromises, and it's a bit fragile to Google pulling the plug. But it's great in its own ways.

Yes, this is why garden leaves are popular in quant finance.

You get paid for about a year to do nothing so that the trade secrets from your firm (trading strategies) expire.

That's very different from a non-compete. A non-compete is about your own know-how, not the company's.

I have never said they always act as a bloc, but their industry has a strong component of long-term strategic government planning behind them.

I think it's a deliberate business strategy of commoditization of their complement.

China acts like an entire bloc, not as single companies, and they want to monetize hardware.

It is true that Lean has seen relatively little adoption in software verification compared to e.g. Isabelle and Rocq (previously Coq). Even Agda has had more traction in that domain.

However, Lean is currently gaining significant momentum as an alternative, particularly due to its capabilities as a general-purpose functional programming language.

Personally, I think something based on Hoare or separation logic would be more practical as it'd be easier to align requirements with specifications. I like Dafny and F*.

SailfishOS can run lots of banking apps with an Android emulation layer.

It's not perfect, but far from useless. Some use it as a daily driver.

Depending on your country, it can be super doable. There are also lots of indie native apps.

Keep in mind vitamin D is really, among other things, an immune signaling molecule.

So, we know the mechanism, and it's quite plausible that supplementation works.

In other words, as an skeptic, I don't think it's just an epidemiological correlation.

I am not sure I agree we've yet to see any other architecture that competes with a large transformer. For example, in long-range tasks such as those related to genome prediction, state-space models (Mamba) exhibit SOTA performance. I also think it's hard to separate architectural advantages from maturity, given that transformers have received much more attention.

I agree. I also think it's about the hardware and, obviously, recognizing AD as the fundamental primitive.

Particular architectures don't matter so much yet. It's quite possible that S3-Mamba or xLSTM could be used in lieu of transformers and we would still have LLMs.

I agree. The US Army already recognized this problem and developed the Munson last before WWI.

Some mid and high-end footwear brands produce boots with Munson or Munson-like lasts. It helps tremendously. I cannot go back to narrow toeboxes.

Oddly, lots of sports footwear suffers from the same issue and wide toeboxes are not as popular as they should be.

I would say that lots of interesting things are happening in biotech, and these things are slowly building critical mass, similar to what happened in computer hardware during the period 1970-2000.

Genomic platforms are now able to capture multiple measurements (e.g. RNA and chromatin openness) from single cells in large tissue slices/massive perturbation experiments.

Once time gets baked into the equation, we will be able to build better models of systems biology. However, human trials will still be a major bottleneck.

It is difficult. I think the key is that Spain has a large corps of civil engineers working for the government. They plan all projects with great detail and then oversee their execution.

Agile regulations against NIMBYism and a world-class civil engineering industry with HQs in Madrid also help.

A good analogy is to ask what would need to be true for Madrid to replicate the AI hub in SF? Great VC, top engineers, certain risk-taking mentality, etc.

So, it's not easy. The environment that creates a fabric for radical innovation is quite different from a statist mentality, although hopefully, both are not mutually exclusive.

True, also very precarious and unstable. It is now common not to get a long-term contract until your 40s.

Given the massive pay gap with industry and scarce funding, it's natural lots of innovation has shifted to industrial labs.

"Probabilistic Machine Learning" by Murphy [...] even if it contains virtually no deep learning in it

This is confusing. Are you referring to the old 2012 version?

Volumes 1 & 2 (2022-3) contain a substantial amount of deep learning [1], including relatively recent developments.

There's also a new RL volume getting written, with some drafts deposited in arXiv [2].

[1] https://probml.github.io/pml-book

[2] https://arxiv.org/pdf/2412.05265

See for example https://www.mongodb.com/company/blog/engineering/conformance...

I've worked in formal methods for quite a long time, and I disagree a bit with your statement that new logics are not helpful. Industrial logics are really practical and allow you to write all sorts of sophisticated properties that your system should satisfy in a very succinct way. Logic is to computer science and software engineering what calculus is to physics and mechanical or civil engineering [1, 2]. Things like LTL or, more recently, separation logic, have been incredible breakthroughs.

TLA+, which has gained quite a lot of popularity, is a testament to that. Model checking is eminently practical. The exciting thing now is that heavier formal methods, in particular theorem proving, might become cheap enough to use in regular systems software. Writing formal specifications for functions and getting them synthesized and proven correct by some SAT/SMT, theorem prover & LLM hybrid may become the norm in the not-too-distant future.

[1] On the Unusual Effectiveness of Logic in Computer Science. https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf

[2] From Philosophical to Industrial Logics. https://www.cs.rice.edu/~vardi/papers/icla09.pdf

My statement obviously referred to major cities, which is where most IT jobs are, as I indicated remote work allows you to leverage cheaper locations.

Take for example Oxford. A typical rental will be around £1,600 pcm. The median pre-tax salary is around £50,000, which converts to around £3,100 net. So, the apartment is actually more than 50% of your net income. Some programming jobs will pay a bit more, but you get the idea.

Another example, in Barcelona, a median net salary is less than a median rental. IT will pay better, but expect to spend around 40% of your net salary. I could also bring up Stockholm or Copenhagen and, unless you are in very senior IT jobs, it's going to look very similar.

True, there's also another factor about not having to be tied to a geographic spot, housing costs.

In EU, even relatively good IT salaries are mediocre when you factor in monthly rental. A simple one-bed apartment can easily take 50% of your net income.

Having freedom to move, even within a particular country, allows reducing that 50% to something more sustainable.

But, if I have understood correctly on a quick read, they also claim transformers have pretty low expressive power. In particular, they claim they are limited to star-free subregular languages, whereas RNNs can recognize any regular language/simulate finite automata.

This doesn't imply you can't get aid from a LLM to e.g. implement a function that has a formal specification (an application I think is very promising), but surely it has some profound implications on how much of a large system can be understood by a LLM at once, without supervision.

Yes. However, there are some polygenic risk scores for EDS. While not approved for clinical practice, they can serve as guidance.

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?