nextos

Yes, and the EU, due to this fragmentation, seems to be a fertile playground for all this unacceptable interference by foreign powers.

I think we really need to use sandboxes. Guix provides sandboxed environments by just flipping a switch. NixOS is in an ideal position to do the same, but for some reason they are regarded as "inconvenient".

Personally, I am a heavy user of Firejail and bwrap. We need defense in depth. If someone in the supply chain gets compromised, damage should be limited. It's easy to patch the security model of Linux with userspaces, and even easier with eBPF, but the community is somehow stuck.

Exactly, that's the way forward.

There are lots of old ideas from evolutionary search worth revisiting given that LLMs can make smarter proposals.

AFAIK, it's a bit more than hyper-parameter tuning as it can also make non-parametric (structural) changes.

Non-parametric optimization is not a new idea. I guess the hype is partly because people hope it will be less brute force now.

I guess this depends on the problem at hand.

But I was thinking about a typical hierarchical model with partial pooling and standard weakly informative priors.

These days, the advantage is that a generative model can be cleanly decoupled from inference. With probabilistic languages such as Stan, Turing or Pyro it is possible to encode a model and then perform maximum likelihood, variational Bayes, approximate Bayesian inference, as well as other more specialized approaches, depending on the problem at hand.

If you have experienced problems with convergence, give Stan a try. Stan is really robust, polished, and simple. Besides, models are statically typed and it warns you when you do something odd.

Personally, I think once you start doing multilevel modeling to shrink estimates, there's no way back. At least in my case, I now see it everywhere. Thanks to efficient variational Bayes methods built on top of JAX, it is doable even on high-dimensional models.

> I’ve never personally worked on a problem that I felt wasn’t adequately approached with frequentist methods

Multilevel models are one example of problem were Bayesian methods are hard to avoid as otherwise inference is unstable, particularly when available observations are not abundant. Multilevel models should be used more often as shrinking of effect sizes is important to make robust estimates.

Lots of flashy results published in Nature Medicine and similar journals turn out to be statistical noise when you look at them from a rigorous perspective with adequate shrinking. I often review for these journals, and it's a constant struggle to try to inject some rigor.

From a more general perspective, many frequentist methods fall prey to Lindley's Paradox. In simple terms, their inference is poorly calibrated for large sample sizes. They often mistake a negligible deviation from the null for a "statistically significant" discovery, even when the evidence actually supports the null. This is quite typical in clinical trials. (Spiegelhalter et al, 2003) is a great read to learn more even if you are not interested in medical statistics [1].

[1] https://onlinelibrary.wiley.com/doi/book/10.1002/0470092602

Find recruiters within your niche on LinkedIn.

In the UK, lots of jobs tend to be filled in via recruiters, and they are quite helpful.

I recommend you contact your local data privacy office, as they usually take this quite seriously.

Fill in a formal complaint and watch the slow but inevitable unfold.

It's interesting Lean is taking off in software engineering. Prior to the advent of LLMs & agents, Lean had almost zero use in software and was mostly focused on mathematics, with Isabelle and Rocq leading the way here. In fact, I asked Kevin Buzzard and others in the Lean community, and they simply shrugged.

The exception was [1], a Lean-based text heavily inspired by Concrete Semantics [2], a cornerstone of Isabelle literature. The latter is, in essence, Winskel's classic semantics book [3], a standard textbook in programming language theory, with all proofs mechanically checked.

More broadly, I'm wondering whether dependent types are the right abstraction or too powerful and heavy for humans to review and make sure specifications are aligned with intent. I've been working on automation for this for more than a year, and I've found refinement types sufficient and much easier to review.

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

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

[3] https://direct.mit.edu/books/monograph/4338/The-Formal-Seman...

Not just TDD. Amazon, for instance, is heading towards something between TDD and lightweight formal methods.

They are embracing property-based specifications and testing à la Haskell's QuickCheck: https://kiro.dev

Then, already in formal methods territory, refinement types (e.g. Dafny, Liquid Haskell) are great and less complex than dependent types (e.g. Lean, Agda).

Is SAT/SMT and theorem provers solving yesterday's problems 1.12% better?

Lots of the successes by LLMs that have been much celebrated rely on these.

Something remarkable and unsettling is how the age verification debate has popped up almost simultaneously in the US, UK, and EU.

With the same logical fallacies. Pretty telling about how transnational lobbies and their interests work.

Controlling what children do online is a solved problem: Parenting and parental control applications.

What configuration on the ThinkPad?

In the US, cheap ThinkPads like E14 sometimes sell for a bit less when you factor in all typical discounts. They are good machines that run Linux well and can be repaired.

In EU, and I imagine other markets, there's nothing remotely close. I hope this puts some pressure on Lenovo and the rest of manufacturers to be more competitive.

For instance, under Yann's direction Meta FAIR produced the ESM protein sequence model, which is less hyped than AlphaFold, but has been incredibly influential. They achieved great performance without using multiple alignments as an input/inductive bias. This is incredibly important for large classes of proteins where multiple alignments are pretty much noise.

CSP and Hoare logic were brilliant. He was a huge proponent of formal methods.

