mark4 changed the topic of #forth to: Forth Programming | do drop >in | logged by clog at http://bit.ly/91toWN backup at http://forthworks.com/forth/irc-logs/ | If you have two (or more) stacks and speak RPN then you're welcome here! | https://github.com/mark4th
dave0 has quit [Quit: dave's not here]
<KipIngram> Ok, so after thinking about it for a while, I think that all I need to do is change all of those variables (base addresses, here variables, context, current) and then launch into compiling the system and never come back to the console until it's all done and I've restored the variables.
<KipIngram> That way if an error occurs at any point, my error recovery will restore those variables using the recovery image.
<KipIngram> I'll want the virtual instruction words that generate target code to be part of my host system - I'll actually be executing those words while building target primitives. But everything beyond that will get looked up in the target dictionary.
<KipIngram> All I really need to do to make this work is make sure thaat I don't use the register copies of the base addresses for compiling. Always the variable version, so that I can change them. But the proper RUNNING of the system never relies on those variables - the registers just have to be right.
<KipIngram> So it all should work just fine.
cheater has joined #forth
<cheater> insert may the forth joke here
<tabemann> back
<tabemann> hey guys
logand` has joined #forth
logand has quit [Ping timeout: 252 seconds]
<KipIngram> Hey tabeman...
lispmacs[work] has quit [Remote host closed the connection]
boru` has joined #forth
boru has quit [Disconnected by services]
boru` is now known as boru
LispSporks has joined #forth
dave0 has joined #forth
<dave0> maw
<siraben> remexre: I thought up of a small-step operational semantics for a Forth-like language
<siraben> it occurred to me that Hoare logic could be used as well to decorate the programs, instead of variables you would use stack offsets (like de bruijn indices)
<siraben> then you could truly assert something like, `{ #0 = n } FACT { #0 = fact n }` for a program that calculates factorial
<remexre> ooh, nice
<siraben> I would make constructs like REPEAT, WHILE etc. primitive however
<siraben> then compile to a stack-baesd VM with jumps and all that
<siraben> until I'm familiar with proving fiddly things about such a machine, I'll stick to that higher-level smallstep operational semantics
<siraben> remexre: wrt. conditions, should the stack be typed then?
<remexre> conditions as in CL conditions?
<siraben> conditionals*
<remexre> ah
<remexre> my personal view for what I'm doing in my forth is, it's more useful to have the stack "types" instead be predicates on machine state
<siraben> Ah ok, so the conditionals just operate on numbers rather than booleans?
<remexre> yeah
<siraben> I see. So `state = list nat` then
<remexre> so I'm planning to do mine over the whole state of an aarch64 CPU
<remexre> and then have a helper to get the stack's contents
<remexre> but if your forth doesn't have a stack accessible as memory (and has unbounded nats for values!) then sure
<siraben> Oh I see. I prefer to start more idealistic then gradually add more realism to the formalization
<siraben> with nats as values on the stack, it'd be a very unique Forth for sure, haha
<remexre> yeah, I'll probably do a trial run with a simpler "model" of a forth, where each primitive is one instruction, no paging exists, things are at nice small-numbered addresses, etc
<remexre> but I'll probably try to have the stack in memory all the time, because that's like, a really big change
<siraben> it sounds tougher to formalize things when the stack is also in memory
<siraben> like, you'd have to bound the height of the stack to prevent collisions?
<remexre> yeah
<remexre> but I should know what stack depth each primitive needs
sts-q has quit [Ping timeout: 260 seconds]
sts-q has joined #forth
<siraben> right
<siraben> proving stack-based factorial correct should be a good early milestone, to at least see it works
<siraben> hm, then I would need to read up on the mutable references section of PLF
<siraben> to model ! and @ properly
<remexre> yeah, I'm not gonna be any help there, lol; I've got a friend who does... something with separation logic, I've been meaning to get some stuff from him to read up on
<siraben> oh yeah, sep logic would be cool
<siraben> remexre: see also another good book: https://github.com/achlipala/frap
LispSporks has quit [Ping timeout: 245 seconds]
<remexre> ooh, I'll put that on my list
<remexre> thx
<siraben> remexre: why would you need separation logic at first though
<siraben> isn't that for like, reasoning with pointer-based structures?
<siraben> or maybe it applies to everything involving memory, I forget
<remexre> it's basically for things like
<remexre> { #0 = 5 } +1 { #0 = 6 }
<remexre> how do I know that #1 didn't change
<siraben> oh you're doing stack in memory right
<remexre> yeah
<siraben> because that'd be a pretty easy thing to derive for me, where I just model the language with a stack initially
<KipIngram> That all sounds interesting as hell. I wish I could follow it a bit better.
<siraben> but I see
<remexre> well, my point was more, I didn't write anything about #1, so I want to be sure it didn't change; hoare triples don't guarantee this by default (as I understand them at least)
<siraben> oh right, in Hoare logic you really only make assertions about things you care about
<siraben> so there might be a situation where #1 actually changes but you never checked, since you only asserted #0's value after +1
<siraben> I just remembered yeah, when I showed { X = n } fib { X = fib n }, I completely discarded information about then intermediate variables Y and Z
<remexre> KipIngram: yeah, logical foundations ( https://softwarefoundations.cis.upenn.edu/lf-current/index.html ) is the standard text for learning about some of this stuff :)
<siraben> KipIngram: when we write { P } c { Q }, we mean that P and Q are assertions about the state, and that if P holds before running c, then Q holds after running c
LispSporks has joined #forth
<KipIngram> Cool - I will look that over.
<KipIngram> BTW, I found another old calculator one of my kids used over the years. I don't know for sure it works - need to find some fresh batteries.
<KipIngram> This one is a TI-84.
<siraben> KipIngram: nice, I have a Forth for that!!
<siraben> you need to try out my forth then :)
<siraben> it's annoying that TI called it TI-84+ but there is no TI-84 model, hah
<KipIngram> Oh, superb.
<KipIngram> Yeah - I'd like to. I'll try to get the thing fired back up tomorrow.
<siraben> KipIngram: latest release (as an .8xp file) here https://github.com/siraben/ti84-forth/releases/tag/1.1.0
<KipIngram> Cool
proteusguy has quit [Remote host closed the connection]
LispSporks has quit [Ping timeout: 276 seconds]
Zarutian_HTC has quit [Ping timeout: 246 seconds]
nihilazo has quit [Quit: Gateway shutdown]
proteus-guy has quit [Ping timeout: 265 seconds]
<siraben> KipIngram: just realized there's a hash mismatch between what I'm building and what the release says, it's probably because I finally stabilized the version of the assembler I was using heh
<siraben> i'll do a minor bump then
<KipIngram> I'm guessing I need to scruff up some sort of cable for it?
<siraben> Yes, I forget what kind of cable it is but it's the port that is NOT the I/O port
<siraben> so it looks like a printer cable
lonjil has quit [Quit: No Ping reply in 180 seconds.]
lonjil has joined #forth
mtsd has joined #forth
proteus-guy has joined #forth
mtsd has quit [Ping timeout: 252 seconds]
Zarutian_HTC has joined #forth
gravicappa has joined #forth
spal has joined #forth
andrei-n has joined #forth
nihilazo has joined #forth
* KipIngram sighs.
<KipIngram> I help moderate a sub over on Reddit. Its topic is a fictional urban fantasy series referred to as The Dresdenn Files.
<KipIngram> Guy is a wizard who advertises in the phone book in Chicago.
<KipIngram> Standard setup for a lot of such books - the supernatural is real, and various flavors of vampires, werewolves, fairies, and so on are floating around out there, and there are "supernatural nations" operatinng behind the scenes.
<KipIngram> There are 17 novels in the series so far, and it's expected to get on up to 22-23 and then we get a big "climactic trilogy."
<KipIngram> The overall story arc has been outlined from the beginning, and the author's been feeding it out to us for a little over 20 years.
<KipIngram> Anyway, my opinion of the series could not be higher. I regard the books as amazingly good - very rich world building, characters you can really get into, the works. Top drawer stuff.
<KipIngram> But it seems like every other week someone's got to get on the reddit and gripe about "misogyny in The Dresden Files."
<KipIngram> We see the world from inside the head of the main character, and part of what we get is very... "vibrant" descriptions of his inner reactions to attractive women - some of whom are supernaturally attractive and therefore produce more than the normal response.
<KipIngram> Supernatural aspect aside, it's a common thing to find in "noir detective fiction."
<KipIngram> I regard those descriptions as extremely accurate - we are, after all, supposed to be in the head of a young American male.
<KipIngram> But people just get so worked up over it - I guess I'm just too old a dog to get into the "new way of thinking" on things like this. :-|
deep-thought has joined #forth
deep-thought has quit [Quit: Leaving]
<KipIngram> AHA - there's something I overlooked.
<KipIngram> If I change the base address variables the way I have things set up now, to compile a target image, then if an error occurs the saved recovery image will be written back over the TARGET. That won't do. I have to have separate copies of those base address variables for those two purposes.
<KipIngram> So I was wrong earlier when I said the variables weren't used for anything other than compiling.
<KipIngram> Ok, added comp.b and comp.h as copies of base.b and base.h. The comps will be the ones to redirect to the target image buffer.
<KipIngram> I don't think there's any reason I can't just set the system CURRENT to a vocabulary in the target region; that ought to work.
<KipIngram> I probably don't want searches to pass into the system dictionary while I'm building the target - that would let some tacky errors creep in.
<KipIngram> I'm still scratching my head a little over that part (the search path).
<KipIngram> Oh, hmmm. Another potential gotcha.
<KipIngram> I mentioned earlier that when I parse a word out of the input stream I place it in the correct position to be able to promote it to a dictionary item later on.
<KipIngram> Well, if I want that to work when building a target, THAT also needs to move into the target space. Because that's where the dictionary I'm building is.
<KipIngram> So even though I'm RUNNING code in the system space, that needs to migrate.
<KipIngram> Oh wait - that may already be taken care of.
<KipIngram> Yeah, I think my dictionary pointer dp.h drives that now, so when I move it to the target it will work out naturally.
<KipIngram> Yes - that's correct. I actually have a word
<KipIngram> : wbuf dp.h @ 2+ ;
<KipIngram> The 2+ is to skip over the bytes where the link will need to go.
<KipIngram> One thing is clear, though - the entire build of the target system needs to be one long source load. Can't stop in the middle and return to the console. I've got to get the pointers all restored before I try to snapshot the next system image for error recovery.
<KipIngram> You know, I see that there will be a limitation of this approach.
<KipIngram> I won't be able to build a target that has a different dictionary architecture from the running system. Since I'll be using the running system words to search and build the target dictionary.
<KipIngram> That also seems to mean I can't change cell size. And there may be endieness compatibility requirements too.
<KipIngram> That's slightly disappointing. I'd envisioned this as a porting tool. It may turn out to only be REALLY good for modifying my system on the same platform.
actuallybatman has quit [Ping timeout: 252 seconds]
glubs9 has joined #forth
<glubs9> hey, I am working through starting forth chapter 11 and it doesn't define control structure words. Do yall know where I could find a source on how control structure works in forth? thank you kindly
glubs9 has quit [Quit: Ping timeout (120 seconds)]
glubs9 has joined #forth
<KipIngram> If you can chase down a copy of McCabe's "Forth Fundamenntals," you'll be set up. Volume one is under the hood details of Forth's internals; volume two is a index of Forth words with definitions.
<KipIngram> It's out of print, though.
<KipIngram> You might land a copy on eBay.
<glubs9> thank you :) I will check it out!
<KipIngram> If you can't find anything I can describe how they work for you.
<KipIngram> They all follow the same general principle.
<KipIngram> Here's volume 2 on Amazon:
<KipIngram> Kind of pricy though. :-|
<glubs9> yeah, bit of a shame.
<glubs9> it's actually in a library near me so I might go and check that out
<KipIngram> Volume 2 doesn't really "explain" anything - just gives source listing for the words.
<KipIngram> Excellent.
<glubs9> I will be seeing you, thank you again for the help!
glubs9 has quit [Client Quit]
<siraben> remexre: so... I have a small-step semantics for Forth now :)
<siraben> easier than expected
<siraben> and I did verify factorial
<siraben> `Definition factorial : com := <{ 1 begin over O= not while over * swap 1 - swap repeat swap drop }>.`
<siraben> and `Example fact6 : forall st p, <{ 3 factorial p }> / st -->* p / (N 6 :: st).` was proved by `repeat econstructor.`
<siraben> it'd be fun to adopt all the equiv, hoare, hoare2 chapters to work with Forth!
<veltas> What are you using to evaluate that?
<siraben> I haven't verified it for all n yet, proof is a bit tedious
<siraben> veltas: Coq
<KipIngram> Here's factorial in my system:
<KipIngram> : fact dup : (fact) 1- swap over * swap dup 1 = 0=me drop ;
<KipIngram> If I wanted to hide the (fact) I could put .: before it instead of : and then execute .wipe afterward.
<KipIngram> I could make it a little shorter but that version doesn't have all of the conditional loop words.
<KipIngram> 0=me is one that it did have, so I hoop jumped a little to use it.
<siraben> KipIngram: heh, if you could describe how your conditional works then I could provide a formal semantics for them!
<siraben> right now the Forth I have only has the stack as state, no memory yet.
<KipIngram> 0=me will recurse to the beginning of the definition (with a jump - not a call) if the flag is 0.
<KipIngram> The flag is consumed.
<KipIngram> If flag is non-zero, execution continues forward.
<KipIngram> I'm thinking of including a bunch of words from my old HP 41 in the system I'm building now.
proteusguy has joined #forth
<KipIngram> Particularly access to the Y, Z, and T regs.
<KipIngram> So the equuvalent of ST* Y would be valuable here.
<KipIngram> It would cut out quite a few stack diddles.
<KipIngram> I could envision something like this:
<KipIngram> : fact 1 swap : (fact) ysto* 1- .0=me drop ;
<siraben> Ooh, heh
<KipIngram> The . at the front of 0=me makes it not consume the argument.
<KipIngram> That does a couple of extraneous multiplications by 1, but it's terse. :-)
<KipIngram> Oh, maybe this is better:
<siraben> I like tricks like that, but when formalizing things, I keep the constructs really simple, to reduce the number of cases to deal with, naturally
<KipIngram> : fact dup 1- : (fact) ysto* 1- .0=me drop ;
<KipIngram> That wouldn't work for 1, though.
<KipIngram> This would fix it:
<KipIngram> Oh, never mind.
<KipIngram> Not quite.
<siraben> hmm
<KipIngram> : fact dup 1- (fact) drop ;
<KipIngram> : (fact) ysto* 1- .0=me ;
<KipIngram> Oh, wait - I forgot the fix for 1
<KipIngram> : fact dup 1- (fact) drop ;
<KipIngram> : (fact) .0=; ysto* 1- .0=me ;
<KipIngram> I think that would work, but the conditionals aren't in my system to test it.
<KipIngram> Anyway, I'm a fan of my conditional words. :-)
<KipIngram> In that last one the .0=me could just be me, no condition.
<KipIngram> Since it loops back and picks up the conditional return at the beginning of the loop.
<siraben> remexre: you'll need to put this in the PLF folder (because it imports Smallstep) https://gist.github.com/siraben/4361eca01cb0395cfa3c993e0dd380f3
<siraben> I gave up on proving `forall (n : nat) st p, <{ factorial p }> / (N n :: st) -->* p / (N (fact n) :: st).`, maybe I'm not using the right lemmas in the inductive case
<siraben> Some notion of congruence would really help here, hm.
<siraben> Currently I have, skip, sequencing, pushing literals, + - *, dup, drop, swap, over, O=, not, if, while
<proteusguy> Hey you guys are actually producing forth code?!?!? YOU CAN'T DO THAT HERE!!! :-)
<siraben> proteusguy: an operational semantics for Forth!
<proteusguy> even worse! gads!
<siraben> hah, how so?
<proteusguy> (I'm just kidding - it's refreshing to see actual forth happening in real life)
<siraben> it's a precise model of Forth, i've been meaning to write it for a while but didn't find anyone else's implementation online
dave0 has quit [Quit: dave's not here]
<proteusguy> Don't you know the reason we tell everyone to write their own forth is so they'll get so distracted that they'll never write actual real forth code that makes it out into the wild. This is how we control the "Forth code supply" much in the manner of Bitcoin's "proof of work". Therefore the forth code I wrote in 1985 is still super valuable!
<MrMobius> haha ya someone observed that there are a lot more forth implementations than useful forth programs
<KipIngram> ah man, where's my mind. not ysto* - it should be y*!
<proteusguy> MrMobius, they aren't wrong! ;-) haha
tech_exorcist has joined #forth
Zarutian_HTC has quit [Ping timeout: 252 seconds]
actuallybatman has joined #forth
Zarutian_HTC has joined #forth
logand` has quit [Read error: Connection reset by peer]
logand` has joined #forth
Zarutian_HTC has quit [Remote host closed the connection]
Zarutian_HTC has joined #forth
<KipIngram> siraben: That TI 84 calculator has what looks like a mini-USB connnector on it, and on the other side of the top it has a round connenctor with |/O under it.
<KipIngram> The round one doesn't really look like a data connection to me - the mini-USB of course does.
<KipIngram> Yes - mini-USB; I found a cable and checked.
<siraben> KipIngram: nice, I didn't know it was called mini-USB
<siraben> great. there's programs on every major OS to send data over
<siraben> if you don't mind non-free software, there's https://education.ti.com/en/products/computer-software/ti-connect-ce-sw
<MrMobius> KipIngram, you have tow old claculators now?!
<MrMobius> looks like the TI-84+ still has the old 2.5mm jack used for data before as well
<KipIngram> I just found a couple that my daughters used to use over the last couple of days. Unfortunately, the TI-84 doesn't seem to be working.
<KipIngram> I just put new batteries in it - no love.
<KipIngram> The other one is an nSpire, and you guys said it's not very hackable.
<KipIngram> Aha! It's working.
<KipIngram> The TI-84.
<KipIngram> I had to replace the button battery too, and I guess I found and mashed the reset button.
<KipIngram> TI-84 Plus, 2.43. RAM cleared.
<KipIngram> And a flashing cursor.
<siraben> KipIngram: nice!!
<KipIngram> So I can load your Forth onto this?
<KipIngram> I may have to wait until my new computer comes.
<siraben> yep
<KipIngram> My employer MacOS can't write to USB.
<KipIngram> They're jerks.
<siraben> Oh wow, how restrictive
<KipIngram> It's so employees can't steal IP.
<KipIngram> But...
<siraben> are you sure usb doesn't work at all?
<KipIngram> We can plug a DVD drive into the port and it works fine.
<KipIngram> So we can burn DVDs.
<siraben> lol there's other ways to get data out for sure
<KipIngram> Well, I can't manage books on my ereader, or music on my iPod, and I can't run that little Cortex M4 dongle.
<KipIngram> But I do have a new computer on order.
<KipIngram> So all will be well.
<KipIngram> My first new computer "for me" in over 9 years.
<KipIngram> Ok, good - it seems to be working just fine.
<KipIngram> Miraculously I had some A76 button cells - that sort of surprised me.
<KipIngram> I went on a binge 12-15 years ago where I was collecting wristwatches.
<KipIngram> So I bought some little tools and a bunch of different kinds of batteries.
<KipIngram> I'm not sure the A76 was for a watch, though - it's a little thick for that.
<siraben> KipIngram: that TI-84+ was used by your daughter for school right?
andrei-n has quit [Read error: Connection reset by peer]
<KipIngram> One of them, yes. One of the older ones, I suppose - it's older than the nSpire I found a couple of days earlier.
<KipIngram> Maybe I got the batteries for it, back then.
<KipIngram> Anyway, I figured there was maybe a 30% chance I'd have the right one, but I hit the jackpot. :-)
<KipIngram> I'll definitely take your Forth for a test spin. :-)
<MrMobius> KipIngram, i put lithium AAAs in all my calculators since they dont leak
<KipIngram> Hmmm. What did I just put in this one? Lemme check.
<KipIngram> Nah, these are alkalines.
<KipIngram> They're brand new, though - I'll pick up some lithiums sometime soon.
<MrMobius> ya almost always alkaline unless youre trying to get lihtiums
<MrMobius> countless calculators have met their end by leaky batteries...
<KipIngram> No doubt.
<KipIngram> These are probably trustworthy for a little while at least.
<KipIngram> I was pretty bummed when it wasn't working.
<KipIngram> Happy it worked out.
<KipIngram> Uh oh.
<KipIngram> That's not a good sign.
<KipIngram> I just picked it up and turned it on again, and it said RAM cleared again.
<KipIngram> I'd done a few calculations on it - that was behindn me.
<KipIngram> Looks like it cleared itself again.
<siraben> KipIngram: it might be good to reflash the OS
<MrMobius> i think the curved look of it is terrible. ti and casio made really janky looking calculators then hopefully noticed how dumb it looked and changed most of them back to a normal looking alyout
<MrMobius> layout
<MrMobius> could it be the backup battery?
<siraben> KipIngram: yeah, check the backup battery as well (it's a button)
<KipIngram> I just replaced that too, but those have been around for a while.
<KipIngram> I'll keep an eye on it.
<KipIngram> I took the back cover off - maybe that let the backup battery break contact.
<KipIngram> I'll have a while to tinker with it before my computer comes.
<siraben> nah, back cover shouldn't affect
<siraben> it's screwed with a panel
<KipIngram> Oh, you're right.
<KipIngram> Hmmm. Well, we'll see.
<siraben> hah, I remember taking the back cover off so many times (because I crashed the calculator when I was hacking on it) that I eventually lost the back cover
<siraben> got a replacement back cover though
<MrMobius> backup batteries usually never leak
<KipIngram> Does it use the backup battery all the time when it's off, or is that there just to cover when you've pulled the main batteries?
<siraben> backup battery doesn't do much IIRC
<siraben> or maybe mine just died a long time ago
<MrMobius> it would make sense for the main batteries to power it all the time. thats how the handful of circuits ive seen for that type of thing work
<KipIngram> Yeah, that's how my old ones worked.
<KipIngram> I think I may need to clean the battery contacts.
<siraben> Yeah maybe try that
<siraben> If that fails, maybe a reflash is in order
andrei-n has joined #forth
<remexre> good morning all :)
<remexre> siraben: maybe the factorial_correct one would be easier with a multi_append sorta thing? I had the full nil/one/cons/snoc/append set in the thing I did
<siraben> remexre: oh, could you elaborate on multi_append?
<remexre> ah, never mind, I just actually looking in smallstep.v, they call it multi_trans
lispmacs[work] has joined #forth
<remexre> I just mean that when you're working with small-step, you really want to be able to ignore the structure of multi and just talk about "there's a subsequence with this type," so adding a bunch of list helpers for multi might be useful
<remexre> but if they already define a bunch, that's probably not useful to say :)
<siraben> Yeah I tried various transitivity assertions but the persistent problem was reassociating the sequencing
<siraben> I might really want to do big-step for this instead, hm.
<remexre> the reassociating feels automatable, but I'm not at *all* comfortable with ltac, lol
<siraben> hm, I can't reassociate because I don't have a notion of program equivalence
<siraben> like, how does it make sense to rewrite A -->* B to C -->* B where A ≅ B?
<siraben> Oops I mean A ≅ C
<siraben> let me know if you somehow manage to prove factorial_correct :)
<remexre> oh, I was thinking something easier; being able to split an A-->*C into A-->*B /\ B-->*C
<siraben> showing `begin dup O= not while dec repeat` always takes the top argument to 0 was pretty doable
<siraben> oh yeah but the problem is A -->* B still has the weird associativity of SSeq
<siraben> SSeq (SSeq A B) C instead of SSeq A (SSeq B C)
<siraben> and I'd really like the latter because, you know, Forth programs are linear
<remexre> ah
<remexre> hm
<siraben> The `CS_SeqAssoc` small-step rule is commented out because if I add it it breaks my automated proof of determinism
<siraben> but that was a possible hack
<remexre> well, you could define a really weak equivalence that's just "I can reassociate SSeq", I suppose
<remexre> but yeah, agreed that's kinda displeasing
<remexre> maybe doing the proof in terms of continuations could help
<siraben> small-step equivalence is tricky, doesn't help that PLF doesn't cover it
<siraben> oh yeah, I read about using a continuation parameter to make small-step better
<remexre> like, forall k, (k -->* c) -> (Seq my_program k -->* c) might be an easier theorem
<remexre> yeah, the CCC paper does this and I found it really neat+helpful
<siraben> I'm still fumbling my way around ltac, it's like part Prolog and part follow your nose
<remexre> er, that type's not quite right
<remexre> forall k n tl, (k / (fact n :: tl)) -->* c) -> (Seq my_program k / (n :: tl) -->* c) is probably closer
<siraben> Ok I see, but what's c here?
<siraben> also, what would my_program be
<remexre> arbitrary state after continuation
<remexre> factorial
<siraben> so this is if I had a continuation-passing semantics?
<remexre> I don't think it (necessarily) needs changes to the semantics, but having the continuation gives you some "slack" to talk about parts of the program
<remexre> because you can just shove things into the continuation, while keeping the same inductive hypothesis
<siraben> Hm, I see.
<siraben> I might need to revisit this later, heh
<remexre> yeah, these are pre-coffee thoughts too, so I might be slightly confused as well :P
<remexre> I'll try doing the proof w/ a different inductive hypothesis and see if it gets me anywhere
<siraben> Ok, thanks. If you have any problems loading let me know
<remexre> got it now, thought I didn't realize I had to run make in the PLF dir first, lol
<siraben> petition to make SF's stuff its own library, haha
<siraben> it's a nice self-contained universd
<siraben> universe
<siraben> it's late here, will return in the morning
<remexre> ok, good night!
f-a has joined #forth
f-a has quit [Read error: Connection reset by peer]
<KipIngram> Looks like I got a bad batch of batteries. It already is telling me they need replacing.
<KipIngram> That's quite lame.
f-a has joined #forth
<KipIngram> I ordered some L92 Lithium ones and also a fresh pack of 76a button batteries.
<KipIngram> Well, the coq link you gave me yesterday, siraben - not clicking yet. :-)
<KipIngram> But I don't think I've gotten to anything very meaty yet.
<KipIngram> Ok, I had bought 8 AAA bateries. I've swapped them out one-by-one and now seem to have a reliable set in there. Seems to be behaving.
f-a has left #forth [#forth]
proteus-guy has quit [Ping timeout: 240 seconds]
proteus-guy has joined #forth
<mark4> KipIngram, "Lonter lasting batteries" is marketing wank. it does not mean lasts longer in your device, it means lasts longer on the shelf before sale
<mark4> which does not mean "lasts forever"
<mark4> not sure if this was BS or legit but one youtuber said that charged batteries bounce bettr than dead ones.. i never tested taht lol
<MrMobius> haha ya these lithiums say lasts 20 years but fine print says on the shelf
<MrMobius> current output graphs to look better than lithiums though especially for high drain stuff
mark4 has quit [Remote host closed the connection]
Zarutian_HTC has quit [Remote host closed the connection]
gravicappa has quit [Ping timeout: 252 seconds]
f-a has joined #forth
f-a has quit [Read error: Connection reset by peer]
f-a has joined #forth
Zarutian_HTC has joined #forth
f-a has quit [Read error: Connection reset by peer]
f-a has joined #forth
mark4 has joined #forth
andrei-n has quit [Quit: Leaving]
tech_exorcist has quit [Ping timeout: 268 seconds]
Zarutian_HTC has quit [Read error: Connection reset by peer]
Zarutian_HTC has joined #forth
<KipIngram> Hey, are any of you familiar with the "rougue" HP calculator the 34S?
<KipIngram> It's an aftermarket re-flash of a stock HP calculato, with key stickies to relabel the keys.
<KipIngram> It was an attempt to make the "ultimate" scientific non-graphing calculator.
<KipIngram> Has a huge amount of stuff in it.
<KipIngram> I actually have two of those.
f-a has left #forth [#forth]
<KipIngram> I don't like it as much as I liked my HP 41CV, but it does have one of the "better style" keyboards with that nice click action.
<KipIngram> I just found the HP 41 easier to program.
<KipIngram> The 41 would take multiple keystrokes and use them to build up an "idiomatic operation," and that would then show up as one step in your program. You could see the result of those keystrokes all at once when your program viewer was pointed at the right place.
<KipIngram> The 34S, on the other hand, literally treats each keystroke as a step. So you wind up with a lot more steps and you can only see one of them at a time on the screen. So it's just a lot harder to keep your program in mind somehow.
<KipIngram> Hey siraben, can you post that link to your Forth again please?
<KipIngram> The TI-84 Forth, I mean.
<KipIngram> Thanks!
dave0 has joined #forth
<dave0> maw
<lispmacs[work]> what does maw mean?
<cmtptr> it's the fourth boss in jedi knight
<cmtptr> er, third i guess. the fourth dark jedi, but you fight two of them at once so i guess they count as one boss
<lispmacs[work]> did that somehow become a greeting in pop culture?
<cmtptr> yup, where have you been?
<lispmacs[work]> somewhere not playing star wars games
<cmtptr> ohoho this guy
<cmtptr> what sort of games were you playing, then?
<KipIngram> :-)
<lispmacs[work]> in the past few years I have played freeciv, warzone2100, freeorion, pioneer, and a few other similar free software games. But I have beat them all and currently don't have any gaming interests
<lispmacs[work]> what i do for fun currently is work on a FlashForth programming project
<cmtptr> i just recently started playing rainbow six 3 again
<cmtptr> i hadn't touched it since high school
<cmtptr> great game
<cmtptr> first two are probably good too, and it's been even longer since i've played either of those, but good luck getting them to run on a modern pc