Remember why you started

I think that it’s extraordinarily important that we in computer science keep fun in computing. When it started out, it was an awful lot of fun. Of course, the paying customers got shafted every now and then, and after a while we began to take their complaints seriously. We began to feel as if we really were responsible for the successful, error-free perfect use of these machines. I don’t think we are. I think we’re responsible for stretching them, setting them off in new directions, and keeping fun in the house. I hope the field of computer science never loses its sense of fun. Above all, I hope we don’t become missionaries. Don’t feel as if you’re Bible salesmen. The world has too many of those already. What you know about computing other people will learn. Don’t feel as if the key to successful computing is only in your hands. What’s in your hands, I think and hope, is intelligence: the ability to see the machine as more than when you were first led up to it, that you can make it more.

Read More

On Equality

One of the most fundamental notions in type theory is equality. There are various forms of equality, including propositional equality, judgmental equality, typal equality, extensional equality, intensional equality, path equality (a key concept in homotopy type theory), among others. The list goes on, and any deep exploration of the concept of equality could easily expand to book length. Instead of attempting to cover all these notions at once, I believe it’s best to build this blog post incrementally.

Read More

20 Films That Inspire, Teach and Move

Inspired by Satyajit Ray’s Deep Focus—a compulsory reading at FTII Pune and NSD Delhi—I was struck by the depth and nuance with which Ray analyses his favourite films and directors. This led me to finally compile a list of my own 10 (+10) favourite films. However, I soon realised that rather than ranking them purely on cinematic merit, my choices were more personal—a reflection of the life lessons they offer.

Read More

Solving Monty Hall with the List monad (or Probabilistic Programming)

Continuing from my Bayes Theorem-based blog post on solving the Monty-Hall problem, I will now show a rather elegant way to model the solution that exploits the humble List monad. To remind the reader, the Monty Hall problem involves a contestant initially choosing one of three doors, hoping to find a car behind it. Monty Hall then opens a different door, revealing a goat, and asks the contestant if they want to switch their initial choice. The goal of the solution is to guide the contestants to make this switching choice such that they have a higher probability of winning. This post was inspired by a less-than 100 lines implementation of a probabilistic programming monad in Haskell

Read More

The Monty Hall Problem and Bayes Theorem

Today, while reading Steven Pinker’s latest book on critical thinking, Rationality, I was scribbling a solution to the Monty Hall problem. The Monty Hall problem is probably one of the most well-studied pop-science problem statement with different intuitive explanations of the solution. In case, dear reader, you have been living under a rock here is the problem statement:

Read More

Overleaf submission to arXiV

After scouring through the entire web for close to 5 years and giving up out of sheer frustration every time, I was finally able to upload my TeX sources to arXiv (as of 17.01.2024). The solution was buried as a comment to one of the lesser upvoted answers in a less popular StackExchange thread. I hope Google will push this post high up so that it can help Overleaf (and minted) users.

Read More

Unfolding Fix

In pure lambda calculus (untyped or typed) the fix combinator is used to encode recursion. fix represents the least fixed point of a function f i.e the least defined x for which f x = x. An important concept is that a function need not have a least fixed point. But for those functions which do, the least fixed point is the base case for recursion. An intuition about the least fixed point is :

Read More

Understanding the Transactional Nature of Smart Contracts

In this post I attempt to summarize my understandings about the transactional nature of Smart contract execution. I conducted this study, while trying to understand the DAO exploit. The basis of the DAO exploit is a recursive(or rather reentrant) message call. One important point to note that an exception(during a message call or otherwise) in the Ethereum Virtual Machine , would imply reverting all changes to state and balance. Solidity has a documentation on cases where exceptions are thrown automatically. However in certain cases like send we need to manually raise an exception using throw. So, the attacker has to be careful not to hit any exceptions while attempting the reentrant call to avoid reverting. I also rectify certain mistaken assumptions, I made in my previous post.

Read More