Alcides Fonseca (english feed)

Z3 Python in the Browser in 10 minutes

me@alcidesfonseca.com (alcides) — Thu, 19 Mar 2026 10:54:00 +0000

Last night, while I was catching up on email, I wanted to make use of my time and our Claude subscription. I decided to scratch an old itch.

Our aeon programming language has Liquid Types (e.g., {x:int | x > 0}) and we rely on an SMT solver to type check the implications of subtyping (e.g., when passing something of type {x:int | x > 3} to a function that accepts {x:int | x > 0}, we need to verify whether x > 3 -> x > 0, for all x).

But there was an issue: aeon is written in Python and relies on the z3 bindings that contain C++ code. We can run Python code in the browser with Pyodide, but the native libraries are not directly supported (at least this one, that relies on multi-threading).

On the other hand, there is a z3 port to web assembly (by alectryon’s Clément Pit-Claudel, no less) but it follows the C API, and has no browser-Python bindings.

So while I went through the ivory tower tall pile of emails, Claude reimplemented the z3 bindings in a different package, used the export to SMT-lib format feature, already present in z3, and passed that to the z3-wasm package.

I asked for examples, and piping the errors I found in the browser back to Claude, I gave up on being a middle man, and instructed Claude to use Rodney to interact with the browser directly (I was running this on a linux server, not my local machine). It then went ahead and made the examples work on Chrome, in a nice demo page. Unfortunately, it did not work on Safari due to the lack of stack switching support in web assembly, so I needed to make another prompt to fix that issue. It deployed to GitHub and Pipit automatically, with little effort.

Of course you get what you paid for: I provide no assurance that there are no bugs. But it’s useful enough for me to prepare some demos and materials for students that do not require any installation or compilation in their machines. That’s a win in my book.

And now, you have support for z3 in Python within the browser for your existing z3 Python projects, or just to play with z3 because the Python bindings are by far the most easy to just play with.

Needed updates to macOS

me@alcidesfonseca.com (alcides) — Tue, 17 Mar 2026 22:21:19 +0000

How to improve macOS in 5 steps, by Alex Potenza

To be clear: bottom-of-the-barrel Windows laptops, Linux laptops, and Chromebooks can plug into these multi-display docks over one cable. No Mac can, regardless of its price.
Hilariously I have even seen Intel Macs gain MST support once booted into Windows via Boot Camp, which at least suggests software and driver support are and always were a huge part of this story.

1. Add DisplayPort MST support.

Brightness control on non-Apple displays is smaller, but it points in the same direction. A lot of displays support DDC/CI. In plain English, the display already knows how to listen, but macOS behaves as if only Apple’s own displays deserve convenient controls. If a connected display supports standard brightness, the keyboard keys, the menu bar, and Control Center should be able to use it. MonitorControl and BetterDisplay exist because people clearly want this to be native.

2. Add brightness control to non-apple displays. I use both apps (one on my M1 and another on my Intel MacBook pros) for my external LG displays.

What if Apple Intelligence was smart enough to know ‘you’re using these three specific windows from different apps and swapping between them to do this one task’ and intelligently surface those groups of app windows for users. Picture an Apple Intelligence managed better version of Stage Manager where you can easily orchestrate it all from ‘Mission Control 2’. Those are the sorts of features I want from Apple Intelligence.

3. Focus on user tasks, and not application or window-level UI control.

Apple could retire Zoom entirely, make Fill the standard ‘make this window bigger’ action, and have the green button, title bar, and top-edge drag all follow the same model.

4. Bring back old maximize.

udio has gaps too. Per-app volume control should be built into the system, and external audio devices, in particular USB audio interfaces, should be more widely supported from the keyboard and menu bar. SoundSource is useful precisely because it solves both problems at once. The market keeps proving demand for things Apple could and should have built years ago.

5. App-level volume control.

You do the five things, and I won’t consider moving to linux anytime soon. Your move, Apple.

Flickr REST API design

me@alcidesfonseca.com (alcides) — Wed, 11 Mar 2026 17:13:26 +0000

Half of my education in URLs as user interface came from Flickr in the late 2000s.

[…]

This was incredible and a breath of fresh air. No redundant www. in front or awkward .php at the end. No parameters with their unpleasant ?&= syntax. No % signs partying with hex codes. When you shared these URLs with others, you didn’t have to retouch or delete anything. When Chrome’s address bar started autocompleting them, you knew exactly where you were going.

[…]

