August 7, 2014
One weird type (or, good representations as a tool for thought)

I gave a talk at Lambda Jam in July. We start off with this question…

…and arrive at this:

Here’s the abstract.

If you define a thing in a certain kind of way in a certain language, the language will make it fun and easy to prove things about the thing! It’ll help you reason about how the value was constructed. By supplying evidence that a proposition is true for a base case (e.g. 0) and that it’s true for a “built-up” value (e.g. n + 1) given that it’s true for the “non-built-up” value (e.g. n), you can show that the proposition is true for all values of that type.

How does this work computationally? Defining properties or types inductively in Coq, a proof assistant, will generate an “induction principle” that you can use (along with other proof techniques) to prove things by induction about the property or type.

We will examine several examples, such as natural numbers, interesting properties, and propositions.

The materials are here, including slides and usable Coq code. I’d love to hear any comments or suggestions.

Update: If you don’t mind using other lemmas, here’s a much more elegant version from @eisaru!

July 9, 2014
syntax

I have a piece in Method & Apparatus*, a zine on the use of accessible tools, works created using them, and the process behind the work. It’s curated by chrisamaphone. You can get a copy here!

*In the spirit of patents.

May 21, 2014
Proofs about programs, proofs as programs, and programs as proofs!

I gave a talk at !!con last weekend. This was the abstract:

"Say you had two pieces of code that looked different, but you strongly suspected they were ‘equal.’ Maybe you have two if statements and you’re a compiler who wants to optimize code by exchanging one for the other. How would you prove that they were equal? And since you’re already a compiler, why don’t we verify your proof with a computer?!

We’ll take a tour through the world of interactive theorem proving with Coq, a proof assistant. We’ll use Coq to interactively prove that two pieces of code, though they look different, are ‘equal’ in that they return the same values for all inputs. Our proof will lead us to examine the strange correspondence between proofs and programs. It’s an exciting development at the frontier of CS and math research: a data type is a proposition, and a value of that type is a proof of that proposition!”

Here are the materials:

• Slides with notes
• Coq code from live-coding (well, live-proving)
• Interactive version of the code. Hover over each line to see the current proof state and goals.
• Interactive version of Coq 2048. (In Chrome, go to `View > Encoding > UTF-8` to fix the characters.) I did not write this; it’s by Laurent Théry. Scroll to the bottom and hover over each line of `Lemma thm1`. The theorem states that there exists a list of moves (`ms`) such that the initial configuration results in a 2048. Each step in the proof is a move (note the similarity to an imperative program), and you can complete the proof with `Qed.` when you get 2048!
• Check out these amazing sketchnotes by Chris Martens.

I used Proviola to generate the interactive Coq proofs.

May 11, 2014
Open source comes to Princeton

Cross-posted from the OpenHatch blog.

On November 24, Open Source at Princeton helped run an Open Source Comes to Campus event with OpenHatch. (Warning: the word “open” will occur very often in this post.) OpenHatch is a non-profit dedicated to matching prospective free software contributors with communities, tools, and education. They provide online tools for new contributors and organize and support outreach events. Open Source Comes to Campus is a one-day workshop to teach the tools and culture of open source development and to help students make contributions to real projects. Groups at 21 schools have run this event, including 10 women-in-CS organizations.

We were super excited to run this event, and it seems that people were as excited to attend—we received 80 sign-ups, of which about 40 people showed up. Here’s how it went.

The schedule

The workshop was held on a Sunday from 10 am to 5 pm. You can see the schedule here. Sumana Harihareswara, our wonderful speaker from the Wikimedia Foundation and Hacker School, delivered the introduction to open source communications tools.

People seemed to really enjoy the activities. First, OpenHatch found two cute bugs, accessible to beginners and documented in issue trackers. They were “No December” (that is, in a certain version of Android, the month December disappeared) and “can’t print on Tuesdays.” Pairs of people looked at the bugs and tried to explain the causes to each other. I won’t spoil why they were happening—take a look at the handout here!

