The first time I heard Coq was in college. Since then I always wanted to learn Coq but didn’t know how to. Lots ofhypotheses the tutorials are about logic, which doesn’t seem interesting to me.
I took UW CSE505 last quarter. Prof. Zach Tatlock and the TA Talia Ringer made some wonderful homework to help us learn Coq. While in this course, we proved more practical things, like a programming language interpreter and a regular expression matcher. I actually found myself feeling quite good about proving things in Coq (writing specifications is a completely different other thing), at least when doing homework.
If you are teaching yourself Coq, I’d suggest the following resources:
- Homework of UW CSE505
- Formal Reasoning About Programs is the textbook we used in class. It’s a short textbook with big margins and lots of whitespaces. It comes with detailed Coq code for each chapter and a very powerful Coq library
- Software Foundations is the material for you if you are really into verification.
I’m quite happy that I completed Coq in my wish list. But I’m not a huge believer of machine-checked proof or verification. Before I fully forgot Coq, let me write down some beginner-level tricks I learned when doing homework, just in case you might find it useful or I come back to Coq some decades later.
Take a close look at the following code:
Example: Concurrent Hashmap
Suppose we need a concurrent hashmap. I know there are lots of libraries, but let’s assume we need to write it by ourselves. For simplicity, we only support three kinds of operations:
We can use
std::unordered_map, but it is not thread-safe. So, the most straightforward solution would be to have a big lock to protect it. It’s simple, just like this:
I have always been loving Python. When people mention Python, they usually think of the following two advantages:
- Easy to write
- Easy to call C/C++ libraries
In fact, the first bullet point comes with super slow execution speed. And the second bullet point requires C/C++ libraries to export APIs according to Python specification, which might not be available for most of the libraries.
During the internship at Tianrang Inc., I had several experiences with Cython. I think although this tool is buggy sometimes and has terrible user experience sometimes, it can boost Python significantly and also help create wraps for C/C++ libraries. In this article, I’d introduce Cython to readers. Notice that, Cython is different from CPython. Cython helps us to conveniently:
- Use Python syntax to mix code in C/C++ and Python while boosting Python performance
- Call C/C++ libraries
I used not to care about parallelizing small programs because I thought parallelizing them would cost me more time than writing the programs themselves, and also because there are only four cores on my laptop. Unless the task were IO intensive, I would leave it running with a single thread. Everything has changed since I have access to a machine with 32 cores and 128GB memory. Looking at all those idle cores from
htop, I felt the urge to utilize them. And I found it’s super easy to parallel a Python program.