2022-05-15 17:32:46 <remexre     > what symbols are other people using for quotations? I'm using { } right now, but kinda feeling like [: ;] might be "more mnemonic"
2022-05-15 17:34:14 <Zarutian_HTC> what kind of quotations?
2022-05-15 17:36:03 <remexre     > uh like in-line anonymous word definitions
2022-05-15 17:36:40 <remexre     > : foo { bar } ;   =   : foo [ :NONAME bar ; ] LITERAL ;
2022-05-15 17:37:09 <remexre     > (assuming the latter works in the relevant system)
2022-05-15 17:37:33 <Zarutian_HTC> I see, but I have never have used such so I do not know
2022-05-15 17:38:17 <Zarutian_HTC> I have toyed with nested definitions
2022-05-15 17:40:42 <Zarutian_HTC> where each : at compile time inserts a jump that the corrisponding ; patches
2022-05-15 17:41:31 <remexre     > yeah, in my bootstrap implementation it gets compiled that way
2022-05-15 17:41:43 <crc         > remexre: I use [ ] for quotations
2022-05-15 17:42:26 <remexre     > the implementation being bootstrapped is a "proper" optimizing compiler, and so is (able to be?) a bit trickier
2022-05-15 17:42:48 <remexre     > crc: hm, a bit too far from the spec for me :)
2022-05-15 17:43:01 <remexre     > (not that I'm following it strictly, but still)
2022-05-15 17:43:11 <Zarutian_HTC> plus ; changes the LATEST or equiv to point at the header of the corrisponding : while also putting into the auxulary of that header what that LATEST had been pointing too
2022-05-15 17:44:14 <crc         > If following standard Forth, I’d probably use [: ;]
2022-05-15 17:44:51 <Zarutian_HTC> meant that SEE had to become a bit more complicated but it could, given an XT figgure out how to display that word
2022-05-15 17:45:20 <remexre     > Zarutian_HTC: hm, like it displays the "surrounding" word?
2022-05-15 17:46:23 <Zarutian_HTC> more that it gave the nested word a name path so to speak
2022-05-15 17:46:44 <Zarutian_HTC> then one could see the surrounding word
2022-05-15 17:47:08 <Zarutian_HTC> note this idea supports arbitrarly nested definitions
2022-05-15 17:47:52 <KipIngram   > remexre: I've never used that mechanism either.  I just give everything a (possibly un-linkable) name.
2022-05-15 17:48:36 <KipIngram   > In mine a new word created by : is available immediately, so you could use that as a recursion method if you wished.
2022-05-15 17:49:11 <KipIngram   > That leaves ; just compiling (;), setting STATE=0, and handling any appropriate tail optimization.
2022-05-15 17:49:55 <remexre     > yeah, that's what my older ones have all done
2022-05-15 17:50:31 <remexre     > I'm trying out using quotations pretty heavily for control flow and replacing patterns like 2R> some stuff >2R this time around though
2022-05-15 17:50:49 <Zarutian_HTC> KipIngram: STATE in what I described above became a nesting level counter
2022-05-15 17:51:01 <KipIngram   > Ah - nifty.
2022-05-15 17:51:55 <KipIngram   > In that early book Chuck wrote he had a "levels" mechanism.  Wasn't quite the same thing - it allowed the system to decide whether to execute something now or push it onto a "level stack" for later execution.
2022-05-15 17:52:07 <KipIngram   > Let him do things like infix processing pretty smoothly.
2022-05-15 17:52:30 <KipIngram   > It was early in his career - he didn't seem as hard nosed about just throwing out "poor methods."
2022-05-15 17:52:50 <KipIngram   > He seemed worried that lack of infix support would be "held against" the language.
2022-05-15 17:54:47 <KipIngram   > remexre: I'm guessing that implementing quotations explicitly lets you explore some areas that would be hard to otherwise explore?
2022-05-15 17:55:07 <Zarutian_HTC> I am glad he saw the idiocy of inifix notation and dispensed with it
2022-05-15 17:55:41 <remexre     > KipIngram: this is partly an attempt to convince the category-theory people I talk to that they should be interested in concatenative languages :)
2022-05-15 17:55:53 <KipIngram   > :-)  Me too.  I think he was just worried that if  he didn't show that the language *could* do certain "common things" they'd reject it.
2022-05-15 17:55:56 <remexre     > and partly that someday I want to try bolting some formal verification tooling onto a Forth compiler
2022-05-15 17:56:12 <KipIngram   > Looks like he got more confident later, like most folks do as they move on from being a kid.
2022-05-15 17:56:32 <remexre     > and it's a _heck_ of a lot easier to write down the formal semantics of quoted definitions than the semantics of e.g. BEGIN
2022-05-15 17:56:36 <KipIngram   > got it - that makes sense.
2022-05-15 17:56:46 <KipIngram   > Both of those things make sense.
2022-05-15 17:57:54 <Zarutian_HTC> dunno, formal methods both reek of math wankery to me and seems to be usefull as in verifying stuff like seL4
2022-05-15 17:59:11 <KipIngram   > :-)  That wankery can be be pretty powerful.  I don't know much "really formal" math (pure math, I guess you'd say), but it does seem to have a place as far as I can tell.
2022-05-15 17:59:26 <KipIngram   > but yeah, something like a microkernel seems like a pretty good thing to be "sure" of.
2022-05-15 17:59:28 <spoofer     > If you haven't skimmed throught the WASM spec, it might be amusing to you over a lunch.  Use it for inspiration/caution rather than adopting though. ;)
2022-05-15 17:59:33 <remexre     > yeah, it very much depends on _what_ formal methods stuff you're talking about
2022-05-15 18:00:09 <Zarutian_HTC> spoofer: hmm? could you expand on that?
2022-05-15 18:00:33 <remexre     > I'm planning on trying a first-order-logic-only separation logic-based thing; so to a large degree, a human doesn't need to write proofs themselves
2022-05-15 18:00:38 <remexre     > only properties words have to conform to
2022-05-15 18:00:56 <spoofer     > The WASM machine defines a lot of "forth" like words with a pre condition/ post condition for each op code.  It goes a long way towards a formalish mechanism.
2022-05-15 18:01:29 <spoofer     > You can basically do a large part of a constructive proof given a sequence of opcodes.
2022-05-15 18:02:09 <Zarutian_HTC> spoofer: right, it looks to me like WASM spec was written by someone with hw and cpu design background
2022-05-15 18:02:17 <remexre     > yeah, that's approximately what my thing would look like
2022-05-15 18:02:35 <remexre     > that mostly breaks down ime (I work on very similar systems at work) when control flow with complicated invariants gets involved
2022-05-15 18:03:02 <remexre     > e.g. pretty much any form of parsing needs automation-infeasible amounts of handholding
2022-05-15 18:03:11 <Zarutian_HTC> spoofer: a lot of instruction specifications do have pre- and post-conditions like that
2022-05-15 18:05:37 <remexre     > my theory with my effort is that encapsulating the looping with easier-to-analyze looping combinators (i.e., ones where the induction variable is explicitly provided) will make it much more tractable
2022-05-15 18:05:42 <Zarutian_HTC> remexre: as I understand it there is basically two kinds of branching control flow, looping and conditional execution of a block
2022-05-15 18:06:31 <Zarutian_HTC> sorry, what the heck is an induction variable?
2022-05-15 18:06:51 <remexre     > that's the term compilers textbooks use, I'm not thrilled with it either :)
2022-05-15 18:07:04 <remexre     > in a C-like loop, e.g. for(int i = 0; i < n; i += 4)
2022-05-15 18:07:19 <remexre     > the induction variable would be ((n - i) / 4)
2022-05-15 18:07:35 <Zarutian_HTC> you mean the variable of kind boolean which selects if the branch is taken or not?
2022-05-15 18:07:35 <remexre     > (I think some things would define it as (i / 4) instead, idk)
2022-05-15 18:07:51 <remexre     > no, a counter that's essentially the number of iterations left
2022-05-15 18:07:58 <remexre     > not all loops have one, ofc
2022-05-15 18:08:07 <remexre     > but most "well-behaved" ones do
2022-05-15 18:08:15 <KipIngram   > That kind of comes straight from pure math.  If you want to "axiomize" all of math, you start out by building up the natural numbers.  And you build them one at a time.  You start with 1, then define a "successor function," and so on.
2022-05-15 18:08:19 <remexre     > and a lot of loop-related compiler optimizations rely on the compiler being able to determine one
2022-05-15 18:08:29 <Zarutian_HTC> aah! like the down counter used by (next) in Forth
2022-05-15 18:08:30 <KipIngram   > Then arithmetic gets defined in terms of successors and predeccors and so forth.
2022-05-15 18:08:52 <KipIngram   > Makes me cringe, but I guess a formal proof of correcness does have some value.
2022-05-15 18:09:01 <KipIngram   > correctness
2022-05-15 18:09:33 <remexre     > Zarutian_HTC: I'm not familiar; down counter?
2022-05-15 18:09:40 <Zarutian_HTC> and is often read only for the code inside the loop body in PrimitiveRecursiveArithmatic
2022-05-15 18:10:07 <KipIngram   > But then in the 1920s or 30s or so Godel came along and proved that any system of logic capable of expressing arithmetic could not be simultaneously complete and consistent.
2022-05-15 18:10:11 <KipIngram   > Or something like that.
2022-05-15 18:10:30 <KipIngram   > In any such system there is a "true statement" that cannot be proven true within the framework of the system itself.
2022-05-15 18:11:08 <KipIngram   > He proved that by demonstrating a way to construct such a statement, and it was ridiculously obtuse and weird, but undeniable also.
2022-05-15 18:11:24 <KipIngram   > Math guys were pretty unhappy for a while after that.
2022-05-15 18:11:26 <remexre     > most formal verification people would argue that very little code not "about computation" (e.g. an interpreter) is both believably correct and difficult to prove for that reason though :)
2022-05-15 18:12:14 <Zarutian_HTC> : (next) R> R> dup 0= if drop CELL+ >R else 1- swap @ swap >R >R then ;
2022-05-15 18:12:14 <remexre     > though there are later works that're more annoying for formal verification
2022-05-15 18:12:39 <remexre     > I've read a paper saying essentially that some always-terminating loops don't have _any_ computable loop invariant
2022-05-15 18:12:52 <remexre     > iirc the proof that said loops exist was non-constructive though :(
2022-05-15 18:13:39 <Zarutian_HTC> that (next) expects a down counter on the return stack just below where its return address
2022-05-15 18:14:15 <remexre     > oh, that's neat; yeah
2022-05-15 18:17:22 <Zarutian_HTC> in other languages say E one might construct a loop whose down counter is not accessible to the loop body or only accessible via facet that gives read only access and zeroing access (to terminate the loop earlier)
2022-05-15 18:18:41 <Zarutian_HTC> (but you could use an ejector instead, which is kind of an truncating dynamic extent continuation)
2022-05-15 18:18:57 <remexre     > truncating? like a delimited continuation?
2022-05-15 18:19:02 <KipIngram   > That's my "informal" feeling about loop invariants.  When you can write one down, it can be damn handy.  But I don't just routinely try to write one.
2022-05-15 18:19:32 <Zarutian_HTC> remexre: yeah, I just forgot the term for it.
2022-05-15 18:20:15 <KipIngram   > These days it's fairly common for me to write an infinite loop, but with a conditional return in it.
2022-05-15 18:20:33 <KipIngram   > My main loop in INTERPRET works that way.
2022-05-15 18:20:54 <Zarutian_HTC> when I am writhing say js, I find meself not using loops but iterators, map, forEach, reduce, and more functional aproach
2022-05-15 18:20:58 <KipIngram   > Actually that's not a conditional return, though - that's where the null word does a double return instead of a single one like most words do.
2022-05-15 18:21:15 <KipIngram   > EXECUTE sits at that top level, where the loop is.
2022-05-15 18:21:27 <KipIngram   > So if the word you execute does a double, it pops out of INTERPRET.
2022-05-15 18:21:30 <remexre     > yeah, for a loop like that, coinduction is usually a better approach to define the behavior than induction
2022-05-15 18:21:55 <KipIngram   > 
ACTION watchies ideas sail over his head...

2022-05-15 18:21:58 <KipIngram   > watches
2022-05-15 18:22:13 <KipIngram   > I know some CS, but not this part of it.
2022-05-15 18:22:22 <remexre     > coinduction is approximately, you show that each step of work takes only finitely much time/energy/work/whatever
2022-05-15 18:22:41 <remexre     > and that doing it maintains whatever properties you like
2022-05-15 18:22:58 <remexre     > therefore for any number of steps (even infinitely many) the properties still hold
2022-05-15 18:23:25 <KipIngram   > I see.  Ok.  So, in my case I could say that parsing any finite null-terminated string will eventually return the null word, and that executing the null word terminates INTERPRET.
2022-05-15 18:23:42 <KipIngram   > So INTERPRET will always terminate on a correctly formed finite string.
2022-05-15 18:23:56 <KipIngram   > Of course, if I stick >IN OFF in there, it'll never reach the null.
2022-05-15 18:24:04 <remexre     > If you "get to" assume the string is finite, you could use normal induction too (which is only good with finitely-large "input")
2022-05-15 18:24:25 <remexre     > the nice thing with coinduction is you can say "as long as there keeps being input" without having to say that it's finite
2022-05-15 18:24:29 <KipIngram   > Yeah - I do know enough math to know that infinities cause all sorts of weirdness.
2022-05-15 18:24:50 <KipIngram   > Normal reasoning doesn't always apply when infinite quantities are floating around.
2022-05-15 18:41:03 <Zarutian_HTC> I recommend that BBC radio series titled "A short introduction to infinities"
2022-05-15 19:20:41 <KipIngram   > remexre: If the string is in my RAM, it's finite, right?
2022-05-15 19:21:09 <KipIngram   > Though I guess a string could be produced by some function.
2022-05-15 19:21:17 <KipIngram   > And that might never terminate.
2022-05-15 19:21:26 <KipIngram   > But if it's a *stored* string, it's finite.
2022-05-15 21:25:31 <remexre     > KipIngram: 0 >IN ! needs effectively the same reasoning as an infinite string to handle
2022-05-15 22:31:18 <KipIngram   > Hey, the lunar eclipse is getting underway.
2022-05-15 22:31:29 <KipIngram   > Totality in about an hour per what my wife told me earlier.
2022-05-15 22:31:35 <KipIngram   > remexre: that makes sense.
2022-05-15 22:34:04 <remexre     > oh wow, I think this is the clearest I've ever seen one
2022-05-15 22:34:22 <KipIngram   > :-)  Excellent.
2022-05-15 23:24:43 <KipIngram   > Yeah - this is turning out really well down here.  Just entering totality now.
2022-05-15 23:56:34 <KipIngram   > Maximum eclipse in about 15 minutes.
2022-05-15 23:57:01 <KipIngram   > Full eclipse ends in just under an hour - then we get the rest of the partial.