hwayne

function Ask {
  Param (
    [PSDefaultValue(Help="*")]
    [switch]$Fast,
    [Parameter(Position=1)]
    [Alias("M")]
    [int]$Tokens=256,
    [Alias("n")]
    [int]$Results=1,
    [Parameter(Mandatory=$true, Position=0)]

hwayne

Pleased to announce a new #NFT offering: #eNdFT! We are minting one cause of death NFT for every person on earth, which is 100% guaranteed to reflect the way you do, in fact, actually die.

Unless you trade it!

Unhappy with your "car crash" #eNdFT? Exchange it for an "old age"! Of course, you better be prepared to pay through the nose for "old age". Due to the nature of our product, eNdFTs cannot be bought or sold, only be traded 1-1 for another #eNdFT (plus an optional eth price to cover value differences). There is no escaping death.

Please note that our prediction software isn't perfect. While every #eNdFT is accurate, it may be imprecise. For example, you could receive the "Most likely drowned" NFT, or "either cancer or a stabbing". Don't worry, eNdFTs are still an exciting speculation opportunity! We're improving our prediction software all the time, and that "cancer or stabbing" #eNdFT could one day become a super valuable "cancer"! Join the #eNdFT network today!

(Disclaimers: while we will confirm

hwayne

// dreidel model I wrote in 2023.
// see https://buttondown.com/hillelwayne/archive/i-formally-modeled-dreidel-for-no-good-reason/
dtmc

const int M; //starting money
formula Players = 4; //Players
formula maxval = M*Players;
formula done = (p1=0) | (p2=0) | (p3=0) | (p4=0);
formula halfpot = ceil(pot/2);

hwayne

// put in https://editor.p5js.org/
// generated (mostly) with GPT4

let cols, rows;
let w = 2;
let colors = [];
let i = 0;
let j = 0;
let sorted = false;

hwayne

import planner.

lookup(Val, Arr1, Arr2) = Out =>
    nth(I, Arr1, Val),
    nth(I, Arr2, Out).

main =>
    Machine = [{{load1, 1}, {proc1, 0}, {done1, 0}, {load2, 1}, {proc2, 0}, {done2, 0}, {lock,  1}},
               [ {load1, 
                  {{load1, 1}, {lock, 1}},  % Maybe the inner ones should be lists, they're only iterated over

hwayne

import planner.

main =>
    S0 = {22, 0, [6, 6, 9, 5, 9, 1, 10, 9, 9, 3]},
    plan(S0, Plan),
    nl,
    writeln(Plan),
    nl.

final({Target, Current, _}) => 

hwayne

CONSTANTS
    Threads = {t1, t2, t3}
    NULL = NULL

SPECIFICATION Spec
PROPERTY NoRaces

hwayne

// ETL pipeline

sig DataSource {}

sig Step {
  requires: set Step
}

sig Database, File extends DataSource {}
sig Extract in Step {

hwayne

-- Put this in after/plugins

local api = vim.api

local function chunk(text)
  local sections = {}

  for line in vim.gsplit(text, "@@@") do
      if line:find("^s") then
          table.insert(sections, {role = "system", content = line:sub(3)})

hwayne

People who take my TLA+ Class get a free specification review. Cory Myers asked for a review of his Reply.tla spec, reproduced from the PR below, and has graciously agreed to let me make it public. The review itself is here.

Note this is a "light" review: I'm looking for general TLA+ antipatterns and techniques that don't require me to deeply understand the problem domain. This represents about an hour of review.