Attendees also really enjoyed the git mini projects. They worked in groups of five with one mentor each. They cloned a sample repo that was the Princeton page with quirky changes added in, made changes on their machines, made pull requests, and got them merged in. After the merge, they could refresh the page to see their changes. It was rewarding because of the instant and visual feedback. Here’s a sample page and here are the pull requests.

Contributions

The contributions workshop was designed to be the capstone of the workshop, where attendees would finally have the chance to make their own changes. In reality, there were mixed responses. Some attendees left early, whereas some attendees got really excited about their bugs and stayed for an hour after the workshop ended.

OpenHatch put together a great First Tasks page that listed welcoming bite-size issues for beginners to fix, including projects like Dreamwidth, WelcomeBot, the Open Science Collaboration Blog, and OpenHatch itself. We also had mentors familiar with projects like OpenStates, Debian, and MediaWiki.

The attendees made six pull requests total, of which three were successfully merged (yay!), two not completed by the students, and one fixed by the maintainer. Most contributions went to OpenHatch itself and OpenStates. Unfortunately, Dreamwidth, WCWeekly, and Open Science Collaboration blog didn’t get contributions, possibly because the maintainers weren’t present at the video call.

One sample pull request: Scott, a student here, worked on OpenStates. He found that a legislator had unsightly Javascript on her page, and diagnosed the cause in the source code, which was that House representatives’ pages were missing the closing </div> tag. A maintainer for the project emailed the source website, and the error was fixed.

You can find details of the other pull requests here.

Attendee statistics

We were excited about the fact that the people who signed up (and showed up) were about 30% women! (Compare this to the estimated 2% of women in the wider open-source community.) I hope our emphasis on reaching out to Princeton Women in CS and making the event beginner-friendly played a part in this.

In response to the question “Please briefly describe your involvement in open source,” most people had never contributed before, but many had used Firefox, WordPress, Eclipse, Ubuntu, and various other flavors of Linux. One great anonymous response: “My brother forced me to install Ubuntu and use gcc to code, but I never really did much with it.” Many people mentioned that they were particularly interested in contributing to Linux, Firefox, and Chromium.

The majority of people used Macs, more than half were already comfortable using the command line, and freshmen and sophomores made up about 70% of the registrants.

Future directions

Some things we learned:

• People really liked the more structured projects, like diagnosing bugs and practicing making pull requests. Some attendees struggled with the more-unstructured contributions workshop. We would encourage mentors to take a more active role in guiding students.

• Alternatively, maybe find projects with more bite-size issues to address. Maybe add features instead of fixing bugs? Writing HTTPS Everywhere rulesets could be well-structured and rewarding.

• Some attendees wanted the lectures to be more interactive.

• We should have encouraged people to follow the Hacker School social rules for a more welcoming environment.

• The workshop was rather long, and we forgot to ask most people to fill out the exit survey.

• Experienced CS students who attended the workshop weren’t annoyed by the review of the basics. In fact, one of them came up to us and said that he was very glad to see that we were going over git and version control, because a welcoming environment for beginners signaled that it would be welcoming for everyone else.

We’ve been continuing our work at Open Source at Princeton. Right now we’re running a long-term initiative with ThoughtWorks, a software consultancy, for students to contribute to OpenMRS, an open-source electronic medical records platform. You can find our documentation and progress here.

We’ll end with this encouraging exit survey response from an attendee:

“The skills you’re introducing people to… no, the world you’re introducing people to—it is so valuable for everybody that this world is nourished. And there is no better way to build the community around it than to pair people off with mentors who can give one-on-one attention to these future open source contributors.”

Thanks!

It took a lot of time and effort to make this happen, and we’d like to thank the following people and organizations.

Members of OpenHatch: Shauna Gordon-McKeon and Asheesh Laroia.

