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....
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....
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....
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 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....
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. My slides for the workshop are available here....
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....
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....
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....
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....