2021-11-23 03:30:39 imode: "you're using one machine to ensure that another machine isn't doing dumb things" I like that 2021-11-23 15:29:53 imode: where's the stack then? 2021-11-23 15:39:41 niedzejkob[m]: you manipulate a stack of theorems. 2021-11-23 15:40:24 https://groups.google.com/g/metamath/c/vkV2mZ_O_F4 2021-11-23 15:40:46 "The verifier is a stack machine which starts with the empty stack. Each proof step pops as many hypotheses as required by the theorem, and then pushes the conclusion (so an axiom with no hyps increases the stack length by 1, and a theorem with n hypotheses increases the stack length by 1 - n). At the end of the proof, the stack is required to have exactly one element on the stack, which must match 2021-11-23 15:40:48 the statement of the theorem." 2021-11-23 15:43:14 oooh 2021-11-23 16:19:39 Not to gossip but, I wonder if Chuck and Elizabeth was not on good terms. Lol. 2021-11-23 16:26:06 what happened? 2021-11-23 16:31:17 Just in the fireside chat Elizabeth joined later on and the exchange of words was a bit awkward. 2021-11-23 16:31:30 I'm being dumb, nothing serious though. 2021-11-23 16:32:03 where is that you are talking about? 2021-11-23 16:32:06 It was Elizabeth's presentation on Computer Chronicles show got me check what Forth is about. 2021-11-23 16:32:08 I would be interested in seeing that. 2021-11-23 16:32:19 joe9: https://www.youtube.com/watch?v=BpsXyB2WsUw 2021-11-23 16:36:36 thanks. 2021-11-23 17:52:05 Rather enjoyed that gossip 2021-11-23 17:54:34 Haha