It was a beautiful and predictable scheme. Once you knew how it worked, you could guess other URLs. If I were typing an email or authoring a blog post and I happened to have a link to your photo in Flickr, I could also easily include a link to your Flickr homepage just by editing the URL, without having to jump back to the browser to verify.

— Marcin Wichary (via Michael Tsai)

The advent of Single-Page Applications (through Angular and React) screwed over the beautiful URL design of the late 2000s, of which Flickr is one of the best examples.

Back then, APIs were designed for the public. But the facebookesque progressive siloing of the internet made big companies stop providing public documentation for most APIs, in order to control the clients (where the money is made).

If only we could solve the monetization of the internet…

Age-verification in Operating Systems and the Internet

me@alcidesfonseca.com (alcides) — Wed, 11 Mar 2026 10:50:02 +0000

The only way to prove that someone is old enough to use a site is to collect personal data about who they are. And the only way to prove that you checked is to keep the data indefinitely. Age-restriction laws push platforms toward intrusive verification systems that often directly conflict with modern data-privacy law.
This is the age-verification trap. Strong enforcement of age rules undermines data privacy.

— Waydell D. Carvalho

To this point, here are some of the recent changes:

Here’s where each of the “All Operating Systems must do age verification” laws are as of today.

- Brazil (Law 15.211) : Signed into law. Requirements in effect on March 17th, 2026.

- California (AB-1043) : Signed into law. Requirements in effect on January 1st, 2027.

- Colorado (SB26-51) : Passed Senate on March 3, 2026.

- New York (S8102A) : In Senate Committee.

Note: As of today, March 4th, Operating Systems developers have only 13 days remaining before the Brazilian law takes effect.

Related: In order to “incentivize” age verification, The Federal Trade Commission (FTC) has announced that they will ignore COPPA violations for software performing age verification.

— The Lunduke Journal

As I have written before, social networks and short videos are a matter of public health. However, I disagree that is a matter of age — this affects adults as much as kids. But let us assume that the liberal side of me wants each and every one of us to make their own decision. Except minors, which are dependent on their guardian’s decisions (the American-centric way) or their government’s decisions (the European way).

The American approach is more suitable for a technologic translation — devices for kids (think iPhone 17e, with underage-mode enabled) require explicit permissions, either à priori, or an interactive prompt to their guardian’s devices.

The European approach is much more difficult — you need to use your government-issued ID certificate to authenticate on the web, which leads to the end of the anonymous internet. I believe this change is coming, but I would like to preserve the 2000s internet as the governance model, especially given how our global village navigates the geopolitical changes of the 21st century.

Regardless, internet websites require a way to asking the age of their users from either the user or the device. Users lie — everyone I know lied on website age checks, even after being 18, out of habit — so device-based checking is being instituted. Apple designed an API on the 26+ versions of their OSes, in response to the law changes mentioned above.

Mandating that operating systems even have accounts is insane. The Facebook dominance of the user-facing internet gives lawmakers the false impression that the whole internet follows the same siloed pattern. But the internet and operating systems are so much more than that: we should have the freedom to design operating systems (and internet protocols) however we like. If I want to design a user-less operating system, I should. Internet protocols should be designed by experts who understand how the internet works, with input from the social sciences to understand the impact.

Yes, we have a problem, but we are law-constraining the wrong things here. It’s like passing a law requiring all knives to have a fingerprint lock to only allow over 16 year olds to open it. Several internacional security and privacy researchers warn against these changes without proof that they have any impact.

A simpler alternative would be for a non-profit or a government authority to create whitelists of websites that are suitable for different age ranges, and let parents configure those whitelists in their kids devices.

But I am sure I can embed an http proxy in our university domain. The bottomline is that there is no technology that can replace good parenting.

Colin Brittain plays From Zero

me@alcidesfonseca.com (alcides) — Wed, 11 Mar 2026 09:18:24 +0000

Today’s work session is brought to you by Colin Brittain playing and talking about Linkin Park’s From Zero, one of my favorite albums from the past two years.

A New Age Software Engineering Degree

me@alcidesfonseca.com (alcides) — Wed, 04 Mar 2026 00:16:44 +0000

What may happen is that software development involves less coding than it has in the past because of AI. At least coding by humans. So BLS is probably right about a decline in the need for computer programmers. At the same time, if software developers spend less time doing actual coding they may have more time for higher level (if that is the right term) thinking and involvement in design. Unless AI starts doing more of that. So maybe we will not need more of them. Or perhaps AI will make it possible for more people to be software developers who wouldn’t be that now. We’ll see I guess.

