Posts

Using Coqtail to setup the Coq interactive theorem prover in Vim or Neovim Besides using Coq in the Coqide or with Proof General in Emacs, you can also set it up on Vim/Neovim with the Coqtail extension. I had some difficulties while setting it up and there weren’t that many resources for it, so I’m documenting the steps here. We’ll have to: Set up Vim / Neovim with Python support Install coq for command line Add the coqtail plugin / setup colors or colorscheme 1. Setting up Vim / Neovim with Python On Vim If you use Vim, you will have to compile it yourself with the --enable-python3interp flag. I haven’t tried this myself because I use Neovim, but this seems to be the way. I found out about the flag from this stackoverflow answer. ...

ChatGPT can help you get non trivial things done. In this case, I wanted to build something that didn’t have much of a precedent that ChatGPT could build on. However, ChatGPT does seem to have some logical abilities (by generating logical looking code). I used it as a second brain and dumped some responsibilities on it so that I could keep my head relatively clear. When building something as non-trivial as a lockfree data structure, there are many edge cases to consider. I went through a process where I pointed out cases to ChatGPT, sometimes suggesting opinionated fixes and giving it outright patches, and sometimes asking ChatGPT to point out these cases itself. ...

This post has my commentary, and a call to action for Element developers, on The Government of India banning Element. In the beginning, the universe was created. This made a lot of people very angry and was widely regarded as a bad move. Then, India banned Element, and it made a lot more people even angrier. My country made another decision that I strongly disagree with. The MEITY – the Ministry of Electronics and Information Technology – banned Element, among 14 mobile apps that they identified as being used by terrorists. It’s a rash decision, and I think it was made without talking to technology experts. It keeps good software away from ordinary people, and doesn’t deter terrorist groups at all. ...

I’ve been recently deploying apps rather frequently on my personal droplet that I use for self-hosting. I tried hosting some bulkier apps and I was surprised when they ran without crashing or bothering any of the other apps that were already deployed. I was impressed by this setup, and I hope that writing this post inspires confidence in others to self-host their own software. VPS Information I have a single $6 droplet and a 50GB volume mounted to it that costs $5. I reckon most people would be able to do without needing that extra 50GB, but I have to mention it for the sake of completeness. ...

I had started with SICP (Structure and Interpretation of Computer Programs) some time early last year. I had read through one and a half chapters and then stopped because it felt too mathematical and I didn’t know what I was getting from it. Then later that year, I attended Lambda Retreat, conducted by Anand, who is my colleague and has found SICP to be quite profound himself. It changed the way I think about programs, added new perspective, and got me interested in the design and implementation of programming languages. I have heard varied opinions from people who have read this SICP. Some feel that it is overrated and for some it changes how they think about programs. ...

Me (left) accepitng a momento from Hadif (right), one of the two NITC students on my team On Feb 11, I conducted a 3 hour introductory workshop on Self Hosting at FOSSMeet ‘23 at NIT Calicut. This post has my notes on teaching Self-Hosting to a crowd and an easy-to-find link for people who land on my personal website. ...

Python’s type system is fascinating. Everything in Python (anything that can be given a name or passed as an argument) is an object. This includes primitives (such as int, str, bool objects), compound objects (made from handwritten classes), and very interestingly the classes or types themselves. This fact that everything in Python is derived from a common base makes it very powerful because any two of these objects can be combined or extended in similar ways. However, the implementation of this idea has consequences. It sometimes gives rise to confusing behaviours that can be hard to reason about if you only understand the behaviour intuitively. ...

I was in the shower and got thinking about how computers encode everything as numbers. Around the time when I was in school and had some familiarity with programming, I didn’t really think it was a good analogy to think of computers as sophisticated calculators. Calculators are dumb, they can only perform operations on numbers whereas computers are able to build something as complicated as the internet. I was younger then. Now I am older and wiser and I can see why “computers are sophisticated calculators” and even appreciate the beauty of what it implies. ...

Web development has an abstraction problem. The low-level implementation details have leaked all the way into code we reguarly write. It’s analogous to writing C or assembly where you need to shape your thinking in terms of the underlying architecture. Good abstractions capture thought ideas with only as much bend as is absolutely needed to eliminate ambiguity. The ideation of a web app is in terms of the content the user can see and the interactions they can make with the website – simple. When it goes to implementation however, the developer has to think analytically and separate what goes into the frontend from what goes into the backend. This feels very artifical and low-level. ...

This blog post tells my reflections on reading Camus’ novel The Stranger. I reference the content of the novel and it is unlikely to make sense to you if haven’t read the novel yourself. For a tl;dr of the novel, I would recommend reading the Wikipedia entry. I’ve never read a novel like this before. There is only a series of events, narrated with a hint of indifference. The murder of a man, Mersault’s separation from his fiance, his death sentence, and of course the death of his mother. None of these incidents were profound enough to throw the man into some odd kind of reflections on his life. He never regretted any of his actions, and as he proved to the chaplain towards the end, he didn’t change his religious beliefs despite much attempt. ...