From "Kundalahalli Is Not Kundalahalli Gate" to "LGTM Is Not a Theorem" :: Reflections on IndiaFOSS 2026

This blog has been on my to-do list for a while now. It has been a month since I went to IndiaFOSS, and I could finally finish it thanks to my retreat at the Isha Foundation in Coimbatore, and to two days of an Instagram-free life that let me collect all my thoughts and put them into a document in less than a day.

Let me hang some really dirty clothes out to dry before I begin. At JEC (Jabalpur Engineering College, where I did my undergrad), most of us had missed out in JEE, and largely believed there were only two ways to redeem ourselves: a great GATE rank or CAT percentile. So if I finished 9000th in the CodeChef monthly long challenge, I basically sucked, and my options were GATE, CAT, UPSC or Bank PO. Failing that, I could hope that Infosys Mysore would take me in, put me up in an exotic hostel and run me through six months of training, or disaster management. It was my seniors Mayank Kumar Sharmareference for Mayank Kumar SharmaMayank Kumar Sharmalinkedin.com/in/mayanktg and Saransh Jainreference for Saransh JainSaransh Jainlinkedin.com/in/saranshjain1 who introduced me to the words “open source”, to the shocking news that there is a huge world outside Yashavant Kanetkar’s Let Us C, and to the groundbreaking idea that not everything in life has to be a competition, a rank or a score. Knowing DFS is essential, knowing max flow is great, and the fundamentals of coding are crucial. What matters far less is whether your code runs in $n^{2.75} + c$ or $n^2 + c$, or whether you can print “Hello World” in C without a semicolon, swap two numbers with bitwise tricks, or pull off any other party trick that needs arcane knowledge of the language. Armed with this new worldview, I opened Mozilla’s Gecko codebase, because it was in C and C was the only thing I knew (yes I thought I knew C, I was young and pretty stupid), and I swear to the Almighty (and I am a very theist guy) that giant piece of code did not look like C at all.

So in 2015, Vipul Sharmareference for Vipul SharmaVipul Sharmalinkedin.com/in/vipul20 and I took the train to Bangalore for PyCon India. I had installed the Python REPL a whole week before, so naturally I was ready. Vipul, on the other hand, was the real deal, and he will absolutely hate this sentence when he reads it. He is the most intuitive coder I have ever seen. It genuinely does not matter to him whether he is writing Python, C or Java, and he had been Tkinter-ing (pun very much intended) for some time already. After reaching Bangalore, we had to get down at Kundalahalli (which, for the uninitiated, is very different from Kundalahalli Gate) and stay at Apoorv Anandreference for Apoorv AnandApoorv Anandlinkedin.com/in/apoorvanand Sir’s apartment. He was working at $\mu\sigma$ back then, which in JEC parlance $\equiv$ Google. (Remember this equivalence, because it will matter. Somewhere out there is a man whose résumé has both Mu Sigma and Google on it, someday I will write about him as well. In the first chapter of the first Harry Potter book, Hagrid casually mentions borrowing a motorbike from “young Sirius Black”, and nobody thinks twice about it until book three. Consider this as my “young Sirius” moment. Clever writing, you see.) That PyCon was my first real exposure to the idea that you don’t need to be from a big name to contribute to open source. It sounds naive now, but until then the idea of making our engineering lives better had simply not crossed our minds.

Fast forward eleven years. Same venue, the NIMHANS Convention Centre, except this time I was the one on stage giving a talk at IndiaFOSS, and I will admit it brought me more joy than I expected. Vipul came along again, this time paying the full price and no student discount, now a founding engineer at a Bangalore startup. On day one I ran into Apoorv Anand Sir, still the same guy the college girls used to post about anonymously, and the circle closed. I mean closure in the mathematical sense: apply the operation as many times as you like and you still land inside the same set. A few cities, a few countries, a few continents, a few jobs, a PhD, and yet the set of people had not changed. The same people who watched the journey begin were standing in the same set. Mathematically sound, completely bizarre. Whoever is writing the story starring Durwasa Chakraborty is doing an amazing job. Forever greatful. :) :)

First Reflections

#

Many students wanted to know more about my area of work. A couple of them told me they had read my post on how agentic LLMs almost destroyed my academic career and shared it in their college group. I really did not expect that! (You have no idea what that means to my broken self-esteem :’) :’) )

Almost every talk had some AI angle or buzz around it. The other thing that stood out was how much interest there was in hardware, and Vipul had the best explanation for it. He has built a career in software engineering, but these days, he says, we are mostly prompting, and for builders tinkering with hardware is one of the few things that still feels a bit organic. That is where the joy is coming from now. I could not agree more, and I count myself among those builders. I hope to build a music player or a keyboard from scratch, from the microcontroller up. For now, at least for a year, both stay on the back burner.

From the Main Track

#

