| 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 |
| 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 |
| 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: |
| 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 | |
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
}
| ; NOTE: might not work out of the box, I'm assembling this from several different files | |
| g_mode := "" | |
| set_mode(new_mode) { | |
| global g_mode | |
| if (g_mode = new_mode) { | |
| g_mode := "" | |
| } | |
| else { |
| " vim: ft=vim:fdm=marker | |
| " This must come first or else | |
| " the local mappings for plugins | |
| " won't use the mapleader? | |
| let mapleader="\<Space>" | |
| " Using powershell messes up Gutentags, temporarily disable | |
| " TODO make a way to quickly enter powershell |
| 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})" |
| A model of https://utcc.utoronto.ca/~cks/space/blog/programming/GoConcurrencyStillNotEasy | |
| ---- 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