Coq will be renamed From the Coq-club: The Coq development team acknowledges the recent discussions (started on the Coq-Club mailing list) around Coq’s logo and name. We wish to thank everyone that participated in these discussions. Testimonies from people who experienced harassment or awkward situations, reports about students (notably women) who ended up not learning /

Building the future of computing with your help For the last five or six years, since I bid goodbye to the startup scene and Silicon Valley, I have been increasingly working in public. I have written a book, given around 100 talks (many of which are available on YouTube), published over 20 research papers (all freely available

LAMBDA The ultimate Excel worksheet function Post by Andy Gordon and Simon Peyton Jones on LAMBDA giving Excel users the ability to define functions. Ever since it was released in the 1980s, Microsoft Excel has changed how people organize, analyze, and visualize their data, providing a basis for decision-making for the millions of people who use it

Google Brains Jax and Flax Google’s AI division, Google Brain, has two main products for deep learning: TensorFlow and Jax. While TensorFlow is best known, Jax can be thought of as a higher-level language for specifying deep learning algorithms while automatically eliding code that doesn’t need to run as part of the model. Jax evolved

Decentralised content moderation Who is doing interesting work on decentralised content moderation? With Donald Trump suspended from Twitter and Facebook, and Parler kicked off AWS, there is renewed discussion about what sort of speech is acceptable online, and how it should be enforced. Let me say up front that I believe that

What is the Right Response to Employer Misbehavior in Research I enjoyed my conversations with Timnit when she was in the MSR-NYC lab, so her situation has been on my mind throughout NeurIPS. Piecing together what happened second-hand is always tricky, but Jeff Dean’s account and Timnit’s agree on a basic outline. Timnit and others wrote a paper for FAccT

Using Bloom filters to efficiently synchronise hash graphs This blog post uses MathJax to render mathematics. You need JavaScript enabled for MathJax to work. In some recent research, Heidi and I needed to solve the following problem. Say you want to sync a hash graph, such as a Git repository, between two nodes. In Git, each commit

Experiments with the ICML 2020 Peer-Review Process This post is cross-listed on the CMU ML blog. The International Conference on Machine Learning (ICML) is a flagship machine learning conference that in 2020 received 4,990 submissions and managed a pool of 3,931 reviewers and area chairs. Given that the stakes in the review process are high — the careers

New courses on distributed systems and elliptic curve cryptography I have just published new educational materials that might be of interest to computing people: a new 8-lecture course on distributed systems, and a tutorial on elliptic curve cryptography. Distributed Systems Since last year I have been delivering an 8-lecture undergraduate course on distributed systems at the University of

The open source paradox A new idea is insinuating in social networks and programming communities. It’s the proportionality between the money people give you for coding something, and the level of demand for quality they can claim to have about your work. As somebody said, the best code is written when you are supposed to