Skip to content

Instantly share code, notes, and snippets.

hwayne /
Created Nov 2, 2020
Code for PRISM essay
from math import comb
from string import Template
guard = "[worker] (left >= {n} & ((queue >= {n} & K = {n}) | (queue = {n} & K > {n}))) ->"
# For n = 3, this should be
# p^3 + 3p^2(1-p) + 3p(1-p)^2 + (1-p)^3
def actions_for(n):
base = "{prob}: (left' = left - {x}) & (queue' = queue - {x})"
hwayne / channels.tla
Created Sep 2, 2020
Go Channels in TLA+
View channels.tla
A model of
---- MODULE channels ----
EXTENDS Integers, TLC, Sequences
CONSTANTS NumWorkers, NumTokens
NULL == "NULL" \* Should be a constant, being lazy
Workers == 1..NumWorkers
Processes == Workers \union {0} \* Main

I don't have GPT-3 access but probably have followers that do and really want to see what happens when run on my writing. Here's some half-written drafts in my slush pile with no editing:

Don't be clever is something that's "obvious". The things are often obvious for very subtle reasons. So I like to ask questions about obvious things to learn the subtle thinking behind them. So why is clever bad? Why is what bad? What does it mean for something to be clever? Cleverness is also something that's obvious, which means we have to come up for a way of describing it and identifying it.

Clever is different from smart and is different from witty. I define cleverness to be "the capacity to insightfully exploit particulars of a problem." By "particulars", I mean things that make it less like a general case. By "insightfully", I mean the exploitation is not considered conventional.

Insightfully is context dependent. Doing a bit twiddling is not clever if you are in embedded systems design error, because in th

hwayne / friendlist.csv
Last active Jul 12, 2020
Friendlist draft two
View friendlist.csv
Name Days Contact Comments
their name on average how often to contact method of contact (signal/fb/etc) misc
required required optional optional
View taxes.als
//assumes no tax overrides
//assumes no tax can replace another tax
sig Location {} //states, cities
sig Category {}
sig Item {
, category: some Category
View gist:225f6818e59423e77c50c54effce9fec
87/ I've never been to France
88/ I've never been to France
89/ I've never been to France
90/ I've never been to France
91/ I've never been to France
92/ I've never been to France
93/ I've never been to France
94/ I've never been to France
95/ I've never been to France
96/ I've never been to France
hwayne /
Last active Jun 23, 2020
The Knights and Knaves Express

It's time to drag the Island of Knights and Knaves kicking and screaming into the 19th century! We're going to run a train. For these puzzles, you'll have a set of stations with possible connections, and you need to find a route that starts at one station, goes through every other station exactly once, and ends in a station. IE if our map was

A -- B -- C
|    |    |
D -- E -- F

Valid routes might be A B C F E D, or A D E B C F, but A B E D C F is invalid. The ordering matters: A B C is a different route from C B A.

hwayne / access_policies.als
Last active May 25, 2019
Alloy Access Control
View access_policies.als
one sig Person {
roles: set Role
sig Role {}
sig Resource {
, access: set Person + Role
, parent: lone Resource
View snippet thingy
proc write(key: str, value: T) modifies store {
store[key] := value;
fun read(key: str) returns (out:T) {
out := store[key];
// ....
hwayne /
Last active Apr 27, 2019
Gilded Rose Kata


  • At most one of sulfuras?, pass?, and brie? are true

Assuming whenever they say "increases or decreases" without a qualifier, they mean 1. This is a BIG assumption (it's not specified).

sulfuras? pass? brie? days_left change
T - - - 0
F T - 11- +1