nextos

FWIW, Novo Nordisk also tried to kill their GLP-1 effort several times according to the project lead, Lotte Bjerre Knudsen: https://archive.is/oLnBl

In large organizations, I guess a big chunk of success comes from being able to navigate all these political ups and downs.

The advantage of Apple is that they deal with a tiny amount of hardware. Vertical integration enables aggressive optimizations.

I agree that in case of Linux, a udev rule generator would be a fantastic step ahead in terms of usability.

One of my favorite machines was the MacBook Air 11 (2012). This was a pure Intel machine, except for a mediocre Broadcom wireless card. With a few udev rules, I squeezed out the same battery performance from Linux I got from OS X, down to a few minutes of advantage in favor of Linux. And all this despite Safari being a marvel of energy efficiency.

The problem with Linux performance on laptops boils down to i) no energy tweaks by default and ii) poor device drivers due to the lack of manufacturer cooperation. If you pick a machine with well supported hardware and you are diligent with some udev rules, which are quite trivial to write thanks to powertop suggestions, performance can be very good.

I am getting a bit more than 10 hours from a cheap ThinkPad E14 Gen7, with a 64 Wh battery, and light coding use. That's less than a MacBook Air, where I would be getting around 13-14 hours, but it's not bad at all. The difference comes mainly from the cheap screen that is more power consuming and ARMs superior efficiency when idling.

But I prefer not to trade the convenience and openness of x86_64 plus NixOS for a bit more battery range. IMHO, the gap is not sufficiently wide to make a big difference in most usage scenarios.

Probably, I would go through https://htdp.org.

Excellent textbook, intended for non-CS majors as well.

Builds solid timeless understanding.

The semantics of Dafny is carefully designed to make verification efficient.

Dafny can compile to and interface with a few languages, including C#.

There are excellent probabilistic extensions to temporal logic out there that are very useful to uncover subtle performance bugs in protocol specifications, see e.g. what PRISM [1] and Storm [2] implement. That is not within the scope of TLA+.

Formal methods are really broad, ranging from lightweight type systems to theorem proving. Some techniques are fantastic for one type of problem but fail at others. This is quite natural, the same thing happens with different programming paradigms.

For example, what is adequate for a hard real-time system (timed automata) is useless for a typical CRUD application.

[1] https://www.prismmodelchecker.org

[2] https://www.stormchecker.org

Yes, in fact there is research on type systems to ensure information flow control, avoiding unauthorized data access by construction.

Concrete Semantics [1] has a little example in §9.2.

[1] http://concrete-semantics.org/concrete-semantics.pdf

That's my opinion as well. Some functional language, that can also offer access to imperative features when needed, plus an expressive type system might be the future.

My bet is on refinement types. Dafny fits that bill quite well, it's simple, it offers refinement types, and verification is automated with SAT/SMT.

In fact, there are already serious industrial efforts to generate Dafny using LLMs.

Besides, some of the largest verification efforts have been achieved with this language [1].

[1] https://www.andrew.cmu.edu/user/bparno/papers/ironfleet.pdf

In case of LLMs, due to RAG, very often it's not just learning but almost direct real-time plagiarism from concrete sources.

FWIW, Jolla just announced a new phone: https://commerce.jolla.com/products/jolla-phone-preorder

That was my point, it is not a disability from an education POV, or at least I would not consider it as such without an independent audit.

I reviewed incoming applications during one Oxbridge academic application cycle. I raised some serious concerns, nobody listened, and therefore I refuse to take part on that any longer. Basically, lots of students are pretending to be disabled to enhance their chances with applications that are not particularly outstanding, taking spots from truly disabled students.

All it takes is a lack of principles, exaggerating a bit, and getting a letter from a doctor. Imagine you have poor eyesight requiring a substantial correction, but you can still drive. That's not a disability. Now, if you create a compelling story inflating how this had an adverse impact on your education and get support letters, you might successfully cheat the system.

I have seen several such cases. The admissions system is not effectively dealing with this type of fraud. In my opinion, a more serious audit-based system is necessary. Applicants that claim to be disabled but that are not recognized as such by the Government should go through some extra checks.

Otherwise, we end up in the current situation where truly disabled students are extremely rare, but we have a large corpus of unscrupulous little Machiavelli, which is also worrying on its own sake.

Samsung has good hardware, but their software is really mediocre, at best. Many of their devices are laggy and slow down further after some updates.

This is the case even on high-end devices. Our 12-month-old Galaxy Tab is slower than a 7-year-old Pixel. Hard to understand.

Plus, they make really odd tweaks to the UI, such as adding a permanent button overlay that clashes with most hamburger icons in websites and apps. This drives novice users insane.

If you wanna ship a custom Android, at least get it right. Otherwise, just stick to stock. Sony does this really well: https://developerworld.wpp.developer.sony.com/open-source

Some of the current EU ID cards are actually smartcards, so in terms of privacy guarantees and separation of concerns, we are moving backwards. I am also more comfortable with a low-tech solution that is not linked to my personal devices. Something like a FIDO passkey would be ideal as those are also able to verify the identity of the other side, but are relatively low-tech and won't serve to track me.

Personally, I liked the low-tech solution of code cards + password (2FA), used by e.g. Denmark as digital ID, now discontinued. I am aware that it is imperfect, and if you are not careful with MITM attacks you can get in trouble, but it was a good compromise to avoid the temptation to track citizens. Something like a hardware TAN generator, but with protection against MITM, would be an ideal compromise. The current trend of moving towards mobile apps that require hardware attestation is worrying.