COSH, by Prof. Mohit P. Tahilianireference for Prof. Mohit P. TahilianiProf. Mohit P. Tahilianilinkedin.com/in/mohittahiliani (watch). I am glad I attended this talk. In 2013, as a new faculty member at NITK Surathkal, Prof. Mohit kept wondering why students stayed in the club room till 1 a.m. but submitted course projects at the last minute. Becoming a GSoC mentor for ns-3 in 2016 changed how he wrote course projects, and for about ten years now his students have earned marks for real open-source contributions. That grew into the Centre for Open Source Software and Hardware (COSH): a campus of 40,000 devices moved to IPv6 by students, a packet scheduler merged into Linux 5.6, and even the IndiaFOSS WiFi set up by his students. I strongly share his view that the open source revolution, and (personally) really the free software revolution, should be taken forward by India and Indians. I could not resist and next day asked him how a course that rewards students for opening PRs avoids Hacktoberfest-style PR spam. He kindly explained the two-tier strategy he uses to keep NITK’s name from being diluted. As someone who aspires to become a teacher there are pages I can borrow from the book or might as well just borrow the whole book.

Textbooks that run, by Prof. KC Sivaramakrishnanreference for Prof. KC SivaramakrishnanProf. KC Sivaramakrishnankcsrk.info (watch). KC sir’s NPTEL OCaml course has 2,000+ students, many without a computer of their own, so he wrote a book that runs entirely in the browser: no install, live type errors, quizzes, and a full Linux VM booting in a tab. I really enjoyed this one. The next day my friends were still discussing lightweight VMs in browsers, WASM, compiling X to Y. What I loved most was his idea that books should evolve. That should be the only point of making books digital: you dive deep into the topics you want, and the book gives you an interface for it.

Digitisation should not just mean “hey, here is an iPad, it is easier to carry”. Nor should it mean that the Kindle does not smell like a book, so you spray old-book perfume on the screen. At that point I might as well buy the book. The one honest argument I have seen for plain digital copies comes from my father. He retired as a proud Chief Engineer and has written two books, including Jab They Met, which you can buy (shameless plug). All he wants is reviews, not money, and he found that the free Kindle edition (free because there is no production cost) serves that purpose perfectly. Over evening tea, on much the same theme, Prashant Singhreference for Prashant SinghPrashant Singhlinkedin.com/in/prashant-singh-030159177, a PhD student with Prof. Rupesh Nasrereference for Prof. Rupesh NasreProf. Rupesh Nasrecse.iitm.ac.in/~rupesh, made an interesting point: in this age of chasing validation and feedback, a shrinking stack of unread pages gives you a satisfaction that a PDF cannot. Sure, the screen says 56% complete, but it is not the same feeling. I agree.

So yes, books need to evolve. When I read about entropy, I should be able to find out that Rudolf Clausius coined the word in 1865, that Sadi Carnot’s paper on heat engines came out in 1824, and that Thomas Newcomen had built the first practical steam engine back in 1712.^{Click for more†} I should control the flow: decide how deep I go, and at an opportune moment say “okay, enough depth-first search, let’s go back”. Books should be interactive. Of course, Prof. KC is my guide, and my guide is better than your guide. But honestly, the whole presentation was great: the humour, the cool-factor and as someone pointed out the boldness to attempt live coding inside a slide deck.

The future of FOSS, SWE and technical education, a panel moderated by Ansh Arora with Kailash Nadh and others. I liked this one a lot. It addressed some pressing issues, especially junior hiring, and came with very good, pragmatic solutions.

Telling India’s story through data, by Rukmini S. Rukmini is a Chennai-based journalist and the author of Whole Numbers and Half Truths, and the talk was very informative. Her line was that working with Indian data is not about trust but about reading closely. A crime rate “jumps” because the denominator quietly changed in a footnote, and 1.2 billion SIM cards still leave one in five women without a phone. Statistics can so easily be used to hide the truth, and that is something I personally care about deeply.

Offline-first mobile apps on Frappe, by Deepak Batra. recording Like the foundational idea of I am burning my tokens so that you don’t have to. Their users are field workers with entry-level phones and one bar of signal, and as he put it, “the field is the most honest code reviewer: it doesn’t file a bug report, it just stops using your app.” Frappe already treats a form as data rather than code, so their open-source Flutter SDK has the phone read the same form definition from the server and keep working offline.

The Programming Languages and Systems devroom

#

My talk was in the Programming Languages and Systems devroom, and the whole devroom is on YouTube with chapters for every talk. The devroom managers were Pradeep and Ashutosh Pandeyreference for Ashutosh PandeyAshutosh Pandeylinkedin.com/in/ashupdsce from LLVM Social Bangalore. They are the people right now, and they even got a shoutout from Google (not that we need Western scholarship to appreciate great work, but yeah, it is kind of a big deal). A disclaimer: some of these ideas are not captured verbatim. That is entirely down to my inability to have a sumptuous lunch and then not doze off while the convention centre AC runs at full capacity.

