miikka

(* How do to topology in Coq if you are secretly an HOL fan.
   We will not use type classes or canonical structures because they
   count as "advanced" technology. But we will use notations.
 *)

(* We think of subsets as propositional functions.
   Thus, if [A] is a type [x : A] and [U] is a subset of [A],
   [U x] means "[x] is an element of [U]".
*)
Definition P (A : Type) := A -> Prop.

miikka

# RELAX NG compact syntax cheat sheet

# See also:
# * tutorial <http://www.relaxng.org/compact-tutorial-20030326.html>
# * spec <http://www.relaxng.org/compact-20021121.html>

# Checking a XML file:
#
#     jing -c schema.rnc file.xml
#

miikka

/* Recursively observe property reads of an object. 
 *
 * Takes the target and an object for returning results. Returns the proxied
 * target. Results are assigned to result.reads.
 *
 * Example:
 *
 *     var target = {a: 1};
 *     var result = {};
 *     target = observeReads(target, result);

miikka

/* We present: high-quality highly accurate nanosleep with a spinner.
 *
 * Compile and run:
 * 
 *     gcc -shared -fPIC -o libsleep.so sleep.c
 *     LD_PRELOAD=./libsleep.so sleep 3
 * */

#include <time.h>

miikka

#!/usr/bin/env python
# Like sleep(1), but shows a spinner while waiting.

import time
import sys

CHARS = '/-\\|'


def spin(delay):

miikka

import inspect

DONE_ONCE = set()


def only_once():
    """Use as a generator to run a block only once."""
    frame = inspect.stack()[1]
    # frame is (frame object, path, line, ...)
    key = (frame[1], frame[2])

miikka

Moralistic Therapeutic Rationalism (MTR)

1. A rational principle exists that ordered the world and governs over human life on earth.
2. Rationalism wants people to be good, nice, and fair to each other, as taught by LessWrong and by most world religions.
3. The central goal of life is to be rational and to feel smart about oneself.
4. Rationalism does not need to be particularly involved in one's life except when rationalism is needed to resolve a problem.
5. Rational people live forever when the Singularity happens.

See also: http://en.wikipedia.org/wiki/Moralistic_therapeutic_deism

miikka

"""This is a sketch of implementing pattern matching of lists.
"""

from collections import namedtuple

# Destructuring lists
#
# In a destructuring pattern:
#
# * V('foo') matches a value and assigns it to foo

miikka

"""A sketch of parser combinators for Python.

I wanted to parse a recursive list of words with Python-like syntax, for
example:

    [foo, [bar, baz], quux]

Using an external library would have been too hard and complicated.
Unfortunately this didn't end up being very beautiful, either. Check out the
definition of wordlist(). Ugh.

miikka

Keybase proof

I hereby claim:

• I am miikka on github.
• I am miikka (https://keybase.io/miikka) on keybase.
• I have a public key whose fingerprint is 0753 C3DA 748E DA91 AAB1 E35E 8005 E0EB BCB7 E306

To claim this, I am signing this object: