Zarutian_HTC has quit [Read error: Connection reset by peer]
<cmtptr>
actually it's wem flipped upside down
<cmtptr>
no, that's not right either. what a colossal failure on my part
<KipIngram>
It was still fun.
<KipIngram>
Like Back To The Future: Holes you could sail a battleship through, but still collosally fun.
jedb has quit [Ping timeout: 245 seconds]
jedb has joined #forth
boru` has joined #forth
boru has quit [Disconnected by services]
boru` is now known as boru
<MrMobius>
do you guys know if there's a forth that you can insert into your C project for debugging that can access the C variables?
sts-q has quit [Ping timeout: 246 seconds]
dave0 has joined #forth
jedb has quit [Quit: Leaving]
jedb has joined #forth
<mark4>
i think that would be almost impossible
sts-q has joined #forth
<siraben>
remexre: ok, the Hoare2 chapter is pretty awesome, I went through it recently
<siraben>
by annotating the fiboancci program with Hoare triples (and the appropriate loop invariant), Coq was able to automatically verify correctness, since Hoare logic is compositional and all you have to do is check local logical consistency
<siraben>
I wonder if there's a topological interpretation of that, being consistent is a local property, so maybe it makes sense to impose a lattice structure where the meet of two program fragments exists iff they agree logically
<siraben>
Then you just take the topology induced by the principal filters of elements of the poset
<siraben>
Just purely speculating, would need to understand more about logics in general to say for sure
<MrMobius>
mark4, i think youd have to insert the forth into the assembly the compiler generates unless you were gonna try to parse the C yourself
<MrMobius>
like maybe you could see the addresses in the map file
<siraben>
proteusguy: how long did it take to go through Software Design for Flexibility?
<siraben>
SICP can take ages to go through for instances (in detail and also doing the exercises), I wonder if the new book would be written in a different style
Zarutian_HTC1 has quit [Read error: No route to host]
<proteusguy>
siraben, I perused it in a day (I was aware of most of the concepts - just really interested how he put them together and what he did with them). Now I've gone back and am reading it in more detail. Yes - only on chapter 2 now as I pay close attention to the code.
<siraben>
Yeah makes sense to skim it quickly initially to get the big picture
Zarutian_HTC has joined #forth
mtsd has joined #forth
gravicappa has joined #forth
<KipIngram>
I'm still in the middle of my SICP skim. I slowed down a good bit when I started watching the lectures.
<siraben>
KipIngram: there's neat exercises in the book about solving basic differential equations with streams, which you might like from an EE standpoint
<mark4>
i think you COULD do it if the executable still had debug info on it and you were prepared to parse all that gobbldegook from the forth :)
<KipIngram>
Cool. I just got past the stream lectures, and found all of the discussion over functional vs. imperative in that general bit of stuff to be really interesting.
<KipIngram>
The whole back and forth on the various ways of implementing Cesaro's algorithm with the different perspectives - very nice.
DKordic has joined #forth
andrei-n has joined #forth
vesankellot has joined #forth
vesankellot has left #forth [#forth]
jimt[m] has quit [Quit: Bridge terminating on SIGTERM]
jevinskie[m] has quit [Quit: Bridge terminating on SIGTERM]
siraben has quit [Quit: Bridge terminating on SIGTERM]
jevinskie[m] has joined #forth
mtsd has quit [Quit: Leaving]
siraben has joined #forth
jimt[m] has joined #forth
mtsd has joined #forth
jedb_ has joined #forth
jedb has quit [Ping timeout: 252 seconds]
jedb__ has joined #forth
jedb_ has quit [Ping timeout: 246 seconds]
f-a has joined #forth
<veltas>
siraben: I have not had a ton of time for recreational programming recently but I have been getting into scheme slowly in guile
<veltas>
Was out all last night looking for a friend's cat
<veltas>
Probably stolen
<veltas>
It's interesting so far, not sure what to make of it yet
<veltas>
I try not to pass judgement on languages until I really understand them
<veltas>
What scared and intrigued me a little was seeing all cores running on a program that got stuck!
<KipIngram>
veltas: I think I'm ever so gradually beginning to see some of the usefulness of Lisp/scheme.
<KipIngram>
Not super clearly yet, but something is "teasing at me."
<KipIngram>
What's still got my head going in circles is DKordic's lambda calculus presenttion he linked a few days ago.
<KipIngram>
That still just feels like a game with extremely arbitrary rules to me.
<KipIngram>
And the examples they give seem like they're chosen to be as confusing as possible - sort of like those arithmetic riddles you see online sometimes where they leave out the parentheses and write things in the most obtuse way possible - I think the whole point of those is to make people argue about them.
<KipIngram>
Like they'll give an LC expression where x appears in like three different independent ways.
<KipIngram>
Why would anyone even write something like that????
<KipIngram>
Use different symbols so that it's clear.
<KipIngram>
And there's utterly no consistency. This feature associates left, that feature associates right, nothing is commutative, etc. etc. It feels like the rules were DESIGNED to make it unwieldy and hard to learn.
<KipIngram>
But there must be something to it; DKordic seemed beyond excited over it the other day.
f-a has left #forth [#forth]
<KipIngram>
I think, for example, it would be easier to parse if they just nixed the left and right association rules and just required parentheses to designate that.
<KipIngram>
I can already tell that as I learn to deal with the things I'm probably going to be re-writing all of them I encounter in that way - insert the parentheses so I can SEE the association.
<KipIngram>
I just feel like someone (Church, I guess) got carried away with brevity.
<KipIngram>
And regarding free, bound, and binding variables, I *think* it's the lambda that makes the variable(s) after it bound, but I'm not sure it actually SAID THAT anywhere.
<siraben>
KipIngram: (lambda (x) e), then when x occurs free in e, it is bound by the outer lambda
<KipIngram>
Yes, that's what I'd inferred, more or less. But only within e, right?
<siraben>
KipIngram: hm, I think lambda calculus notation is terse but it's precise also. application associates left so x y z means (x y) z
<siraben>
Right.
<KipIngram>
Oh I'm sure it is (terse).
<siraben>
too many parents would make hard to write I suppose
<siraben>
parens
<KipIngram>
I guess I'm thinking perhaps a little too terse, given how contradictory to most of mathematics some of the rules are.
<siraben>
Could you link to the presentation again?
<siraben>
Yeah it funnily enough breaks with traditional mathematical notation
<KipIngram>
Especiaslly the fact that different associtivity changes the meaning - that just doesn't happen very much in math.
<KipIngram>
A*B*C = (A*B)*C = A*(B*C) etc. But not in LC.
<siraben>
It's because there's no binary operator here, everything is prefix
<siraben>
I mean to say, the only binary operation is really application, which is invisible
<siraben>
a(bc) =/= (ab)c
<KipIngram>
That makes sense - I'm just noting it's not how most of math trains your brain.
<KipIngram>
It's just another version of the same problem some folks have getting comfortable with the lack of commutivity in matrix multiplication.
<siraben>
KipIngram: wow, that seems like a lot for a presentation
<siraben>
I've certainly seem far simpler explanations of the lambda calculus, showing how it can be used to actually compute as well
<KipIngram>
I feel like the presentation could profit from some more examples. But examples that actually show a practical use case, rather than examples chosen to force you to carefully invoke the rules to be sure you get it right.
<KipIngram>
You know, some where I can clearly see what it's telling me.
<siraben>
For me it was when LC really clicked, with all those examples of it actually doing stuff
<KipIngram>
Oh, cool - good. Another one - maybe that one will sink in better. :-)
<KipIngram>
I'm griping over this and I shouldn't be - I'm just used to understanding things fairly well on first reading, and I'm not getting that from the one I linked.
<siraben>
I think it might be because of all the non-LC stuff in the presentation as well!
<siraben>
it looks more appropriate for logicians or mathematicians
<KipIngram>
Oh, I like this one better already.
<KipIngram>
That first bulleted list right at the top already conveys a lot.
<siraben>
Do try the evaluation buttons, it's slow only on the first click when it loads stuff I tihnk
<siraben>
think*
<siraben>
also, numbers are not condemned to be unary in LC, a binary encoding is possible with all the log n bounds, but at that rate you might as well use native integers or bignums
<KipIngram>
What's going on in that first evaluate? Where does the second lambda come from and why are there so many a's?
<siraben>
What's interesting, rather, is that the encoding of natural numbers is enough to do all the usual arithmetic, in theory.
<siraben>
That's the Church encoding of 6
<siraben>
I think it should print out 6 if it detects the Church encoding
<siraben>
λa.λb.a (a (a (a (a (a b))))) can be thought of as, take a function a and apply it to an argument b 6 times
<KipIngram>
I guess they'll avoid presenting, say, 1427 that way.
<siraben>
Hah, certainly.
<siraben>
KipIngram: funny story is that when Church invented that encoding for natural numbers, he had a hard time figuring out how to write the predecessor function and almost gave up on LC, but his grad student (Kleene, I think), had it come to him during a dentist visit
<siraben>
"Kleene allegedly realized how to define the predecessor function (as given in the previous section: Kleene had earlier defined the predecessor function using an encoding of numerals different from those of Church) while at the dentist for the removal of two wisdom teeth"
<siraben>
veltas: that's a good idea, to not judge a language until one really understands them
<siraben>
I struggled with Forth initially but stuck through it to see the other side
<KipIngram>
Forth was an instant love for me, because most of my programming prior to finding it had been on an HP-41CV calculator.
<KipIngram>
At first Forth was just an "RPN language" - that was the drawing card for me.
<KipIngram>
But it didn't take long for me to see its... "further beauty." :-)
<KipIngram>
On the other hand, my first reaction to Lisp, long long ago, was "yuck - way too many parentheses..." :-)
<KipIngram>
But that's probably because Forth had spoiled me on that front.
<KipIngram>
That's the whole beauty of RPN, actually.
<KipIngram>
Of course, Lisp's ability to add two numbers, or three, or 300 is pretty cool.
tech_exorcist has joined #forth
jedb__ is now known as jedb
Zarutian_HTC has quit [Remote host closed the connection]
lonjil has quit [Quit: No Ping reply in 180 seconds.]
dave0 has quit [Quit: dave's not here]
lonjil has joined #forth
user51 has joined #forth
user51 has left #forth [#forth]
<KipIngram>
You know, it's a bit of a shame that Forth doesn't allow nested namespaces like Lisp does. Then I could put all my "helper words" inside the scope of the word they're helping, rather than require a separate mechanism for hiding or otherwise removing helper names. I must say, though, even if the machinery would allow that, I'd really hate having the name of a word "up here" and then the (short) code for the
<KipIngram>
word an the far side of a big slug of helper word definitions. I think my .: / .wipe mechanism is about as simple as it gets, but it is still "something extra" that I have to put in.
<KipIngram>
There's just an elegance to the Lisp approach that we're missing in Forth.
<cess11>
some forths have namespacing, i think factor handles the non-built-in as hashtables but don't remember if it supports modifying and juggling them at runtime
<cess11>
i mainly use forth as a toy or exercise on fairly capable hardware so crude prefixing hasn't become a problem yet
<KipIngram>
Crude prefixing? I don't quite follow.
<cess11>
e.g. : helper-wordname ... ;
<cess11>
if you're implementing your own system it might be interesting to experiment with chaining dictionaries in a list and figure out some way to connect metadata to it
<KipIngram>
Oh, got it. Actual prefixes. :-)
<KipIngram>
I do something like you described already. My dictionary is one continuous range of memory, but within that I have multip linked lists, each associated with a specific vocabulary. At any given time I maintain a higher level linked list, of vocabularies, that specify my search path.
<KipIngram>
This will let me do what I described, but in my previous system I had a way of actually removing the names and links of temporary words completely from the dictionary, leaving only the CFA/PFA pair and the implementtion body after the need for the words ended.
<KipIngram>
This time, on my new implementation, I won't be recovering the RAM the names and links occupy, but I do intend to "unlink" temporary words from their linked list when I'm done with them.
<KipIngram>
That will be a feature of the base system, as is the ability to search the structure I described above. Actual ability to define and manage vocaulary words, though, is something I will add later on.
<KipIngram>
After I am far enough along that I can edit Forth source into disk blocks and use them to extend the system.
<remexre>
siraben: huh, I haven't thought about a topological interpretation like that at all... tbh my knowledge of topology is pretty much limited to what's covered in the chapters of HoTT not about topology, heh
<MrMobius>
one way to solve the problem is to tag pointers as pointers then garbage collect at the end
<MrMobius>
although that adds a good bit of complexity
<siraben>
remexre: at the basic level, topology looks like glorified set theory because the conditions to be a topological space talk only about a family a subsets of a set X being closed under finite intersection and arbitrary union
tech_exorcist has quit [Quit: tech_exorcist]
tech_exorcist has joined #forth
tech_exorcist has quit [Remote host closed the connection]
tech_exorcist has joined #forth
f-a has joined #forth
gravicappa has quit [Ping timeout: 268 seconds]
andrei-n has quit [Quit: Leaving]
mtsd has quit [Quit: Leaving]
f-a has quit [Ping timeout: 252 seconds]
f-a has joined #forth
f-a has quit [Quit: leaving]
tech_exorcist has quit [Ping timeout: 268 seconds]