Semantic Quantization in KV Cache Eviction, by GiGi. The idea is to evict KV cache entries using only the key and value tensors already in the cache, so open models can run on a laptop without hitting OOM. Whenever I hear the word “tensor” my ability to visualise the engineering takes a hit, but the JPEG analogy landed: you lose the fine detail but keep what the image means. I came away with PyTorch SDPA and PagedAttention on my reading list.

Bend, Don’t Break, by Anupam Jain. This was more up my alley: strongly typed functional programming, with strong head nods from the audience (Haskell folks, I tell you!). It answered the classic industry complaint, that changing x to xButCooler means changing it everywhere, with a few jabs at Rust along the way. The division example, asking for a NonZeroInt instead of returning a Maybe, showed how types turn the argument around. The whole game of languages is saying precisely what you want to do. A very nice getting-started video for functional programming and types.

Databases in Ethereum Nodes and PeerDAS, by Sudeep (Erigon) and Agnish Ghosh (Nimbus). ETH is still a huge interest of mine: it is Turing complete, and it is the reason I fill in a different tax document every year for owning a very insignificant amount of it. Honestly, the Reed–Solomon bit parity in PeerDAS went over my head. But “how do you store the history of a world computer” and “how do you know the data exists without downloading all of it” are exactly the two questions I want to go and read about.

Benchmarking Can Be Hard, by Navaneethreference for NavaneethNavaneethlinkedin.com/in/navaneeth-nambiar. The first FP Launchpad talk, like Horatio’s entrance in Hamlet: the friend who shows up in the first scene and sets the tone for everything after. Run the same Java pipeline a few times and JIT warm-up, GC, E-cores, throttling, ASLR and even the season move the numbers. Performance is a distribution, not a number. OCaml 5’s old benchmark suite had drifted away from real workloads, and the new one is meant to let people upstream GC and compaction work with confidence.

What LLVM Does Differently When the Target Is CPU vs GPU, by Bhuvan. It starts with a plain if on threadIdx, which a GPU warp ends up running both sides of, and goes on to divergence analysis, address spaces and occupancy. Anyone taking a GPU course at undergrad or grad level must watch it. It assumes you know what a pass is, but beyond that a lot is packed into 15 minutes.

PythonBPF, by Pragyanshreference for PragyanshPragyanshlinkedin.com/in/r41k0u and Varun. Ordinary decorated Python compiled to eBPF through LLVM, and my favourite talk of the devroom. It had FOSS smeared all over it: the modus operandi and even the way things were discussed felt very SIG-like (as the k8s folks would say), and the demo was Snake running inside the kernel. Of course, I am also trying to stay or buzz in the good books of a Canonical developer who shares my space-time continuum (he literally sits next to the lab), but credit where it is due: great presentation skills by Varun and Pragyansh. After the event, Vipul and Varun had a great conversation about something we are not allowed to print (redacted, but some ultra nerdy things) :lol:

LGTM Is Not a Theorem, by yours truly, and the boldness to go after Pragyan and Varun warants an award but I would really appreciate it if you watched the video. More on it below.

One Language, All GPU, by Shreyas Hegdereference for Shreyas HegdeShreyas Hegdelinkedin.com/in/shreyas-omkar. A beautiful talk on how one Julia kernel compiles to CUDA, ROCm, oneAPI and Metal. I remember the Julia folks from MIT holding community gatherings in Boston cafés, and having worked at MathWorks I have a soft spot for languages of the scientific community. The line that stuck was “portable does not mean hardware-blind”. For first-year students looking for a language community to grow up in, I would highly suggest Julia (or, well, OCaml). Feature requests there are driven by real scientific pull, not popularity, and that is more academically rewarding than JavaScript or Python or… C++.

Rust Is Not an HDL, So I Built a Tiny One, by Afnan. I do not understand much Rust, which seems like blasphemy in this day and age when everyone says the borrow checker is the new cool. Luckily this talk was less about Rust and more about humility. Afnan, an AI and web developer and startup founder, met Verilog through a friend, decided he could write his own, and then, in his words, got humbled about five times. That turned into Frag, a tiny hardware description language. You write a half adder as typed bits, and it hands back a truth table, a dataflow diagram, waveforms and Verilog. That last part is a gift to anyyone who had to memorise truth tables for an exam.

So what was my talk about?

#

It was about program verification: LGTM Is Not a Theorem: Pragmatic Verification and the Economics of Software Confidence (slides). The argument was that green tests and 100% coverage tell you which lines ran, not which states are reachable. Writing down one invariant and trying to prove it finds the bugs no test schedule would. And now that machines can produce the proofs, the economics have shifted in our favour: what is left for us is choosing the right theorem.

I used to have every question that someone without a verification background has today. Isn’t this what tests are for? Who writes proofs for a refund function? Five years at IBM, MathWorks and AWS gave me the answers. I have typed LGTM meaning “I could not find anything wrong”, which is very different from “nothing is wrong”. And every postmortem I sat through was, in hindsight, a missing “something”. On the PhD side I have come to realise that serious programming languages work means producing proofs, or at least some semblance of one. “It worked on my examples” is just the PL version of LGTM.