Dino (XMPP, https://dino.im) is a great desktop client to talk to other XMPP clients, in particular Conversations, due to its broad support of XEPs.

This is a valid concern. Perhaps, if you are still interested in giving Linux a chance, you should consider immutable distributions like Fedora Silverblue or even going one step further with NixOS.

NixOS has a declarative configuration that is simply key=value for most use cases. Whatever you configure stays configured, and you can also rollback when doing dramatic changes e.g, migrating from Xorg to Wayland takes 2 min and changing 1 LOC in your configuration.

IMHO, this remains a great space to explore. You type some formal specification in e.g. Hoare logic, and a mix of SAT/SMT and LLMs autocomplete it. Correct by definition.

It would also facilitate keeping engineers in the loop, who would decompose the problem into an appropriate set of formally specified functions.

They could also chip in when necessary to complete difficult proofs or redefine the functions.

No, I haven't. I have used them with shallow embedding techniques that are relatively similar, but not in this way.

I have found Isabelle very useful, and Dafny even more so.

Amazon AWS uses Dafny to prove the correctness of some complex components.

Then, they extract verified Java code. There are other target languages.

Being based on Hoare logic, Dafny is really simple. The barrier of entry is low.

I don't think this is the real problem. In R and Julia tables are great, and they are libraries. The key is that these languages are very expressive and malleable.

Simplifying a lot, R is heavily inspired by Scheme, with some lazy evaluation added on top. Julia is another take at the design space first explored by Dylan.

No, it's just a gentle overview.

Igalia (https://www.igalia.com), also Spanish, is a fairly prominent tech company that is also a co-op.

Galois, Inc. (https://www.galois.com) is employee-owned, and they do lots of great formal methods work.

But not sure whether this model is appropriate for a startup. I guess splitting stock more evenly is a good starting point.

It does have a lively ecosystem in some niches. Formal verification is one of them.

For example, https://opam.ocaml.org/packages/why3 is a little marvel of engineering.

Gadgetbridge has very limited aGPS support, right? Without aGPS updates, any GPS device is going to have terribly long lock times.

Ideally, watches should do like Garmin's. Mount as mass storage devices via USB, and let the user download activity data and upload updates or routes.

We've done this, and it works. Our setup is to have some agents that synthesize Prolog and other types of symbolic and/or probabilistic models. We then use these models to increase our confidence in LLM reasoning and iterate if there is some mismatch. Making synthesis work reliably on a massive set of queries is tricky, though.

Imagine a medical doctor or a lawyer. At the end of the day, their entire reasoning process can be abstracted into some probabilistic logic program which they synthesize on-the-fly using prior knowledge, access to their domain-specific literature, and observed case evidence.

There is a growing body of publications exploring various aspects of synthesis, e.g. references included in [1] are a good starting point.

[1] https://proceedings.neurips.cc/paper_files/paper/2024/file/8...

It's disappointing. It reinforces the cliché that most hardware companies don't understand software.

The GPR-B1000 was promising, as it signaled Casio might be heading towards making watches with advanced features like GPS, yet a bit different from regular smartwatches and close to their traditional models. This model was tied to a phone app, but I thought this was OK for their first iteration.

Fast forward to 2023, their expensive DW-H5600 was very disappointing. They included a Polar heart rate monitor, which are known for their reliability. Nevertheless, hear rate readouts are extremely noisy to the point of being useless. Also, setting up the watch requires pairing it with a Casio app, which is absurd for a non-smartwatch.

I would love to be able to buy a normal watch that offers heart rate monitoring and basic GPS tracking but can be operated fully offline, doesn't need updates, and will not become abandonware in 5 years time. Garmin is nearly there with some models. Some Casio, Withings, Polar, and Suunto models also have interesting features but overall still far from that ideal goal.

Besides, in many regulated environments you can't have a watch with hardware radios like Bluetooth. Only Garmin seems to understand this. Suunto had terrific models, but is slowly falling behind and has been sold to a Chinese conglomerate.

> there is not anything necessarily wrong with dependent types, but that he doesn't believe they are necessary.

I think that, at least in software engineering, his point has not been disproven. Isabelle (classical) has a great track record in software verification. I don't see it as something inherently inferior to Rocq (dependently typed), which also has a great track record.

Lean doesn't have a great focus (yet?) on software verification. And Agda is also not mainstream on large-scale industrial verification. One interesting thing would be to compare Concrete Semantics [1] (Isabelle) vs The Hitchhiker's Guide to Logical Verification [2] (an approximate rewrite in Lean). I am still starting with the second one, so I can't say much yet, but it might be too basic to draw any conclusions.

Ultimately, refinement types embedded in general-purpose languages might be a more pragmatic approach. Leftpad proofs using Rust Creusot, Dafny, or LiquidHaskell are quite straightforward [3], but again this is just a toy problem.

[1] http://concrete-semantics.org

[2] https://github.com/lean-forward/logical_verification_2025

[3] https://github.com/hwayne/lets-prove-leftpad

The advantage of small purpose-specific models is that they might be much more robust i.e., unlikely to generate wrong sequences for your particular domain. That is at least my experience working on this topic during 2025. And, obviously, smaller models mean you may deploy them on cheaper hardware, latency is reduced, energy consumption is lower, etc. In some domains like robotics, these two advantages might be very compelling, but it's obviously early to draw any long-term conclusions.

True, also before, during, and after the Intel transition the ecosystem of indie and boutique apps for Macs was great. Panic and The Omni Group, just to name two boutique development companies, were probably at their peak in terms of desktop software. Besides, Mac OS X Tiger, Leopard, and Snow Leopard were polished and the UI was usable and cohesive.

Right now, the quality and attention to detail have plummeted. There is also a lot of iOS-ification going on. I wish they focused less on adding random features, and more on correctness, efficiency, and user experience. The attention to detail of UI elements in e.g. Snow Leopard, with a touch of skeuomorphism and reminiscent of classic Mac OS, is long gone.