Members of Open Source at Princeton: Lisha Ruan, Katherine Ye, Valerie Morin, Dorothy Chen, Evelyn Ding, Colleen Carroll, Diana Liao, and Annie Chu.

Mentors: David Prager Branner (Hacker School), Omar Rizwan (Hacker School), Katerina Barone-Adesi (Hacker School), Jeremy Baron (MediaWiki, OpenHatch), Sumana Harihareswara (Wikimedia Foundation, Hacker School), Alex Clare (eBay, Hacker School), Alec Story (Google), and Paul Tagliamonte (Sunlight Foundation, Debian).

(There was one mentor for every five students!)

Organizations: Jane Street, GitHub, and Google sponsored us, and Princeton Women in CS helped us a lot with logistics.

This workshop was inspired by the OpenHatch workshop held at Columbia University.

February 23, 2014
What is the most fascinating thing you’ve learned in the past month?

Say your friend picks a number from 0-999,999 and you need to guess that number with 20 yes-or-no questions (Qs). You realize that you can ask max 20 Qs, instead of 1,000,000, if you eliminate half the numbers with each question with a binary search.

You succeed, but you realize that each Q depends on the result of the previous Q. You need to know your friend’s answer to the current Q to determine the next number to ask about. You wonder: how can I write Qs so they don’t depend on order? Can I can give them all to my friend, then generate her number? It’s possible, since each yes/no answer yields 1 bit of information, 20 Qs yields 20 bits, and (2 possibilities)^(20 bits) determines 1,048,576 possibilities (> 1,000,000 numbers).

You realize that 20 bits to determine a possibility sounds like the number in binary! Each number from 0-999,999 would be uniquely determined by 20 or fewer 1s or 0s. Using this, you can write 20 order-independent Qs. Each asks whether each successive digit in the binary representation is 0 or 1. (Is the 1st binary digit 1? etc.) With your friend’s answers, you can find the number by converting the number back to base 10.

If your friend can’t convert to binary, you convert each Q to base 10: Is the 2nd binary digit 1? → Is the number 2, 3, 6, 7, 10, … ? etc.

This tactic underlies a magic trick in which the participant picks a number from 1-50, the magician shows her 6 cards, the participant responds if her number is on the card, and the magician divines her number.

(I wrote this last year for Hacker School and recently dug it up. It’s terse because there was a word limit. Thanks to Professor Bhargava for teaching me this!)

February 8, 2014
fun with (fun with recursion)

Here are the slides for a short talk I gave at Code@Night. You can find the PDF here (in-browser). I only assume knowledge of recursion and arithmetic, so I hope it’s very accessible.

You can find some of my solutions to the ending exercises here. Let me know if you come up with more! And yes, the title is an ML pun.

January 29, 2014
Constructing a perfect comma

Click for larger.

The construction uses only a compass and straightedge, and I did it using Ancient Greek Geometry. This was inspired by the geometry of Twitter’s logo.

The fonts are Bodoni Std Poster Italic and Bodoni Std Book Italic.

September 2, 2013

It’s hard to describe what Hacker School is, but I think “a writers’ retreat for programmers” comes closest. Here are some things I did this summer:

Along the way, I met (and received lots of help from) the excellent people of the Hacker School community: facilitators, residents, fellow batchlings, and alumni. I had a great summer. If you’re interested in joining this community, applications for fall 2013 are still open. :-)

April 28, 2013
Things

Made a Twine game for this weekend’s Ludum Dare competition, whose theme was “minimalism.” You can view the entry here and play it here. As always, I’d love to know what you think.

Also, I’ll be at Hacker School this summer! Looking forward to being a batchling :)

(Note: this blog is mostly to document things I’m making / doing / learning. Maybe I’ll add opinions later.)

February 19, 2013
What I’ve been working on

I made a story/game experiment with Twine. You can read/play it here: Testimony

Let me know what you think!

If you liked Testimony, you might also like hypotext. I’ll write more about these and other writing+coding projects later.

Also added new non-artsy things to my GitHub.