77 Followers
152 Following
819 Posts
OpenBSD Slacker, CS student. Interested in all things BSDs, security, LISP and compilers. From Italy, currently trying to learn Japanese.
Bloghttps://www.omarpolo.com/
Italian Bloghttps://it.omarpolo.com
Gemini Capsulegemini://gemini.omarpolo.com
Honk@[email protected]

‘Luncheon of the Boating Party’ is an 1881 painting by French impressionist Pierre-Auguste Renoir. It is now in The Phillips Collection in Washington, D.C.

It’s going to Paris to the Musée d'Orsay for the major exhibition ‘Renoir and Love: A Joyful Modernity’. The work is on view from March 17 to July 19, 2026.

That same exhibition will move to London in October. Unfortunately the painting will have returned to DC and won’t be in London.

#art #impressionism #Renoir #exhibition #Europe

If you told me in 1990 that a coalition of Opus Dei and Italian fascists were going to platform a gay billionaire Republican to challenge the pope on end-times doctrine, I would conclude that one if not both of us was having a stroke

I'm actually quite surprised at the number of open source repositories using git rev-parse --parseopt for option parsing, even for things that are not Git-related.

I use it in my code because it's a reasonable, portable way to get sensible option parsing in shell scripts in a way that works across shells and OSes. Apparently other people had the same idea.

Despite its looks, the English word ‘heart’ is etymologically related to ‘cardio’, ‘cordial’, ‘to record’, ‘courage’, and even Spanish ‘corazón’.

Through Germanic, Greek, and Latin, these words all derive from a Proto-Indo-European root meaning “heart”.

In Germanic, sound changes that are called Grimm’s Law radically changed its consonants.

Click my new infographic to learn how:

Partner sent me this today and I laughed and laughed and if it wasn't so against my inherent way of interacting with people I would use this all the time irl.

#mutualaidrequest #mutualaid

I don't suppose that I have any #bsd #unix #foss #infosec friends out there willing to signal boost, by chance? ​ 

https://bsd.network/@brynet/114458997143046937

cvs'ing on the go 

This weekend is the perfect time to get your #eurobsdcon submissions done!

The Call for papers https://2026.eurobsdcon.org/cfp/ is open until June 20th, for the conference in Brussels September 9-13, 2026.

We also offer pre-submission guidance/mentoring, see within.

Wonder what BSD and the conferences are about? See https://nxdomain.no/~peter/what_is_bsd_come_to_a_conference_to_find_out.html

@EuroBSDCon #freebsd #netbsd #openbsd #freesoftware #libresoftware #brussels #bruxelles

EuroBSDCon 2026

I love how vibecoded commits are called vommits. It's so perfect.

I accidentally read LinkedIn again and lots of people are talking about the flow of writing code with an LLM and then using a feedback loop with formal verification to reject incorrect implementations.

On the surface, this seems sensible: LLMs can produce kind-of correct (or, at least, correct-looking) code rapidly, verification tools can tell you if it’s correct and you can just keep exploring the design space until you find something correct.

But the bit no one is talking about is: who writes the specification, which must be sufficiently detailed that it can reject incorrect things (including thins in the wrong complexity class, so you don’t accept when the LLM writes a factorial complexity algorithm where a linear one would work)? And why is writing a formal specification believed to be easier than writing code? And what tools can take an arbitrary program and prove that it does or does not implement a spec? If these things were all easy, formal verification would already be ubiquitous.

EDIT: I should say that I am a huge fan of formal verification and wish it were more common. I've worked with folks doing formal verification of a few things that I care about and my experience is that writing a good specification is a similar amount of effort to writing an implementation. Formally verifying equivalence between the specification and the implementation is much more work.

There's some work on LLMs + theorem provers to try to automate this, where you basically give the properties you want to prove and have it fill in the proof. The nice thing here is that the theorem prover will reject proofs that don't work (though you need to be careful that the LLM doesn't introduce new axioms or you end up with ex falso quodlibet issues [any property can be proven if you start with axioms that are false]). But that still requires a specification that captures everything that you care about in the program.