nextos

You need them in some scenarios. For example, lots of car rental companies refuse to take anything but a physical card.

AFAIK, Galois is 100% employee owned: https://www.galois.com/life-at-galois

I know people working both at Galois and Mondragón, and they seem to be relatively similar in spirit.

> You can't formally verify your application works correctly under transient network error conditions if you never thought about what your application should do under those conditions.

This is why it's so important to separate functional from stateful code. Functional code is generally easier to specify. And, by isolating stateful code, one can e.g. fail fast and avoid stepping into undefined behavior.

I agree with the core thesis that LLMs + theorem provers might make formal methods cheap enough to be practical in software development.

The biggest issue was always cost. But there's still an alignment problem. Without human supervision, things might drift away from the original specification and intent.

From my own experience, what works best is some kind of Hoare/separation logic (contracts), as these are quite easy to follow and decompose.

Even something as simple as a minimal Haskell subset, plus a bit of LiquidHaskell can get you really far if you are pragmatic.

Yeah, I heard some horror stories a few years back. Trustpilot and Google reviews had some interesting cases.

Gatwick long-term parking is not expensive if you book in advance. You need to take a slow bus shuttle to the terminal, but it's never more than 15-20 min including waiting time. I've used it a zillion times as I'd rather not give my keys to those meet & greet companies who drive your car 5 miles. It might void insurance and waiting times when you return tend to be over an hour.

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].

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