gigamonkey

Guy Steele on formal proofs from Coders at Work

Seibel: Do you ever try to formally prove your code correct?

Steele: Well, it depends on the code. If I’m writing code with some kind of tricky mathematical invariant I will go for a proof. I wouldn’t dream of writing a sorting routine without constructing some kind of invariant and proving it.

Seibel: Peter van der Linden in his book Expert C Programming has a sort of dismissive chapter about proofs in which he shows a proof of something, but then, ha ha, this proof has a bug in it.

Steele: Yes, indeed. Proofs can also have bugs.

gigamonkey

#!/usr/bin/env python3

"Generate all strings containing just ( and ) with parens balenced."

from itertools import count

def parens():
    def nested(x):
        return ("(" * x) + (")" * x) if x > 0 else ""

gigamonkey

def levenshtein_distance(a, b):
    """
    Compute the Levenshtein distance between a and b.
    (https://en.wikipedia.org/wiki/Levenshtein_distance) Uses an
    efficient dynamic programming implementation.
    """

    m = [ [ 0 for _ in range(len(a) + 1) ] for _ in range(len(b) + 1) ]

    for i in range(1, len(a) + 1):

gigamonkey

function onInstall() { 
  onOpen();
}

function onOpen() {
  DocumentApp.getUi()
  .createMenu('Fix links')
  .addItem('Entitle link at cursor', 'entitleAtCursor')
  .addItem('Entitle all links', 'entitleAllLinks')
  .addToUi();

gigamonkey

#!/bin/bash

# Prune remote branches that no longer exist on remotes
for remote in $(git remote); do
    git remote prune "$remote"
done

# Delete branches whose tracking branch no longer exists
for b in $(git show-ref --heads | cut -c 53-); do
    remote=$(git config "branch.$b.remote")

gigamonkey

#!/usr/bin/env python3

#
# Dump all the messages from a given Slack channel since a certain
# timestamp, one line per message with timestamp and user name.
#


from datetime import datetime
from pytz import timezone, utc

gigamonkey

#!/usr/bin/env python3

#
# Find the best matches between a set of dirty names and a canonical set.
#
# Is O(N^2) in the number of names.
#

import json
from lcs import lcs

gigamonkey

#!/usr/bin/env python3

from functools import wraps
import json

# Pretend this was logging to disk
log = []

def mutator(fn):

gigamonkey

#!/usr/bin/env python3

from time import sleep
from datetime import datetime, timezone

# Snowflake like ID generator that generates a 53-bit id suitable for sending as a number in JSON.

TIME_BITS    = 40
COUNTER_BITS = 10
MACHINE_BITS = 3

gigamonkey

Turing Award Winner Fran Allen on changing role of women in computing. (From Coders at Work)

Seibel: You also mentioned before that when you started, people thought women would be good programmers because women were thought to be detail-oriented. These days the conventional wisdom is that it’s men who have a bizarre ability to focus on things, usually to the detriment of everything else, and that’s why most programmers are men.

Allen: Right.