2021-11-22 06:58:48 <neuro_sys_  > This is very neat: https://t3x.org/t3xforth/index.html
2021-11-22 07:03:00 <dave0       > cool
2021-11-22 08:02:43 <veltas      > neuro_sys_: parse-name is achievable in a standard forths, manipulating >in and accessing through either SOURCE or TIB/#TIB (depending on Forth200x / ANS)
2021-11-22 08:06:06 <neuro_sys_  > I ended up writing it in a couple different ways, and wanted to compare it to some other implementation. But thanks niedzejkob[m] I saw the reference impl on Forth200x website.
2021-11-22 08:06:32 <veltas      > Oh I thought that was a joke ( : word word ; ), didn't realise it was serious too
2021-11-22 08:07:11 <veltas      > I've implemented it here too https://github.com/Veltas/zenv/blob/master/src/zenv.asm#L2674
2021-11-22 08:07:35 <veltas      > In a standard forth replace  IN# @  with  SOURCE NIP
2021-11-22 08:07:44 <veltas      > Or #TIB @
2021-11-22 08:08:19 <veltas      > I'm sure mine is bad though, looking at it, but maybe it will make you feel better about yours lol
2021-11-22 08:08:54 <neuro_sys_  > Yes, now I'm familiar with SOURCE as a replacement for TIB #TIB >IN.
2021-11-22 08:09:31 <neuro_sys_  > It defeats the purpose, but when I write, say, parse-word in x86 asm, it is much smaller and simpler compared to its Forth version (at least the ones I wrote).
2021-11-22 08:10:58 <veltas      > I know how you feel, this was my experience with some words where I'd rewrite in assembly and it was 1000 times faster and easier/shorter
2021-11-22 08:10:59 <neuro_sys_  > Currently in my Forth I was trying to avoid/minimize hand-coded Forth as much as possible. So I wrote a quick'n dirty text interpreter mostly in asm, which works fine. But then I thought of converting asm into hard-coded Forth words, then the code gets bigger.
2021-11-22 08:11:32 <veltas      > Sometimes it's because I miss clever factorisations, sometimes maybe not. Writing FORTH is quite hard, it's harder than assembly IMO
2021-11-22 08:11:39 <neuro_sys_  > Here're a few version of parse-word I wrote on that day: https://gist.github.com/neuro-sys/db2276860b42c5d2a18bbc12145f0b1f#file-parse-name0-fs
2021-11-22 08:11:57 <veltas      > It's harder than modern assembly anyway, where most stuff is easier. 8-bit assembly (in a classic assembler) not so much
2021-11-22 08:12:15 <neuro_sys_  > veltas: I agree. Although (in theory and in my impression) the ease of programming in Forth becomes relevant when writing higher level applications.
2021-11-22 08:15:02 <neuro_sys_  > I updated my gist to include the asm version of parse-word.
2021-11-22 08:16:03 <neuro_sys_  > parse-name* I mean, not word.
2021-11-22 08:16:49 <veltas      > Parsing functions treat BL specially, you know
2021-11-22 08:16:56 <veltas      > So it's not just 32 you should check for
2021-11-22 08:17:10 <neuro_sys_  > Just keeping it simple for now
2021-11-22 08:17:14 <veltas      > parse-name acts like this too, it uses any whitespace as a delimiter
2021-11-22 08:17:33 <neuro_sys_  > I'm happy to live with only 32 for the bootstrap compiler
2021-11-22 08:19:15 <neuro_sys_  > The WORD definition here is rather nice: https://t3x.org/t3xforth/t3xforth.html
2021-11-22 08:19:34 <neuro_sys_  > I am curious about some of the formatting rules here, it looks very nice.
2021-11-22 08:24:25 <veltas      > neuro_sys_: https://pastebin.com/raw/JdsbCJY1
2021-11-22 08:24:30 <veltas      > Just tried again, untested
2021-11-22 08:24:48 <veltas      > Probably something will need fixing but you get the idea
2021-11-22 08:25:58 <veltas      > I was so disappointed with zenv's version I needed to write another lol
2021-11-22 08:27:44 <neuro_sys_  > Yeah looks much simpler. It uses SOURCE, which I suspected could simplify.
2021-11-22 08:29:54 <veltas      > Not really, when I converted SOURCE back to TIB and something like #TIB !
2021-11-22 08:30:22 <veltas      > SOURCE is just there to allow more flexibility in how interpreter buffers work
2021-11-22 08:30:44 <veltas      > TIB and #TIB are usually easier and closer to what you want
2021-11-22 08:36:16 <neuro_sys_  > Does SOURCE point to the beginning of TIB or TIB >IN @ +
2021-11-22 09:18:13 <veltas      > neuro_sys_: It gives the input as a string, so addr is at beginning and the number is size of the input
2021-11-22 11:49:41 <joe9        > is there a "safe" forth? something that restricts address arithmetic/usage, etc?
2021-11-22 11:51:46 <f-a         > address seems relatively easy to implement
2021-11-22 11:51:58 <f-a         > typings maybe would make it something different than Forth
2021-11-22 11:53:07 <eris[m]     > a 'safe forth' is not a forth :p
2021-11-22 11:53:10 <eris[m]     > its like
2021-11-22 11:53:37 <eris[m]     > a factor
2021-11-22 11:55:06 <f-a         > tho maybe some static analysis could be done
2021-11-22 11:55:11 <f-a         > without mangling the language
2021-11-22 12:00:25 <imode       > fwiw I'm building a typed forth.
2021-11-22 12:00:49 <imode       > where typechecking is done via stack effect annotations.
2021-11-22 12:00:52 <f-a         > burn the witch!
2021-11-22 12:00:59 <f-a         > (excellent idea, imode)
2021-11-22 12:01:13 <joe9        > imode, is it hosted anywhere?
2021-11-22 12:01:38 <imode       > not yet. all private work right now. I needed a forthy thing to generate code for a tiny architecture, and I needed types to ensure that the words fit together right.
2021-11-22 12:02:02 <imode       > the gist right now is that the type checking actually boils down to, basically, evaluating a grammar, or in my case, simulating a queue automaton.
2021-11-22 12:02:24 <imode       > instead of pushing values, you push types.
2021-11-22 12:02:39 <imode       > so you consume some X Y Z and produce some Q W B.
2021-11-22 12:03:08 <joe9        > that's a good idea. I like the thinking.
2021-11-22 12:03:52 <imode       > the underlying machine is all linear accesses, no RAM, so the type checking effectively needs to respect that.
2021-11-22 12:04:07 <imode       > for instance.
2021-11-22 12:04:45 <joe9        > I would love to follow what you are doing to learn if I could use those ideas, if you wish to share, btw.
2021-11-22 12:05:14 <imode       > `Integer -> Mark Bit Number` -- an integer is a marker (denoting what it is, markers can take on any value so long as we know it at compile time), a bit to denote sign, and a natural number in sequence.
2021-11-22 12:05:51 <imode       > `Rational -> Mark Number Number` -- a rational is two numbers combined.
2021-11-22 12:06:06 <joe9        > almost all types can be implemented with word and array, correct?
2021-11-22 12:06:20 <joe9        > and byte.
2021-11-22 12:06:21 <imode       > `Sequence -> Mark * Mark` -- a sequence is any segment of things delimited by two markers.
2021-11-22 12:06:51 <imode       > you can get crafty and do dependent typing by having some operations return the type representation of their values, such as Mark:StartSequence and Mark:EndSequence
2021-11-22 12:07:06 <imode       > so `Sequence -> Mark:StartSequence * Mark:EndSequence`
2021-11-22 12:07:33 <imode       > the underlying machine just uses a deque of bits, which can be treated as two stacks of bits.
2021-11-22 12:07:43 <imode       > you need to carve data types out of that via some encoding.
2021-11-22 12:08:25 <imode       > all data elements look like 0<some sequence of 1s>0<some data>
2021-11-22 12:09:35 <imode       > your program's annotation forms a grammar, and thus corresponds to some automaton.
2021-11-22 12:10:13 <imode       > the language that that automaton recognizes is regular.
2021-11-22 12:10:42 <imode       > though I guess it's more powerful.
2021-11-22 12:12:28 <joe9        > how would that work with EXECUTE?
2021-11-22 12:12:41 <joe9        > vectored execution
2021-11-22 12:12:46 <imode       > it's not a traditional forth, so no traditional words apply.
2021-11-22 12:13:15 <imode       > :- sequence > mark:start-seq * mark ; :- int-sequence > mark:start-seq int ... mark:end-seq ;
2021-11-22 12:13:30 <imode       > missing a mark:end-seq in sequence but you get the idea.
2021-11-22 12:14:03 <imode       > generic sequences vs. typed sequences, if you have value types you can ship around, that'll apply too (they're just symbols to the typechecker)
2021-11-22 12:15:24 <imode       > :- point > [ int int ] ;
2021-11-22 12:15:47 <imode       > if we defined [ to be mark:start-seq, and ] to be mark:end-seq, that'd be what you could do.
2021-11-22 12:17:11 <imode       > word definitions are roughly similar. : square ( int -- int ) dup * ; ... : sum ( seq:start int ... seq:end -- int ) ... ;
2021-11-22 12:17:59 <joe9        > that is starting to look like haskell / idris.
2021-11-22 12:18:01 <imode       > so it's "not quite typed" but "not quite untyped". it's just enough structure to make your words fit together, but loose enough to support anything from dependent typing onward.
2021-11-22 12:18:10 <joe9        > it loses the versatility of forth though(?)
2021-11-22 12:18:10 <imode       > yeah but the mechanisms are vastly easier to implement.
2021-11-22 12:18:53 <imode       > hardly. think of it as attaching some well-defined studs to the lego blocks that are words
2021-11-22 12:19:05 <imode       > so that they can fit together in only certain ways that make sense.
2021-11-22 12:20:39 <imode       > the actual type checker is simple enough to be implemented in assembly, for example. it's just a circular buffer with a linear search through a set of lhs -> rhs patterns, dequeueing the length of the lhs if it matches, and enqueueing the rhs.
2021-11-22 12:21:11 <imode       > so you have typechecking at runtime as you define new words, and you can leave things untyped if they don't make sense to type.
2021-11-22 12:26:40 <veltas      > It's one of those "I'll believe it when I see it" things
2021-11-22 12:26:46 <imode       > 
ACTION shrugs.

