UB Hacking 2024

I attended the University at Buffalo Hacking event over the weekend. It was fun. There were 90+ projects, I judged 15 projects. There were some interesting talks as well. It was good to see youth energy. It feels good to teach next generation something.

Another thing,  GeoGuessr played as a group game under time pressure is a lot of fun. This may be a great family activity.

Why should you care about proofs, if all you want to do is coding?

Atri and Andrew decided this would be a good talk to give at a hackathon. Daring!

They did a good job imparting their passion about the joys and benefits of mathematical thinking. They talked about Paul Erdos's the book of proofs concept, and the difference between a  correct proof versus a great proof from "the book". They talked about the deep insight that you can achieve through an abstract mathematical thinking. They also mentioned that if you don't have good insight to the problem or your program, you will have a hard time debugging. I think these parts landed well. 

They also tried to argue that writing proofs and programs are the same thing. I don't know how much of that argument landed on the audience though. It feels like we are getting increasingly more separated from mathematical thinking by new programming languages and trends/approaches.

What happened to writing specifications before you code? Figuring out the specification accurately and writing the specification down precisely would give you the insight into writing the program faster, easier, and often more robust.

Once you make the imprecise problem precise, it is often easy to solve. Writing the specifications down precisely would often lead you to the correct abstractions to use in your development. This reminds me of coding in Functional Programming langugages, especially writing Lisp programs. Once you get your definitions/abstractions in place, writing the rest of the program becomes a breeze, and you also have a flexible powerful framework to address similar problems at hand. This is also surprisingly similar to writing theory papers: once you found your abstractions, and write the model/definitions section well, writing the actual proof is easy. Atri gave an anecdote on this from Jon Kleinberg, and mentioned that he is exceptionally good at distilling things in to an abstract problem, and then his proofs become easy to write.  

Of course I have been touting the TLA+ specifications and modeling horn in this blog every chance I get. Indeed I get a lot of joy and satisfaction when I am able to abstract things down and capture the core insights in TLA+.

A student asked a beautiful question: How do I start with proofs or mathematical thinking? This sounds more of an art than science. 

This was such a great question that I chimed in from the audience. If you follow my blog, you may already know my opinions about this. 

Thinking is not natural. The brain is lazy. It doesn't like thinking hard, because that expends too much energy. Instead it tries to automate things; it recycles tired thoughts, and avoids unfamiliar and uncomfortable territory. 

Thinking hard for distilling insights is hard and unnatural. So my answer is to accept this, and embrace being uncomfortable for as much as it takes to get some results back from your brain. Think about the problem really hard until your brain aches, and until you are uncomfortable and even until you start to dream about the problem.

If you don't have access to a computer or notepad to take notes, the better. That will force your brain the invent abstractions so it can hold the problem in your mind, and make it more manageable to think about the problem. We are now actually taking advantage of brain's laziness in our favor. Having a walk (without any distractions) is a good way of forcing your brain to think about a problem. 

Below is Dijkstra's description of how he invented the all-pairs shortest path algorithm.

"What is the shortest way to travel from Rotterdam to Groningen, in general: from given city to given city. It is the algorithm for the shortest path, which I designed in about twenty minutes. One morning I was shopping in Amsterdam with my young fiancée, and tired, we sat down on the café terrace to drink a cup of coffee and I was just thinking about whether I could do this, and I then designed the algorithm for the shortest path. As I said, it was a twenty-minute invention. In fact, it was published in ’59, three years late. The publication is still readable, it is, in fact, quite nice. One of the reasons that it is so nice was that I designed it without pencil and paper. I learned later that one of the advantages of designing without pencil and paper is that you are almost forced to avoid all avoidable complexities. Eventually that algorithm became, to my great amazement, one of the cornerstones of my fame."

Dijkstra (2001), in an interview with Philip L. Frana. (OH 330; Communications of the ACM 53(8):41–47)

I talked about some of these, with more nuance in a 2018 post: Think before you code!

What I learned about judging a hackathon?

I paired up with Ethan, and we judged 15 groups. Some of the projects were really demoralizing, because you could see that the group didn't think before coding. But 3 or 4 of the projects were uplifting enough to energize us through the judging. 

There was a group that developed a sexual abuse detection app. It used text as input (assumed speech to text), and it used an LLM to detect sexual abuse. They demoed it with examples. But when I typed in an elementary school song, it also flagged that as a harmful sentence, with 95% confidence.

There was a group that developed a plant preservation app. When given a plant photo, it identifies the disease it has, and links to Amazon for the plant medicine. They demoed it with some photos they downloaded. I asked them to download Ethan's photo and use that. The app declared that my friend has Northern corn leaf blight disease! 

It was also interesting to see majority of the groups struggling to do a half decent job at pitching their project. They jump right in to talking about the how, rather than the what. First tell us what problem you are solving, then demo it, and then talk about the how part. 

In our batch there were a couple groups that did a good use of local-first AI. One group did the speech recognition locally with the Vosk library and used Google Translate API for converting the language to English to provide a real-time translation experience. This approach pulls the compute to the data, rather than having to transmit the large speech data to the cloud for processing. Simple and effective. 

It was easy to spot the groups that had fun with their project, and that is the important part. The technology is secondary to the solution/product. Always.