— Computer Programming or Software Development by Alfred Thompson

Alfred analyses the difference between a programmer and a software developer. AI is replacing programmers (those that implement features identified by software developers), but not Software Engineers.

On the other hand, we might not be preparing our SE students for the next decade. We have good, core CS and Programming courses. But advanced courses are not up to par with what the market needs. This aligns with the Barbell approach, which is the closest I have seen to a good path for our SE education. We need good, pen-and-paper, fundamental courses, and we need up-to-date advanced courses that make use of AI and whatever comes next.

The main problem is that technology is moving faster than Universities can adapt. Most professors are researchers in their own niche, and most are not doing Software Engineering, but they do teach it. We need more cutting-edge engineers to come back to universities to teach.

Here in Portugal, we have incentives not to hire professionals (I am fighting this locally, and got two real-world engineers to teach Functional Programming with me) and our degrees have to stay static for three to four years. This does not work for this day and age when the development process changes so frequently, and professors are so busy to actually get some hands on experience. I am also fighting that, but that’s for some other post.

Scott Jenson on UI innovation

me@alcidesfonseca.com (alcides) — Mon, 02 Mar 2026 10:19:53 +0000

The internet isn't closed as Facebook

me@alcidesfonseca.com (alcides) — Thu, 26 Feb 2026 09:33:44 +0000

Fantastic piece by Mark Nottingham on the future and openness of the Internet!

New applications and networks appear daily, without administrative hoops; often, this is referred to as “permissionless innovation which allowed things the Web and real-time video to be built on top of the network without asking telecom operators for approval

Yes, the internet is a huge, but unlikely success that (I believe) was only possible because it moved faster than regulatory and legislative bodies could understand it.

On the other hand, the Australian eSafety Regulator’s effort to improve online safety – itself a goal not at odds with Internet openness – falls on its face by applying its regulatory mechanisms to all actors on the Internet, not just a targeted few. This is an extension of the “Facebook is the Internet” mindset – acting as if the entire Internet is defined by a handful of big tech companies. Not only does that create significant injustice and extensive collateral damage, it also creates the conditions for making that outcome more likely (surely a competition concern). While these closed systems might be the most legible part of the Internet to regulators, they shouldn’t be mistaken for the Internet itself.

Yes, countries are regulating something that they do not own (the internet), without considering that (critical, public and international) infrastructure’s wellbeing. There are no border controls on the internet, and while I agree there should be regulation and laws on what you can do with the internet, the internet itself (the infrastructure) should not be regulated.

Likewise, the many harms associated with the Internet need both technical and regulatory solutions; botnets, DDoS, online abuse, “cybercrime” and much more can’t be ignored. However, solutions to these issues must respect the open nature of the Internet; even though their impact on society is heavy, the collective benefits of openness – both social and economic – still outweigh them; low barriers to entry ensure global market access, drive innovation, and prevent infrastructure monopolies from stifling competition.

This is where I think Mark is wrong. The unlikely success of the internet is coming to an end, due to the economics of LLM-generated content. If we want the internet to remain open, it should remain open to humans and agents alike. If everyone has an OpenClaw agent running around, they multiply their internet footprint by 1000x or more. ISPs will notice, and change the pricing and economics of the internet. As I warned before, the signal-to-noise ratio will decrease substantially and something alternative will arise from the Internet’s ashes.

The comma trick

me@alcidesfonseca.com (alcides) — Sun, 08 Feb 2026 11:48:19 +0000

As any unix aficionado, I have my own stash of custom commands. At some point in time, I mimicked Pedro Melo’s idea of starting all of them with an underscore, to have a more precise auto-complete.

Fast-forward some years, and in my macOS and ubuntu shell, I have plenty of system scripts that start with one or two underscores, undermining the autocomplete advantage.

Brandon Rhodes proposes to use the comma. Personally, I am not a fan of having a punctuation symbol that has other meaning in programming languages inside a shell that parses input as a programming language (zsh these days). But this is the type of yak shaving that automates your workflows.

Overview of what has been happening to LLMs

me@alcidesfonseca.com (alcides) — Sun, 01 Feb 2026 12:22:31 +0000

It’s impossible to keep up with all the new developments in the LLM-era. However, one thing has been true: they never stopped improving.

Malte Skarupke explains How LLMs Keep on Getting Better, covering a few of the different visible and invisible aspects of LLMs that have been worked on over the past couple of years. It’s a really good overview for those who are not into the weeds of it.