2021-11-22 12:27:21 <veltas      > I agree that what you describe would be quite useful and save time... if it wasn't too limiting, which I haven't given any real consideration
2021-11-22 12:27:28 <veltas      > But it just seems like there are some hurdles to clear
2021-11-22 12:27:31 <imode       > such as.
2021-11-22 12:27:52 <veltas      > How would you handle return stack manipulation, i.e. rdrop exit?
2021-11-22 12:27:58 <veltas      > That's the first concern
2021-11-22 12:28:04 <veltas      > exceptions
2021-11-22 12:29:08 <veltas      > Conditionally sized stacks
2021-11-22 12:29:10 <imode       > that's not a concern on the platform that this is targeting (because there is no return stack, I can elaborate on that further if needed), but you could solve that in a couple of ways, the first being "I know what I'm doing, don't type this".
2021-11-22 12:29:12 <veltas      > like dup?
2021-11-22 12:29:38 <imode       > * is "zero or more things", so.
2021-11-22 12:29:51 <veltas      > I think it being able to infer types would be very useful
2021-11-22 12:29:58 <imode       > : dup? ( * -- * * ) ... ; or something
2021-11-22 12:30:32 <veltas      > I mean infer stack usage and then complain if a word is misused later on, even though you didn't specify its usage
2021-11-22 12:30:46 <neuro_sys_  > That's what I've been thinking too if/when I come to that point to start implementing it. I believe parsing stack effect comments and making sure the sequence of words match in terms of their stack effect signature should be relatively straight forward during compilation. But maybe I'm wrong.
2021-11-22 12:30:50 <imode       > yeah. you can usually infer that just from the body of the word.
2021-11-22 12:30:56 <veltas      > Maybe don't use comments as type specifications, so that you have a choice whether to use comment or the signature
2021-11-22 12:31:18 <imode       > again, I should stress that this is definitely not a traditional forth by any means.
2021-11-22 12:31:34 <imode       > it just looks enough like forth and smells enough like forth that it's worth calling it forthish.
2021-11-22 12:32:33 <imode       > the architecture is strict harvard, so this is more like a compiler than a full forth system. there's no RAM, the only backing data structure is a deque of bits.
2021-11-22 12:32:49 <imode       > and launching processes that can communicate with eachother.
2021-11-22 12:33:22 <joe9        > limbo is similar
2021-11-22 12:33:28 <joe9        > to what you describe
2021-11-22 12:33:35 <imode       > as in, rob pike's limbo?
2021-11-22 12:33:40 <joe9        > yes,
2021-11-22 12:33:49 <joe9        > inferno
2021-11-22 12:33:51 <imode       > huh, I thought that VM was a traditional register VM.
2021-11-22 12:34:00 <joe9        > yes, that is the only difference.
2021-11-22 12:34:05 <joe9        > frow what I can tell.
2021-11-22 12:34:16 <joe9        > that is just a simple fix to make that stack based.
2021-11-22 12:34:26 <imode       > that VM still has RAM to back it though, right?
2021-11-22 12:34:27 <joe9        > It is just how the vm sees stuff.
2021-11-22 12:35:48 <veltas      > neuro_sys_: You sort of end up tracking stack usage when you write even simple optimisations, so building this kind of static checking into a 'normal'ish forth makes sense too IMO
2021-11-22 12:36:22 <imode       > now you have me interested in implementing `dup?` lol.
2021-11-22 12:36:46 <neuro_sys_  > Yes, but like you pointed there are shortcomings or restrictions with variable length stack, and messing with return stack. I could definitely do away without ?dup (and other variable length stack effects).
2021-11-22 12:37:54 <neuro_sys_  > I just heard Chuck mention in a video he doesn't like ?dup and similar.
2021-11-22 12:38:09 <imode       > : dup? ( bit * -- * * ) ;
2021-11-22 12:38:18 <imode       > take a boolean and a thing, give me back two things.
2021-11-22 12:39:50 <neuro_sys_  > I was also thinking for a very rudimentary "type checking", it could simply make sure the "ccc" used in the stack effect matches? E.g. : word1 ( foo bar -- baz ) ; : word2 ( baz -- ) ; will ensure that word1 word2 is valid but not in reverse order.
2021-11-22 12:40:55 <imode       > you almost need a `dup` but for types. I can _do_ that.
2021-11-22 12:42:22 <imode       > : dup? ( bit -- dup ) cond dup end ;
2021-11-22 12:42:35 <imode       > we take a bit and then dup whatever's on the type stack.
2021-11-22 12:43:07 <neuro_sys_  > imode: Is this dynamic type checking? Is it not possible to sort this out during compilation?
2021-11-22 12:43:16 <imode       > it's both.
2021-11-22 12:43:25 <imode       > in my case, I can't do anything _but_ sort this out during compilation.
2021-11-22 12:43:34 <imode       > because I have to generate code.
2021-11-22 12:43:48 <imode       > so if your program-as-a-whole typechecks, code generation happens.
2021-11-22 12:43:58 <imode       > otherwise I leave a nice note as to where things broke.
2021-11-22 12:46:16 <imode       > I see this as "you're using one machine to ensure that another machine isn't doing dumb things"
2021-11-22 12:46:25 <joe9        > it seems so close to dependent type programming languages.
2021-11-22 12:46:48 <joe9        > that it might be worth exploring them instead of forth, imho.
2021-11-22 12:47:02 <joe9        > ats, agda, idris
2021-11-22 12:47:18 <imode       > i.e you're executing a symbolic program on one machine that takes a summary of the execution of another machine (the program that it'll execute) and says "this is good" or "no it's not".
2021-11-22 12:48:02 <imode       > if yes, code generation happens and/or execution just proceeds. if no, code generation doesn't happen and/or execution stops.
2021-11-22 12:49:04 <imode       > joe9: dependent typing is just "let's allow values into the type system".
2021-11-22 12:49:07 <imode       > which I'm not opposed.
2021-11-22 12:49:19 <imode       > but it also means that typechecking is undecidable.
2021-11-22 12:49:33 <imode       > there's a way to construct a computation that effectively spins.
2021-11-22 12:49:44 <imode       > within the type system itself.
2021-11-22 12:53:23 <imode       > in my scheme, because it either is equivalent to or subsumes dependant types, you can effectively type functions with their actual computations and return actual values, such that the compiler/type checker actually runs these things.
2021-11-22 12:54:43 <imode       > : 10squared ( 10 -- dup *:int ) 100 ;
2021-11-22 12:54:45 <imode       > for instance.
2021-11-22 13:03:07 <joe9        > there are probably some techniques or safe practices to lock down forth code too. Something to prevent malicious asm injections, etc.
2021-11-22 13:03:28 <joe9        > in the code definitions, etc.
2021-11-22 13:03:38 <joe9        > some sanity checks around fetch and store
2021-11-22 13:04:00 <joe9        > anyone have experiences on it?
2021-11-22 13:15:46 <Zarutian_HTC> no, but do look into how FCODE on OpenFirmware is handled
2021-11-22 13:27:11 <joe9        > Zarutian_HTC: thanks.
2021-11-22 13:30:51 <joe9        > I am looking at felixforth code and it has this definition for quit http://okturing.com/src/12517/body
2021-11-22 13:31:15 <joe9        > I cannot figure out the reason for the m_exit after the jump to L253
2021-11-22 13:31:24 <joe9        >  dd m_jump
2021-11-22 13:31:24 <joe9        >  dd L253
2021-11-22 14:23:56 <Zarutian_HTC> probably result of macro expansion
2021-11-22 15:47:26 <imode       > joe9: have you ever seen metamath?
2021-11-22 15:47:31 <imode       > it's a proof verification engine.
2021-11-22 15:47:38 <imode       > stack-oriented theorem validator.
2021-11-22 16:16:45 <joe9        > no, will check it out. Thanks.
2021-11-22 19:41:15 <niedzejkob[m]> metamath is stack based? I didn't get that impression when I looked at it
2021-11-22 20:29:00 <imode       > yeh.