hwayne

You are writing simple budgeting softare. A Budget consists of a total limit, represented as a positive integer, and a dictionary of category limits, represented as a map from strings to integers. For example:

{
  "total_limit": 50,
  "category_limits": {
    "food": 10,
    "rent": 11,
    "candles": 49
 }

hwayne

This works because of undocumented behavior in TLC: 
`Sequences` operators have overrides that also works on strings.
So you take the Head of a string to get the first character.

Please don't use this in an actual spec, it's for demonstration purposes only.
Also, this is likely to get patched out soon. See (https://github.com/tlaplus/tlaplus/issues/512)
ALSO also it breaks on lots of stuff, like it says `TypeOf(1..3) = "int"`
TypeOf(TLCEval(1..3)) works properly but I'd rather not make this more useable

hwayne

class Bank:
    def __init__(self, balance):
        assert balance > 0
        self.balance = balance
    
    def deposit(self, val):
        self.balance += val
    
    def withdraw(self, val):
        if val <= self.balance:

hwayne

get_timezone() {

	clipboard := ""
	Send ^c
	ClipWait, 2
	
	timeshim := A_WorkingDir . "\Lib\Aux-Scripts\timeshim.py" ; TODO use A_ScriptDir somehow 
	cliptime := clipboard
	cmd := "pythonw.exe " . timeshim . " --date=""" . cliptime . """ | clip"
	runwait, %ComSpec% /c "%cmd%", ,Hide

hwayne

open util/ordering[Time]

let unchanged[x, t, t'] {x.t = x.t'}
sig Time {}

sig Msg {}

sig Pub {
	-- really a topic, but then we're double-using T as a letter
	, msgs: Msg -> Time

hwayne

A while back I complained on Twitter about how Ada Lovelace is used as an example of "an important woman in CS", because she's a pretty terrible example (thread in comments), and listed some better choices. In response, somebody said that public people get why Lovelace is interesting, whereas it's hard to explain why, like, Barbara Liskov matters so much. That got me interested in explaining the contributions to CS in ways that are understandable to people with no tech background. Here's my attempt to explain Frances E Allen, who did foundational work in optimizing compilers:

---

Without Frances Allen, our videogames would be stuck in the SNES era.

So at a fundamental level, a computer is just a bag of buckets of data (memory addresses), and a program is just instructions ot move data between the buckets. Like mov edx, [ebp + 8] means "take the data in the 8th bucket after the ebp bucket and move it to the edx bucket." All programs eventually become this "assembly" language that the computer execut

hwayne

How the J Script Works

Going line by line:

b =: >: i. 9 9 9

This generates a 9 by 9 by 9 array with all values from 1 to 729. We can choose what each axis represents: I decided that each table is all of the boolean variables for one number, and the rows and columns map to sudoku rows and columns. For example:

hwayne

" TODO: MAKE THIS ALL USE AUTOLOAD
" Macro Handling {{{

let s:macro_file = g:exo . 'macros.json'

function! s:macro_list(ArgLead, CmdLine, CursorPos)
  let macros = json_decode(readfile(s:macro_file))
  return join(keys(macros), "\n")
endfunction

hwayne

---- MODULE BubbleSort ----
EXTENDS Integers, TLC, Sequences, FiniteSets

Counter(seq) == 
  LET
   Range == {seq[x] : x \in DOMAIN seq}
   CountOf(x) == Cardinality({i \in 1..Len(seq): seq[i] = x})
  IN
    [val \in Range |-> CountOf(val)]

hwayne

---- MODULE Filters ----
EXTENDS TLC, Integers
VARIABLE push_msgs, emails, i, filtered, pushed
vars == <<push_msgs, emails, i, filtered, pushed>>

set ++ x == set \union {x}
set -- x == set \ {x}

TypeInv ==
    /\ emails \subseteq (1..3)