For those curious, the link is at github.com/pmbanugo/tina

GitHub star history for https://github.com/pmbanugo/tina

2 weeks after public release, Tina is gaining some eyeballs. if you haven't already, check it out — don't say I didn't tell you :)

I'm currently working on adding a HTTP lib extension, and in the process decided I had to change some things at the core for better socket handling.

If you are building servers or infrastructure systems that simply cannot fail, I'd love your architectural critique.

Check out the code, the docs (work-in-progress), and run the examples here:

github.com/pmbanugo/tina

demostrate the core unit of execution in Tina

Instead of coloured functions or promise hell, you write Isolates (They don't block nor await).

An Isolate receives a message, updates its state, and returns an Effect (Yield, Receive/Reply, IO, Crash) to the user-space scheduler.

shows the three foundations of Tina

The architecture maps directly to the hardware constraint:

1. The Shard (Cell): 1 OS thread pinned to 1 CPU core.
2. The Isolates: lightweight processes representing a unit of concurrent execution.
3. The Grand Arena: A single memory block, partitioned at boot.

shows the major things the framework rejected, and how it works around them.

I achieved this by strictly limiting what the programmer can do. Architecture constraint solves problems better than language features.

So I chose these constraints:

🚫 No Garbage Collection.
🚫 No async/await.
🚫 No Mutexes.
🚫 No hidden allocations after boot.

comparing Tina to Erlang/BEAM, Seastar, Tokio

Software engineers usually have to compromise between speed and safety.
You get the BEAM’s "let it crash" reliability, but pay with VM/GC overhead. Or you get C/Rust speed, but fight mutexes and async/await fragmentation.

Tina was built to reject this compromise.

shows the pillars of the Tina framework, and the compromise it rejects

What happens when you combine Erlang-style concurrency + ScyllaDB's Seastar speed + deterministic simulation?

Meet Tina: A strictly bounded, fault-tolerant, thread-per-core concurrency framework. 🧵👇

I like this reflection. Quite an interesting post.

Why? Does it hold if you’re pro vs anti coding agent?

Looks beautiful

Why Queues Don’t Fix Overload (And What To Do Instead) Why adding Kafka or bigger queues won't save your server from traffic spikes. Learn the physics of backpressure, load shedding, and the latency death spiral.

Why Queues Don’t Fix Overload

My Saturday musing, published as a blog post
pmbanugo.me/blog/why-que...

Do you agree?

AI coding accelerates software pollution and further advances bad education on what it takes to make software

Just as ppl expected the increase in software performance with 5 - 20x hardware performance decades ago. They’re doing a similar thing with AI - better hardware & models

💜🫂

My current experiment is around stealing some ideas from the BEAM and combining with some from Seastar (C++ framework)

Hopefully it comes out good enough for me to share it publicly.

Imagine-> BEAM (fault-tolerance) + Seastar (Shards) = 💭

In programming reliable software systems, first you make them correct and fault tolerant, then you make them fast.

Elimination is a core part of software optimisation. But it also carries over into other areas of life.

If you can eliminate, thereby reducing the amount of task or functions you would like to do, you have enough memory space to juggle the vital few

Building a Formal Verification Tool from Scratch A deep dive into building a TLA-based formal verification tool from scratch. Learn systems programming, virtual machines, parsers, compilers, and formal method by building a real tool.

Most bugs exist because we only test scenarios we thought of.

What about the ones we didn’t imagine?

I’m building a formal verification tool from scratch and documenting everything — parser, VM, state-space exploration.

You can follow along in my journey:

pmbanugo.me/series/forma...

Series | Peter Mbanugo - Consultant, Trainers, and Programmer Curated multi-part article series on DevOps, JavaScript, and software development

I've got some blog post series if you want to follow my journey into building a compiler and virtual machine, along the line learning about formal method and TLA

MOre info at pmbanugo.me/series

Series | Peter Mbanugo - Consultant, Trainers, and Programmer Curated multi-part article series on DevOps, JavaScript, and software development

I've got some blog post series if you're looking to learn about single-producer, single-consumer queue

MOre info at pmbanugo.me/series

Thank you

Thanks

Congrats. I hope to be a GDE like you some day

Besides stacks/queues, Are there data structures or algorithms in it that are fundamental to making a compiler and VM?
I’m curious about compilers and VM and currently figuring out how they work and how to make one.

Speculations about Web Performance - Barry Pollard - performance.now() 2025 YouTube video by Web Conferences Amsterdam

I also talked about prerender until script (and other improvements to the Speculation Rules API!) a few months ago at @perfnow.nl , so if you prefer your learning though video (and can put up with my um's and err's) then you can check that out here:

www.youtube.com/watch?v=DqE9...

Adapting old programs to fit new machines usually means adapting new machines to behave like old ones.
—Alan Perils

It was a great exercise in translating theory into a Data-Oriented implementation.

Check out the repo here: github.com/pmbanugo/fab...

hashtag#DataStructures hashtag#Learning hashtag#Coding hashtag#Odin hashtag#ComputerScience

implemented the algorithm in Odin as part of my deep dive into Data Structures and Algorithms.

𝗧𝗵𝗲 𝗧𝗟;𝗗𝗥:
Binary Fuse Filters use a peeling algorithm to compress data down to theoretical limits. The implementation achieves:
✅ ~9 bits per entry
✅ 0.4% False Positive Rate
✅ Branchless query logic

Turning academic papers into working code

I recently dove into the paper "𝘽𝙞𝙣𝙖𝙧𝙮 𝙁𝙪𝙨𝙚 𝙁𝙞𝙡𝙩𝙚𝙧𝙨: 𝙁𝙖𝙨𝙩 𝙖𝙣𝙙 𝙎𝙢𝙖𝙡𝙡𝙚𝙧 𝙏𝙝𝙖𝙣 𝙓𝙤𝙧 𝙁𝙞𝙡𝙩𝙚𝙧𝙨" by Graf and Daniel Lemire. I wanted to understand how we can store millions of keys efficiently in memory without the overhead of standard hash tables or Bloom filters.🧵

Building a Formal Verification Tool from Scratch: Part 1 (Die Hard Edition) What if you could explore every possible timeline of your distributed system to find the bugs you haven't imagined yet? I'm building a TLA model checker from scratch to understand how formal verificat...

I used the Die Hard water-jug puzzle to understand model checking, by building a naive solver.

I only defined the rules; the strategy emerged from exploring every timeline/state.

That’s why formal verification catches bugs tests miss.

Part 1: pmbanugo.me/blog/tla-for...