He famously gave up on making formal methods mainstream, but I believe there will be a comeback quite soon.

On generated code, verification is the bottleneck. He was right, just too early.

It was edited again a few minutes ago and now displays Sunday, March 8th as his date of death.

There is very little information around, this is the most authoritative post I could find. There are some comments on X as well.

According to this blogpost, he sadly passed away last Thursday, March 5th.

I agree. The formalization is very impressive even if we consider it was done on a result that is already accepted as true and got a lot of help from humans to scaffold and build the structure.

Jeremy Avigad has discussed this in a short preprint [1]:

Gauss’s success was built on almost two years of creative work, scaffolding, and planning by the human participants, and it would have been unfair to them, mostly early-career researchers, to advertise this as solely a success for AI. A bigger concern was that the company would proclaim the project “done.” The formalization, on its own, is close to worthless, since the correctness of Viazovska’s result was never in doubt.

It looks like the formalization process of this result is a very interesting case of human-AI cooperation. I am very positive about the same kind of cooperation in software engineering, given that proofs = programs. Lots of boring stuff can be automated, making formal methods cheap enough to become widely used.

I said this here two or three years ago and I received some interesting feedback, but in more mainstream venues people thought this was nuts. With a quirky homebrewn setup, including a fine-tuned LLM for Isabelle/Dafny, I have been able to reduce my formalization time by a factor of 5-6.

Some minimal formalisms are needed anyway even in case you are not interested in high quality assurance to make sure agents synthesize mostly correct code. IMHO, purely neural agents are much less useful than advertised without some symbolic guardrails.

[1] https://www.andrew.cmu.edu/user/avigad/Papers/mathematicians...

Lean and Coq might not be the right choice. Perhaps something like Dafny, F*, or Why3, where code and theorems live together.

Nevertheless, Lean 4 has closed the gap and it's closer to those than Coq at this stage.

Not surprising, as Dafny is a bit less expressive (refinement instead of dependent types) and therefore easier to write. IMHO, it hits a very nice sweet spot. The disadvantage of Dafny is the lack of manual tactics to prove things when SAT/SMT automation fails. But this is getting fixed.

Formal specifications can be easier to write than code. Take refinement types in Dafny, for example. Because they are higher-level, you don't need to bother with tedious implementation details. By shifting our focus to formal specifications rather than manual coding, we could possibly leverage automation to not only develop software faster but also achieve a higher degree of assurance.

Of course, this remains largely theoretical for now, but it is an exciting possibility. Note high-level specifications often overlook performance issues, but they are likely sufficient for most scenarios. Regardless, we have formal development methodologies able to decompose problems to an arbitrary level of granularity since the 1990s, all while preserving correctness. It is likely that many of these ideas will be revisited soon.

There are incomplete parsers that cover most of the Org basics. For example, GitHub has one, crafted in Ruby. They use it to render e.g. readme.org files in repositories. It works quite well. I find the Org format very pleasant to work with.

I think the trick with Emacs and Org is to stick to the basics and then only add features or change your configuration very slowly, as needed. I have been using Emacs non-stop for >20 years and my .emacs is just 20 LOC. It's been shrinking, not growing. My goal is to bring it down towards 0 LOC. I have committed a few things upstream to modernize defaults.

Personally, I think the reputation of Org, Emacs, or Nix being hard and complex is undeserved. It's rather a documentation problem. There's no simple documentation to onboard newcomers and show them the basics in a principled way. So it looks like a mess, but it isn't.

There are many classical theorem provers that use simple type systems, e.g. Isabelle. Mizar is even weakly typed.

As a heavy user of formal methods, I think refinement types, instead of theorem proving with Lean or Isabelle, is both easier and more amenable to automation that doesn't get into these pitfalls.

It's less powerful, but easier to break down and align with code. Dafny and F* are two good showcases. Less power makes it also faster to verify and iterate on.

In EU/UK, some are sadly app only. I avoid those. Many others are pushing apps as a 2FA, even if you use their website. You need to insist to get another authentication system, like TAN. Some governments are also pushing mobile IDs.

The best Linux for phones, SailfishOS, has a fairly good Android compatibility layer that runs many bank apps well. But despite that, it's an uphill battle. The network effect of the duopoly is gigantic.

If verification is the goal, but you don't want to learn theorem proving yet, Dafny is really approachable and practical [1]. F* is also worth considering as a proof-oriented alternative to Isabelle that is focused on software verification [2]. Why3, Rocq and Agda are other obvious contenders.

[1] https://dafny.org/latest/OnlineTutorial/guide

[2] https://fstar-lang.org/tutorial

Lean is great, but if someone's primary interest is SWE, I think there are better choices. The Lean community is primarily focused on formalizing mathematics right now. This might change in the future. Lean is nice to learn theorem proving, but once you learn the basics, you'll hit a roadblock when trying to move to software verification applications.

For SWE, the most mature option is probably Isabelle. It's also a classical theorem prover, and it's perhaps easier to start with something that doesn't have dependent types. A cool thing is that the canonical Isabelle book [1] has been rewritten in Lean [2].

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

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