iiinova — where your digital self keeps evolving

All the listings above come from one source program in Turpentine (a nod to Alan Perlis), a small imperative language, with compilers to twelve of the esolangs. Ten of those are certified: derived from the completeness proofs, correct by construction (but useless).

Malbolge (1998) is the craziest of the bunch: instructions encrypt themselves after executing. Its first program was synthesised in 2000. While its memory is bounded, Malbolge Unshackled (2007) lifts the bound. Its Turing-completeness is open (but my agents are on it).

FRACTRAN (1987) is by John Conway (of Game of Life fame). A program is a list of fractions and the state is one positive integer; at each step, the state is multiplied by the first fraction that yields an integer. It is Turing-complete. This run starts at 239 and halts at 2^42:

Subleq (mid-1990s) only has a single instruction: "subtract and branch if the result is ≤ 0". Since there is only one opcode, it is never written down, and a program is a sequence of address triples (and labels). Some enthusiasts built this architecture in hardware using FPGAs:

In Piet (2002), named after the artist Piet Mondrian, programs are images. The interpreter walks between regions of colour, and the operation it performs is determined by the change in hue and lightness at each boundary. As you've guessed, this picture also computes 42:

100

Whitespace (April 1, 2003) uses only spaces, tabs and linefeeds as meaningful commands; every other visible character is just a comment (great for polyglot programming!). For example, this program encodes 42 in binary and is only 21 bytes in size:

Brainfuck (1993) is, arguably, one of the best-known esolangs and a starting point for many others, thanks to its tiny specification. It is, essentially, a Turing machine in disguise: its eight one-character commands operate on a tape of bytes. Here it is computing 42:

210

Ilya Sergey @ilyasergey.bsky.social · 18/03/2026

As a Programming Language nerd, I have a soft spot for esoteric languages (esolangs), which are built by enthusiasts for fun and to make a point. Over the weekend I started collecting them in Lean, so, please, meet Fantastic Beasts and Where to Find Them, PL edition: github.com/ilyasergey/l... →

$Four dark panels showing the same program in four languages: a Piet painting of coloured pixels, Whitespace rendered as labelled space/tab/linefeed blocks, a FRACTRAN list of 58 fractions, and two lines of Malbolge line noise. A badge in the top-right corner reads "answer := 42".$

162

I knew this is slop, but I wished it weren't.

130

Ilya Sergey @ilyasergey.bsky.social · 23/01/2026

Implementing proof systems in Lean in 2026 be like

010

Ilya Sergey @ilyasergey.bsky.social · 22/11/2025

Had a fantastic week teaching Programming with Proofs in Lean at Neapolis University Pafos. It was great to introduce NUP students to program verification with Veil and Velvet, having many insightful discussions along the way. Excited to see what projects they'll develop next!

Ilya Sergey @ilyasergey.bsky.social · 30/10/2025

Spent the last couple of days porting my program verification class from Dafny to Lean via Loom/Velvet, and it just works! Whenever the SMT solver can’t fully prove a program correct, Lean’s aesop and grind take care of the remaining goals.

180

Ilya Sergey @ilyasergey.bsky.social · 09/10/2025

I am thrilled to announce Velvet: a new foundational multi-modal verifier for imperative programs in Lean. Velvet unifies execution, testing, automated and interactive proofs; and is itself proven sound. 💻 github.com/verse-lab/loom 📄 verse-lab.github.io/papers/loom-...

0134

Ilya Sergey @ilyasergey.bsky.social · 16/09/2025

Just visited YST Conservatory of NUS, the venue for the upcoming FARM concert at ICFP/SPLASH'25. Excited about the upcoming performance combining art, music, and creative programming! 2025.splashcon.org/track/splash...

050

Ilya Sergey @ilyasergey.bsky.social · 06/08/2025

It was a pleasure to host @kcsrk.info who visited NUS earlier this week and talked about some cool systems verification projects done by his team.

Ilya Sergey @ilyasergey.bsky.social · 08/07/2025

It was a great pleasure to host Sebastian Ullrich from Lean FRO at NUS and learn about Lean 4 roadmap and its upcoming module system.

020

Ilya Sergey @ilyasergey.bsky.social · 16/06/2025

In Seoul this week. Just got this delicious local treat from a street vendor.

030

Ilya Sergey @ilyasergey.bsky.social · 11/06/2025

One of the cutest small traditions we have in my research lab is, when travelling, to put a flag of the current location into the Mattermost status.

070

Ilya Sergey @ilyasergey.bsky.social · 04/06/2025

The fact that someone made a one hour video about the flight I take every couple of years and it has been watched 90k times is, probably, a sign that my life is a lot more interesting than I think. (Also, feeling like a jaded survivor in my regular economy class.)

040

Ilya Sergey @ilyasergey.bsky.social · 26/05/2025

When you are asking Cursor to help with a Lean proof, but it is pissed at you.

2162

Ilya Sergey @ilyasergey.bsky.social · 21/05/2025

Jonathan Ragan-Kelley is visiting NUS today, sharing his exciting work on verified user-schedulable languages.

Ilya Sergey @ilyasergey.bsky.social · 20/05/2025

I’ve had a ton of fun participating in the Working Group 2.8 meeting on Functional Programming last week. Those lambdas are in good hands.

1130

Ilya Sergey @ilyasergey.bsky.social · 08/05/2025

Looking forward to visiting MIT CSAIL for the next two days, catching up with the verification folks at PLV and PDOS groups.

Ilya Sergey @ilyasergey.bsky.social · 14/04/2025

This is something we've been working on for a while, and now are thrilled to share. Veil: the first foundational framework that combines SMT-based and interactive proofs about distributed protocols, seamlessly, in Lean! Tool: github.com/verse-lab/veil Paper: verse-lab.github.io/papers/veil-...

1385

Ilya Sergey @ilyasergey.bsky.social · 31/03/2025

I feel that if I published the main paper of my PhD now, it would be received with much more enthusiasm than it has been back in 2012:

130

Ilya Sergey @ilyasergey.bsky.social · 30/03/2025

“Render this in the style of Studio Ghibli”.

1120

Ilya Sergey @ilyasergey.bsky.social · 18/03/2025

According to the GitHub organisation of my research lab, these are the

2141

Ilya Sergey @ilyasergey.bsky.social · 11/03/2025

It was great to have @hilacodes.bsky.social visiting NUS over the past few days and educating us on designing interaction models for program synthesis.

090

Ilya Sergey @ilyasergey.bsky.social · 02/03/2025

About 80% of research internship requests I get nowadays are written in perfect English and don't have any typos.

141

And, last but not least, highlight 4: "A Grounded Conceptual Model for Ownership Types in Rust", OOPSLA'23

150

Highlight 3: "Dynamic Race Detection with O(1) Samples", POPL'23

131

Highlight 2: "Catala: a Programming Language for the Law", ICFP'21

150