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

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.

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.

Comments URL: https://news.ycombinator.com/item?id=49049660

Points: 3

# Comments: 0

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.

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

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.

It was Kafkaesque, discontinuing a product before release.

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.

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.

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

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

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.

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.

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.