00:00:00 --- log: started forth/21.04.29 00:02:53 --- join: gravicappa joined #forth 00:38:24 How do I add Content to Amazon Web S***r!? Do I need iOS or can it be done with Android!? 02:25:21 --- quit: spoofer_ (Read error: Connection reset by peer) 02:25:36 --- join: spoofer joined #forth 04:00:25 --- quit: jedb (Quit: Leaving) 04:00:52 --- join: jedb joined #forth 04:53:31 --- join: pointfree joined #forth 05:03:21 Q: Combinators?! How to most convenniently construct and apply Combinators?! W/Funarg_problem ?! 05:03:21 Combinators are at the essence of both Lisp, >>apply<<, and Forth, >>compose<<. Or even better let Us call it <> rather thann >. 05:03:21 An example of my solution (so far): >> [ dfn ( apply M A ) ( M A ) ( Forth M1 M2 A ) ( M2 ( M1 A ) ) ] <<. 05:03:21 Challenge: >> [ dfn ( fix M ) ( M ( fix M ) ) ] << or the Turing's Construction >> [ dfn fix ( A A ) ( A T M ) ( M ( T T M ) ) ] < KipIngram: What do You think? 05:08:04 --- join: tech_exorcist joined #forth 05:38:34 --- quit: dave0 (Quit: dave's not here) 05:46:59 remexre: yay, was able to prove a compiler to a stack machine correct wrt. a small-step operational semantics 05:47:02 since the programs always terminate, I didn't use bisimulation or anything 05:47:26 `forall (e : aexp) (st : state) (s : stack) (p : prog), stack_multistep st (s_compile e ++ p, s) (p, aeval st e :: s).` 05:47:55 where stack_multistep is the reflexive transitive closure of the small-step rules of the stack machine 05:48:50 later on I'll try a compiler for IMP to a stack machine with jumps, that should be sufficiently complex 06:16:15 --- join: f-a joined #forth 06:36:14 --- quit: f-a (Ping timeout: 240 seconds) 06:38:14 --- join: f-a joined #forth 06:59:19 --- quit: f-a (Read error: Connection reset by peer) 07:03:26 --- join: f-a joined #forth 07:22:28 --- quit: f-a (Ping timeout: 240 seconds) 07:24:32 --- join: f-a joined #forth 07:58:31 siraben: is that from PLF? I remember Adam Chlipala's book had something similar at the start too (though that one ramps up hard + fast iirc...) 08:10:21 --- nick: xek_ -> xek 08:46:56 --- quit: f-a (Quit: leaving) 08:52:47 --- quit: pointfree (Quit: Connection closed for inactivity) 08:54:35 DKordic - I'm afraid I don't immediately follow all that yet. 09:10:17 --- join: f-a joined #forth 09:24:51 --- join: f-a_ joined #forth 09:25:30 --- quit: f-a (Read error: Connection reset by peer) 09:25:35 --- quit: f-a_ (Client Quit) 09:25:54 --- join: f-a joined #forth 10:12:51 --- quit: f-a (Ping timeout: 265 seconds) 10:19:39 remexre: yeah from PLF 10:19:59 Chlipala's book goes really fast, one already needs to be a competent user before reading it for sure 10:21:15 yeah, it was actually my first coq book... picked it up at MIT bookstore when on vacation to boston because the idea of formally verifying programs sounded neat 10:21:30 then got immediately lost and didn't come back to it for years, lol 10:35:30 --- join: f-a joined #forth 10:46:12 https://www.sciencenews.org/article/antimatter-stars-antistars-milky-way-galaxy-space-astronomy?utm_source=Nature+Briefing&utm_campaign=241bf5e18c-briefing-dy-20210429&utm_medium=email&utm_term=0_c9dfd39373-241bf5e18c-44313705 10:48:28 So, formally verifying code IS neat. But whatever we humans do when we look at, for instance, a Forth definition, is also neat. We somehow hold it in our minds, and "see" its correctness. We're human, so that is an imperfect process. We can err. But it's still fascinating that our minds can do that. What exactly do you suppose it is we're doing? 10:49:35 Related - the mere fact that we believe in the correctness of Gödel's Theorem means that we can somehow perceive truth even where it can't be proven. 10:50:09 What exactly are we perceiving? It just smacks to me of an indication that something non-algorithmic is happening in our minds. 10:51:14 I mean, if you want to think in a very pure way, then PROVING truth should be the only way to DEFINE truth. But it's not - we can transcend that somehow. 10:51:18 It's fascinating. 10:51:36 but it is not, isn’t it? 10:51:51 Didn't follow - not what? 10:51:57 first because there has to be some premise X to prove Y 10:52:11 Yeah - a system of logic has to have a starting point. 10:52:35 Oh gosh - what is that book. Early 20th century... 10:52:41 Hang on - I have it here on the coffee table. 10:52:57 don’t spill! 10:53:16 Science and Hypothesis, by Poincare. 10:53:27 He contends that everything is a tautology. 10:53:43 That the conclusions of a logical analysis are really just a restatement of the postulates. 10:53:50 And that's hard to argue with. 10:54:08 I.e., the postulates contain all the knowledge to start with. 10:54:20 So we never add any new knowledge - not REALLY. 10:54:54 ohhh poincaré 10:55:18 I mostly read him about interpretations of Probability 10:55:25 welp, my grammar is degrading 10:55:27 One could argue that all of the knowledge, and all of its practical application, is there in the postulates, but aspects of it are not easy to reach. By logic we bring more facets of it into reach. 10:55:37 But it's all "out there" from the jump 10:56:20 heh, that type of nonsense someone wrote to get a diessertation is why I ran screaming from philosophy 10:56:33 Indeed, indeed. 10:56:52 Scientific philosophy is ok in my book, but there are just times to set it aside, that's for sure. 10:57:06 "Shut up and calculate" has value as well. 10:57:07 I read a book once where the guy said the only way to know truth is to test hypotheses but testing hypotheses reveals other hypotheses you couldn't have known about. Therefore, the pursuit of truth actually drives you farther away from it 10:57:28 obviously horseshit but that doesn't stop people from stringing together similar statements that happen to be grammatically correct 10:58:10 was it fayerabend? 10:58:14 he had a point 10:58:16 Well, let's put it this way. In the 1700's we couldn't build computers. In the 2000's we can. Obviously something has been accomplished. 10:58:33 The same with cars, and microwaves, and cell phones. 10:58:48 The pragmatic evidence of the value of scientific reasoning is all around us. 10:58:51 now then 10:58:52 i check out when the words people put together stop having anything to do with reality. you are then wasting my time at that point. once philosophy hits that point we're just inventing things that can be said without regard for reality 10:58:57 for the real tought questin 10:59:08 why is youtube/reddit harassing me with liquid meal replacement? 10:59:11 I do not want them 10:59:30 MrMobius: some kind of speculative analysis can be for good 10:59:35 lmao... 10:59:40 You did SOMETHING to cause that. 10:59:47 Who knows what, though... 10:59:47 yeah that is the scary part 11:00:22 f-a, but this is not speculation. making claims about reality because you put words together in some way that no longer resembles anything real then leaving fantasy land to inflict your construction on everyone is not speculation 11:00:45 no problem with speculating as long as you remain humble 11:00:49 haha 11:03:02 --- join: Zarutian_HTC joined #forth 11:05:11 I engage in that kind of thinking from time to time. Mostly involving quantum stuff. 11:05:40 Most of the pop-sci coverage of quantum theory is New Age woo. 11:05:53 They deliberately cultivate a sense of mysticism around the stuff. 11:07:11 There's certainly some weird shit going on in there, but it's not as weird as they make it sound. 11:07:38 haha, ya there is 11:07:53 I think the "weird" is mostly related to the fact that two separate points in space can be "connected" in a way that breaks our sense of "distance" and "separation." 11:07:58 quantum entanglement and we don't understand, therefore out souls are connect - believe my religion 11:08:16 *our souls are connected 11:08:38 Our intuition tells us that if A and B are at different places, then the only way for them to affect one another is for an effect to be conveyed over space. 11:08:57 But that's just not true - A and B can be in different places and yet behave (in some ways) as though they're right by one another. 11:09:04 That's weird. 11:09:23 But if you just accept that somehow our concept of spacetime misses something, then there isn't any "more weird" after that. 11:09:53 And yeah - minds, souls, whatever you want to call them. How does THAT work??? We have no idea. 11:10:06 I do NOT believe that our minds are just programs running on our brains. There's something more to it than that. 11:10:33 I don't think science is even close to being able to talk about it, though. 11:11:26 welcome to the realm of philosophy :D 11:11:38 Obviously there is a strong correlation between our thinking / feeling and activity in our brains. I just don't think the one IS the other, with nothing else involved. 11:11:54 a world where we all know that there is never going to be a single correct answer but we try and figure it out anyway 11:12:04 ^^ Indeed. 11:12:55 Anyway, back to earlier discussion. DKordic - the thing you asked me my opinion of. Were you specifically asking me about the code-like stuff you'd just written? That you described as your latest thinking? 11:13:09 Was that somehow an implemetation of a Forth-like thingie? 11:13:53 God, I sound like my sister-in-law. "Thingie." :-| 11:14:54 --- part: f-a left #forth 11:32:30 cray cray 12:02:58 --- quit: Zarutian_HTC (Remote host closed the connection) 12:16:23 That also sounds like my sister-in-law. :-) 12:16:57 I have fun at her expense, but she hasn't turned out to be nearly as flaky as I thought she might when I first met her. 12:17:16 Actually has a very responsible job with Southwest Airlines and everything - the kid's done good. 12:37:27 --- quit: andrei-n (Quit: Leaving) 13:00:34 --- quit: gravicappa (Ping timeout: 265 seconds) 13:52:41 --- join: dave0 joined #forth 13:52:51 maw 14:05:23 --- quit: tech_exorcist (Ping timeout: 268 seconds) 14:12:07 Howdy. 14:14:11 hey KipIngram 14:41:40 --- quit: jedb (Quit: Leaving) 15:49:57 --- join: f-a joined #forth 15:55:52 --- join: pbaille joined #forth 16:01:18 --- quit: pbaille (Ping timeout: 252 seconds) 17:32:32 --- quit: f-a (Quit: leaving) 18:55:34 --- join: boru` joined #forth 18:55:37 --- quit: boru (Disconnected by services) 18:55:39 --- nick: boru` -> boru 19:38:51 --- quit: sts-q (Ping timeout: 246 seconds) 19:53:11 --- join: sts-q joined #forth 21:11:41 --- join: gravicappa joined #forth 21:43:09 --- join: andrei-n joined #forth 21:47:43 --- join: pbaille joined #forth 22:12:33 --- quit: pbaille (Ping timeout: 268 seconds) 23:44:09 --- join: pbaille joined #forth 23:59:59 --- log: ended forth/21.04.29