*In the spirit of patents.
*In the spirit of patents.
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:
View > Encoding > UTF-8to 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!
I used Proviola to generate the interactive Coq proofs.
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 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.
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.
You can find details of the other pull requests here.
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.
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.”
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.
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!)
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.
Click for larger.
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. :-)
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.)
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.
In the beginning of January, I was lucky enough to be able to attend Square Code Camp, a 4-day program created by Square to immerse female engineering students (17 from universities across the US) in startup culture and computer science. Here are some of the highlights of the activities that our awesome organizers, Rachel Constable and Vanessa Slavich, planned for us:
Meeting Jack Dorsey
I’d been curious about Jack, the founder of Twitter and Square and man of many interests, for a while. The morning of the first full day, he gave us the Square talk and walked us through the rumored “Gandhi Walk.” I can’t comment on what he said, but I was impressed by the subtlety and depth of Square’s credo.
Tech Trek: Security Workshop
The motto of this workshop could have been “move fast and break things.” In just two and a half hours, the head of security at Square showed us a simple credit-transferring web app he had built, gave us time to hijack it, taught us how to properly hijack it, and told us awesome security war stories. Now I know to look for any opportunity for user input (username, password, email, file upload, filename, numbers, etc.) and think about breaking out of the environment to inject malicious code, the goal being to run arbitrary code. In one of my favorite hacks, we realized that when the web app uploaded files, it would do so like this:
PATH = (get user-inputted filename)
upload (get user-uploaded file) to ~\somedirectory\PATH
If you named your file starting with arbitrary chars set off by a semicolon or &&, you would break out of the upload command into a shell that could run any commands you wanted:
'(arbitrary chars here); (arbitrary commands here)'
'dfhgfkajsh; ls; rm exampledir.db; ls'
So, as seen above, Leah and I deleted the database and killed the web app. Move fast and break everything.
Imagine that you have little to no experience with web development and Ruby on Rails. Then you’re put on a team with two Code Campers who also don’t have Rails experience, plus one engineer from Square, and asked to build a full-fledged event management Rails app for Square in six hours. Thankfully, Erica Kwan, the lady running Dev Day, had built some of the hard parts for each of the teams already, but we still found it tough (and rewarding). We worked with Square engineers Jack Danger and Sean Sorrell, and you can see what Stephanie, Sumaiya, and I built with their help here. Pair-programming with Sean was awesome. In addition to showing us how Rails and the MVC model worked, he also showed me the CMD+` (Safari) and CTRL+TAB (Chrome) shortcuts, saving me years of Mac tab-switching frustration.
Square’s Design and People
There’s much more I haven’t mentioned, but everything we did and saw was touched by Square’s sense of design. Besides the sleek, crisp site and app, I was impressed by the presentations and workshops. I haven’t met many presenters who follow these unwritten rules: that the slides should consist of as many pictures and as few words as possible (five or less, if possible), that there should be opportunities for participants to guess the answer before presenting the real answer, that the presenter should keep it simple and build a narrative with metaphor. All of the presentations at Square followed these principles, but Jim McKelvey, one of the co-founders of Square, gave a talk on glassblowing that transcended slides.
Also, shout-out to my mentor, Vida Ha! I had great conversations about start-up culture and San Francisco with her, and she gave me invaluable advice.
If you’re a woman in college majoring in CS/EE/math and you’re reading this, I would definitely recommend applying to Square Code Camp. If not, I’d recommend trying Square’s app and reader. They’ve put a lot of care into the design, and it shows.