00:00:00 --- log: started forth/20.08.01 00:30:24 --- quit: _whitelogger (Remote host closed the connection) 00:33:24 --- join: _whitelogger joined #forth 00:34:27 --- join: shynoob joined #forth 02:49:54 siraben: tried idris or agda? I like coq for proofs, but can't stand it for program development; idris is a lot more practical than those 03:01:30 --- quit: shynoob (Remote host closed the connection) 03:43:31 --- join: shynoob joined #forth 03:43:58 is the yahoo group for win32forth still active? 03:59:47 --- quit: pareidolia (Ping timeout: 244 seconds) 04:31:57 --- quit: elioat (Quit: The Lounge - https://thelounge.chat) 04:37:07 --- join: elioat joined #forth 04:39:11 remexre: I tried Agda, (plfa.github.io), it seems great but proving isn't as ergonomic as in Coq, and it uses unicode way too much. 04:39:50 I heard good things about Idris, might try it since it's possible the most developed in terms of trying to bring dependent types in a practical way. 04:49:48 s/possible/possibly 04:55:52 yeah, the unicode irks me too 04:57:59 I haven't done PLFA, but I've done a course on type theory in it, and I'm using it for my own research; I actually prefer typed holes to coq's prover, mostly 'cause after about the same amount of experience in coq, I still can't figure out how to phrase certain transformations in the tactic language 04:59:28 (plus, Prop feels "dirty" to me, though I don't like proof irrelevance much as a whole) 05:20:18 ?remexre: I see. I like the holes feature too, yes. What sort of research are you doing 05:20:23 ?* 05:24:08 siraben: kinda same stuff as idris; building a PL with dependent types, trying to make it both human-usable for general programs, while also making it easy to do machine-aided proofs 05:24:48 remexre: What do you make of proof irrelevance. IIRC it's just that two proofs can be considered "equivalent" (in a homotopy type theory sense) if they witness the same proposition, right? 05:24:55 I'm basing it on cubical type theory, unlike idris, though 05:24:56 yeah 05:25:21 Ah, as I understand it cubical type theory lets you do homotopy type theory with computational content (without the equivalence axiom)? 05:25:29 nonconstructive equivalence axiom* 05:25:34 univalence axiom, yeah 05:26:18 Yes. 05:26:43 I saw this talk a few months ago; https://www.youtube.com/watch?v=AZ8wMIar-_c 05:27:33 Interesting that intensional type theory doesn't allow us to prove that ReaderT Maybe isn't a functor, or streams. 05:27:43 or that streams are functors* 05:28:10 When I started trying to do things with Coq, it was very clunky and I never properly learned the more advanced techniques like Setoids. 05:28:16 with streams in Coq* 05:28:35 that's just function extensionality, right? cubical type theory gives you function extensionality, as a provable theorem 05:29:09 Oh, that's amazing. How? 05:30:39 \(f g : A -> B)(p : forall (x : A), f x = g x) -> \(i : Dim)(x : A) -> p x i 05:31:01 You'll have to explain what happens after the second arrow, hm. 05:31:14 er, did the talk cover paths and intervals/dims 05:31:16 What does it mean to produce \(i : Dim)(x : A) -> p x i 05:31:39 Yeah, I think it did, I haven't studied cubical type theory, though. 05:32:00 Do you need to know homotopy theory for HoTT? 05:32:14 I have yet to take an undergraduate course on topology. 05:32:15 not really; I don't know the "actual math" very well, heh 05:32:46 okay, so the values of (A = B), where A and B are of type T, are functions from a Dim (0 to 1 interval) to T 05:33:01 [0,1] as in a real interveal? 05:33:07 such that (for p : A = B), (p 0) evaluates to A, (p 1) evaluates to B 05:33:12 yeah 05:33:26 Ok, so that's the "homotopy" part. 05:33:52 But T is discrete, no? 05:34:03 I guess, homotopy equivalent to [0,1] for all that matters. 05:35:00 yeah, in the implementation you normally just carry around little trees of expressions for the [0, 1] interval; and yeah it's up to homotopy equivalence 05:35:31 So what happens when I do something like p 0.5? 05:35:39 Is it defined there? 05:36:09 yes in a math sense; actual on-a-computer implementations won't let you write 0.5 though 05:36:25 Heh, ok. 05:36:37 What's (i : Dim) then 05:36:43 imThe type D 05:36:44 normally you have 0, 1, max(_, _), min(_, _), and (1 - _) 05:36:49 The type Dim (darn trackpad) 05:37:02 that's the [0, 1] type 05:37:02 I have those for what? 05:37:06 I think Agda writes that as I 05:37:21 er you have those for the Dim type 05:38:06 --- quit: jsoft (Ping timeout: 240 seconds) 05:38:35 Is it alright to think of the [0, 1] interval as a restriction of \mathbb{R}? 05:38:50 It's isomorphic to R 05:39:04 yes, if you keep in mind that because of homotopy equivalence, points other than the endpoints can move around 05:39:22 like there's nothing guaranteeing what's at 0.5 05:39:43 Of course. 05:40:42 Ok, so I have this proposition (p : forall (x : A), f x = g x), then I pass x to it, then I pass the witness i for the interval Dim to complete the proof for extensionality? 05:40:50 yeah 05:41:24 Ah, and it typechecks because (f x = g x) : Dim -> T, and we pass Dim to it, nice. 05:41:38 and since (\(i : Dim)(x : A) -> p x i) 0 = (\x -> (_ : f x = g x) 0) = (\x -> f x) = f 05:41:41 and ditto for g 05:41:49 Wow. 05:42:04 yeah, it's super nice 05:42:50 Ok, why does the talk mention infinite objects such as streams as well, and how cubical types can avoid the problem of custom equivalence relations (and nasty setoid hacks)? 05:43:28 Wait extensionality would solve equality of streams easily, since that becomes equality of functions (in the case that a stream is a function from the natural numbers to values of a type) 05:43:44 yeah 05:43:55 if stream is defined as a datatype, that's probably higher inductive types; basically, you can add extra equalities to the structure of the type 05:44:07 and those are in hott without cubical type theory 05:44:07 Then I can use proof for equality to substitute one stream for another stream, nice. 05:44:11 yeah, what's higher inductive types? 05:44:57 I can specify extra equalities, e.g. 05:45:02 data WeirdList a where 05:45:06 Nil : WeirdList a 05:45:22 ConsLeft : a -> WeirdList a -> WeirdList a 05:45:38 ConsRight : WeirdList a -> a -> WeirdList a 05:46:12 WeirdEq : (ConsLeft x Nil) = (ConsRight Nil x) 05:46:36 How does WeirdEq in this GADT notation? 05:47:15 in a cubical system, it's like you added a constructor WeirdEq : (i : Dim) -> WeirdList a 05:47:33 with the extra rules, WeirdEq 0 = (ConsLeft x Nil), WeirdEq 1 = (ConsRight Nil x) 05:47:44 Oh, I see. 05:47:58 I need to play around with these system to really understand them. What did you use to learn cubical type theory? 05:48:19 I took a class on it, taught in cubical agda 05:48:35 Nice, that certainly helps. 05:48:37 it was last semester so the second half was online (covid); lemme find the lectures, they're on youtube 05:48:48 I don't think I have a class at my university on cubical type theory, heh. 05:49:05 yeah, this was a special one; we've got a class that's just "a prof wanted to teach a thing" 05:49:12 Right, like seminars. 05:49:16 yeah 05:49:33 https://www.youtube.com/watch?v=LWQqE2JcDSQ&list=PL0OBHndHAAZrGQEkOZGyJu7S7KudAJ8M9 05:49:39 There's a category theory one in the fall, but alas I don't have the prerequisites for it. 05:50:22 Nice, I like these visualizations already! 05:50:35 you might be able to convince the prof to let you take it anyway; we de facto don't enforce prereqs 'cause students will just ask the prof anyway 05:51:22 If/when cubical type theory goes more mainstream, imagine all the bad analogies à la what we see with monads right now. 05:51:50 lol, I've just been waiting for little cartoon animals walking along paths 05:52:04 Yeah, or I could sit in, heh. I did that for a logic class last year. 05:53:05 It was classical logic. Very relevant for PL people because logicians also care about syntax, semantics, normalization, equivalence, and so on, just as we do with programs. 05:54:04 remexre: Are you a graduate student? 05:54:53 yeah, I've been meaning to take ours, but the philosophy department sends a lot of their students to it too, so you have to be super-quick to register for it 05:55:26 I will be in the fall; it's at the same institution I did my undergrad at, I took a gap year where I still did classes 05:55:52 so I didn't really stop being a student, I just picked up a job too, heh 05:55:58 Ah, nice. 05:56:37 I think I saw you on #forth some time ago when you mentioned that functions are exponentials in a closed cartesian category, heh. 05:57:15 oh, did you recommend the squiggol book? 05:57:20 I think I remember this too 05:57:58 Yes. I've made some more progress since, actually. It's great. 05:57:58 algebra of programming, that is 05:58:29 nice 05:58:31 I'm up to the last two chapters, took a little break from it and hopefully my professor and I meet regularly again to discuss it. 05:59:31 There's also another book that I came across, a professor in Portugal wrote it initially as notes for people to understand AoP, but it covers more which is nice. 05:59:32 http://www4.di.uminho.pt/~jno/ps/pdbc.pdf 06:00:25 The explanation of F-algebras and catamorphisms is so natural, probably my favorite so far. 06:00:47 I'll add that to my reading group's "books we should read list" too; we're still doing software foundations, just started the second book (will probably switch books at the end of it) 06:01:55 Oh, that's great. 06:02:23 I found the second book quite difficult, might need to revisit it again. 06:02:48 In particular the custom syntax made it unclear how to proceed with a proof, do I unfold the definition, or perform inversion, etc. 06:03:21 yeah, that's something I really hate about coq 06:03:42 at least in lisp, forth, etc.'s custom syntax, I can tell "what's the thing I need to search for to find the definition of this" 06:04:01 Does Agda make this problem any better? They still have mixfix to obscure things. 06:04:09 ^searching Agda is a nightmare sometimes 06:04:26 eh, it's not much better, but I see much less overuse of weird syntax 06:04:33 Right, you know exactly what to search for in lisp and forth. 06:05:09 Haven't used Idris, but it doesn't do any of that unicode stuff right? 06:05:23 I think it might support it, but the standard library is all ascii 06:06:24 That's a relief. 06:08:07 I recently wanted to follow along a linear algebra course I took with Coq, but it rapidly was evident that pen and paper reasoning is faster and easier to check. 06:08:13 Maybe Lean is designed better for the working mathematician? 06:09:22 maybe, I haven't tried it; I kinda suspect formalization is gonna be slower than the "normal" sorts of handwaving one does no matter what 06:10:12 though that's something I want to look at in my language; I'm hoping that the user can "sketch out a proof," and the machine can fill in the gaps 06:11:03 Right. Relatedly I've seen some layman explanations of HoTT and they seem to imply that it will allow mechanized reasoning in a similar way as to how mathematicians draw analogies between fields, how accurate is that claim? 06:11:36 That sounds useful. 06:12:02 ideally I'd like to be able to take notes in formal notation while following along with a lecture in realtime, and in the background, the proving engine tries to work through it; then after, I help it with whatever it got stuck on 06:13:08 it does make reasoning with isomorphic things a lot easier; I'm not sure how much that helps automated proving, though 06:14:08 well, I guess it makes some things only as hard as automated program construction 06:14:15 I have a feeling that Isabelle does this thing quite well. If you look in a book like Concrete Semantics, the proofs are more declarative than their equivalent Coq or Agda proofs. 06:14:41 But also, Isabelle uses a Higher Order Logic, so that may be one reason why they can use such powerful automation. 06:14:51 --- quit: gravicappa (Ping timeout: 256 seconds) 06:15:29 See the proof for irrationality of square root of 2 on https://en.wikipedia.org/wiki/Isabelle_(proof_assistant) , for instance. 06:16:32 huh, that is more readable, though I feel like the "hence"s help a lot 06:17:18 (and agda has those, as the ≡-Reasoning, if I understand what they're doing correctly) 06:17:30 There's the infamous sledgehammer tactic whereby Isabelle calls external theorem provers too. 06:17:34 Right. 06:17:51 Did the Agda parser seem fussy to you, by the way? 06:18:00 It's very sensitive to whitespace. 06:18:06 yeah, like tuples have to be (1 , 2) instead of (1, 2) 06:26:20 < 1 , 2 > even, right? 06:27:25 er yeah for real tuples, I usually use sigmas for everything, heh 06:28:19 Is there a lot of people doing PL research or related topics at your university? 06:28:31 You mentioned the reading group, so that's quite a few. 06:29:05 a dozenish including faculty, I think 06:29:41 er, maybe a few more, definitely less than 20 though 06:30:05 the reading group is usually 5-10 people, depending on the book 06:30:21 Ah, sounds good. 06:32:15 remexre: On a more Forth-related note, you might be interested in slides from a talk I gave recently on an assembler for the EVM. https://github.com/ActorForth/evm-assembler/blob/master/docs/evm-assembler-talk.pdf 06:32:50 that's ethereum vm? neat, will give it a look 06:33:31 Yeah, I've been working with proteusguy on smart contracts on Ethereum and more recently, Bitcoin. 06:34:55 There's been some academic activity on Ethereum smart contracts, their construction, verification, etc. which is nice because of infamous attacks caused by inadequate languages people currently use to write them. 06:35:47 I was interested in how Facebook's Libra would use linear types in their blockchain, but looks like it's stagnant for now because many companies pulled out. 06:36:15 yeah, libra seemed kinda... evil 06:36:34 Come to think of it, a lot of prominent Haskellers are working in the cryptocurrency space. Philip Wadler is working at IOHK on Plutus, which is based on System F omega. 06:36:47 I haven't looked too much into any of the blockchain things other than noting "huh, program validation stuff from $dayjob could be useful" 06:37:46 Yeah. I like the PL aspect of blockchain, not an expert on economics or anything to comment on the viability of it to replace the current financial systems. 06:38:20 Related, heh. https://en.wikipedia.org/wiki/Crypto-anarchism 06:38:56 yeah, I'm somewhat suspicious of cryptoanarchist stuff 06:39:04 Have you heard that GHC merged linear types? 06:39:08 Coming in 8.12. 06:39:22 like yes governments do bad things, but much of existing financial regulation is not evil? 06:39:32 yeah, saw that; haven't had a chance to play with them though 06:39:34 Yeah, so there's that whole debate. 06:40:16 GHC Haskell is a dialect of Haskell at this point, IMO. Almost every useful program I see uses language extensions in one way or another. 06:40:20 I'm not really sure what I'd use them for in haskell, though, since I don't think the optimizer knows about them at all 06:40:30 heh, yeah, I saw a quote recently 06:40:38 "In this talk I'll be using Haskell 98, 06:40:44 i.e. Haskell with 98 language extensions enabled" 06:41:34 Haha 06:41:48 I think the main purpose was for resource-aware computation. Currently there's all sorts of solutions to handle resources, for instance ConT, or resource libraries etc. 06:41:54 ContT* 06:42:31 oh, sure 06:46:19 reading the evm slides now; 24kb is a weird number... 06:47:44 Haha, yeah. The exact number is 24576. 06:48:09 Which is 6000 in base 16 06:49:33 weird they wouldn't go to 32 or 64; do they use the length field for something else when it starts with 0b1110 or something (though that's terrible)? 06:49:36 --- quit: shynoob (Ping timeout: 245 seconds) 06:51:05 Yeah, it's weird. 06:51:30 It's certainly not final. Not sure how I feel about the limitation of 16 call depth. But smart contracts should be fairly constrained. 06:52:05 just wait until someone ports twitch plays pokemon to a smart contract 06:52:09 I wanted to achieve a uniform and relatively cheap calling convention that separates the regular stack from the call stack, so that super efficient code can be written. 06:52:28 yeah, makes sense 06:52:31 Vyper and Solidity are truly messes of languages. 06:53:45 Here's a great example: I wrote a small program that, when compiled, blew up to over 55kb! Then, after two compiler fixes, it went down to 1644 bytes. 06:53:48 https://github.com/vyperlang/vyper/pull/1488 06:54:44 Any reasonable compiler would roll their loops, but Vyper seemingly unrolls them to the max. 06:54:55 huh, is that to avoid having to analyze recursion? 06:55:14 have you seen https://github.com/zetzit/zz ? 06:55:20 C-like lang built for automatic reasoning 06:55:49 Oh, I should say that it's not due to program loops. Rather, they decided to do some sort of procedure for every element in an array. That program has a 1000 length array, so the check is done for every element. 06:55:53 And the check is unrolled 06:56:01 Wow, haven't seen that before. 06:57:10 Yeah, how do languages like that work? They don't implement full-blown deptypes and instead employ solvers to check properties statically. 06:57:15 Symbolic execution? 06:57:54 basically you make a VM, but instead of e.g. u8 memory[65536], you do Expr memory[65536] 06:58:02 where Expr is an SMT expresssion for a u8 value 06:58:28 the as you execute, you're building up bigger and bigger constraints 06:59:10 --- join: pareidolia joined #forth 06:59:17 then you can toss them in an SMT solver, and, if all goes well, it can tell you whether the program can complete or not 06:59:21 The SMT expression constrains the values of the array, yes? 06:59:48 yeah, like memory [0] might equal (if memory[1] > memory[2] then 5 else memory[1]) 07:00:11 Ah, then can the SMT also tell you if the program may not finish in that state? 07:00:29 yeah 07:01:17 That's very cool. Recently, hevm (the haskell implementation of the EVM) added symbolic execution. https://fv.ethereum.org/2020/07/28/symbolic-hevm-release/ 07:01:20 and you can do queries while you're building up constraints (e.g. before you index an array, check "is the index out of bounds?") 07:01:26 Which is big step up for formal methods on the blockchain 07:01:41 ah, nice! 07:01:45 Oh yes, I was reading a paper on bounds checking that used refinement types. 07:01:49 --- join: litvinof joined #forth 07:01:52 Similar idea, I suppose. 07:02:34 Looks like the way hevm did it is relatively lightweight for novice programmers, a simple assertion is all that is needed for symbolic execution to go ahead. 07:03:03 Considering the number sizes are like 2^256, it's impossible to enumerate them in a reasonable amount of time. 07:04:04 yeah, smt solvers are really magical 07:04:30 * siraben hasn't written one yet 07:05:22 me neither, and I don't really wanna; my understanding is that they're (usually) a huge pile of often-gross heuristics, often on top of a sat solver 07:05:32 which then itself is another huge pile of heuristics 07:05:38 There's a little toy implementation I wrote of how HM works in a concatenative language https://github.com/ActorForth/ActorForth/blob/haskell/forth.hs 07:05:44 Yeah, because SAT solving is NP-complete. 07:06:05 DPLL, constraint propagation are popular techniques IIRC 07:07:27 --- join: proteus-guy joined #forth 07:07:38 Even Algorithm J in the Hindley-Milner system can take exponential time for pathological expressions, at least it's not undecidable. 07:10:01 yeah, I'm not looking forward to when I have to do higher-order unification for my language; I've mostly been working on the middle-back-end (after type inference+unification, before codegen) 07:10:38 in your HM, are (:-) argument types? 07:14:40 Basically cons at the type level 07:15:16 Yeah, I seriously want to implement dependent types, checking first then maybe bidirectional type inference 07:16:10 hm, so would a bool-dup have type (T "Bool" :- T "Bool" :- TVar "a") :-> TVar "a" ? 07:16:11 Have you seen Ben Lynn's blog posts? They're a gem. Here's one where he implements type operators; https://crypto.stanford.edu/~blynn/lambda/typo.html 07:16:57 Bool dup would be, T "Bool" :- TVar "a" :-> T "Bool :- T "Bool" :- TVar "a" 07:17:11 er wait yeah I got that really wrong 07:17:14 I should say, x :- y is like 9x,y) 07:17:17 (x,y) 07:17:20 sorry, trying to have like 3 convos at once lol 07:17:34 Haha 07:18:48 You have a repo where you implement a dependently typed Lisp with algebraic effects? 07:19:17 I do bidirectional typing in the typechecker I'm doing now; the fuller unification inference I want would be so I could write e.g. id False or id _ False instead of needing to do id Bool False 07:19:40 Right. 07:20:14 What's the guide to doing bidirectional type inference? 07:20:16 but the bidi inference is not much harder than checking on fully annotated terms; https://davidchristiansen.dk/tutorials/nbe/ is a great reference 07:20:22 I guess I need to look into what bidirectional means in this context in the first place. 07:20:35 http://davidchristiansen.dk/tutorials/implementing-types-hs.pdf for haskell version of same 07:20:43 bidirection is just, you have both 07:20:50 checkType :: Term -> Type -> m () 07:20:52 and 07:20:53 Thanks, looks great. 07:20:56 inferType :: Term -> m Type 07:21:01 and they're mutually recursive 07:21:03 Oh, David Christiansen also wrote the Little Typer IIRC 07:21:21 yep, the last chapter here is a case study w/ a subset of the little typer's lang 07:22:14 for my lang, the algebraic effects are shelved for the moment, I haven't been able to figure out how to do them such that I can do backtracking, but can't do an infinite loop, without adding linear types 07:22:37 Great, the PDF looks very comprehensive. 07:22:49 repo is https://git.sr.ht/~remexre/stahlos though; the exp and src/compiler-bootstrap dirs are the relevant ones for the lang 07:23:17 I've been working on the ocaml branch for the last couple of days; right now, I'm trying to do datatype declarations in such a way that they're not really "wired in" 07:23:34 What do algebraic effects have to do with backtracking and linear types? 07:23:38 but defining the eliminators (like the ind-* things from the little typer) is weird and annoying then 07:23:47 backtracking is an effect I might want to have 07:24:32 and linearly typing the continuation the effect handler is passed makes infinite loops harder (impossible, I think, but not sure) to write 07:25:03 Ah I see. 07:25:07 Logic errors become type errors! 07:25:30 I never thought that linear types could solve the problem of detecting loops in a backtracking effect, wow. 07:26:17 Is the plan to write an OS in this language? 07:26:36 yeah, with everything that can't be written in it written in Forth instead 07:26:50 which is what the src/kernel-aarch64 directory is 07:27:38 right now that's at the point where it can boot on real hardware, allocate memory, run a repl 07:27:44 Fascinating. 07:27:48 but the repl spinloops on the serial port instead of using interrupts 07:29:23 There's also a proof directory on the GitHub repo, have you done much proving in Lean? 07:29:40 basically none 07:30:12 though now that I'm looking through that, there's a lot more there than I remember writing 07:37:40 What would stahl be used for in the OS? 07:37:54 Userspace programs? 07:39:16 so I'm not really having a strong userspace/kernelspace distinction, other than that stahl programs can't do pointery things, the compiler automatically adds preemption points, etc 07:39:30 the answer is "as much as possible," I guess 07:40:04 like even for device drivers, I'm going to try to have Forth run the interrupt handlers, but just set a flag for Stahl code to respond to 07:40:14 (and schedule the relevant driver) 07:43:27 I see. Why make it a dependently typed language with effects/ 07:43:28 ? 07:43:51 dependent types for increased expressivity, and to allow proving the "really important parts" 07:45:26 the effects aren't really baked in at all 07:45:31 and I need some way to do them 07:45:59 and algebraic effects seem like the least bad way 07:46:11 aren't really baked in at all in the current design* 07:46:34 I'm probably gonna reimplement https://hackage.haskell.org/package/fused-effects once I have something typeclass-lookin' 07:49:21 Yeah, effects are great, and it seems like using them to express what a program can and cannot do at the OS level is a novel idea. 07:57:11 --- quit: Zarutian_HTC (Ping timeout: 256 seconds) 08:26:11 --- join: X-Scale` joined #forth 08:27:11 --- quit: X-Scale (Ping timeout: 260 seconds) 08:27:12 --- nick: X-Scale` -> X-Scale 10:09:53 --- quit: proteus-guy (Ping timeout: 260 seconds) 10:22:50 --- join: proteus-guy joined #forth 10:28:10 --- join: WickedShell joined #forth 11:31:10 --- quit: tolja (Ping timeout: 264 seconds) 11:58:27 --- join: tolja joined #forth 11:59:23 --- join: gravicappa joined #forth 12:49:37 --- join: xek joined #forth 13:15:23 --- quit: proteus-guy (Ping timeout: 260 seconds) 13:39:01 --- join: proteus-guy joined #forth 13:43:25 --- quit: proteus-guy (Ping timeout: 256 seconds) 14:05:05 --- join: cox joined #forth 14:08:49 --- quit: cox (Client Quit) 14:36:01 --- quit: xek (Quit: Leaving) 14:52:37 --- quit: gravicappa (Ping timeout: 246 seconds) 15:28:40 --- join: Zarutian_HTC joined #forth 16:03:06 --- join: mark4 joined #forth 16:56:03 --- join: jsoft joined #forth 18:03:03 --- join: boru` joined #forth 18:03:06 --- quit: boru (Disconnected by services) 18:03:08 --- nick: boru` -> boru 18:48:23 --- quit: _whitelogger (Remote host closed the connection) 18:51:23 --- join: _whitelogger joined #forth 19:17:03 --- join: proteus-guy joined #forth 19:30:28 --- quit: proteus-guy (Ping timeout: 260 seconds) 19:43:49 --- join: proteus-guy joined #forth 19:57:53 ok i got a problem :) 19:58:19 im porting x4 to x64 and i have worse in my kernel to store values into an array 19:59:03 []! ( n1 a1 index --- ) stores n1 in array a1 at specified index 19:59:26 n1 is now 64 bits 19:59:52 i also have [w]! and [c]! and of course all the associated @ words 19:59:54 but 20:00:02 what do i call the 32 bit store 20:00:19 i cant call it [d]! because in forth d implies a double 20:00:41 and i cant call it [h] for half word because that implies storing into header space 20:00:43 argh 20:01:21 [s]! for short? 20:01:22 lol 20:01:52 hey guys 20:05:18 h seems to be the default designator for halfwords 20:10:56 --- quit: mark4 (Ping timeout: 240 seconds) 20:10:59 --- join: cox joined #forth 20:11:24 --- nick: cox -> mark4 20:20:37 wb 20:33:08 Welcome back mark4 ! :-) 20:34:43 hey :) 20:34:52 power went out 20:35:24 tabemann, i cant use h becuaes i use h to signify header space 20:35:36 i have allot and hallot and , and h, etc 20:35:56 s makes sense to me. 20:36:00 so i picked s for short which i dont really like 20:36:23 makes sense but i still dont like it, not necessarily intuitive 20:36:37 allot32 20:36:55 I like being explicit. 20:36:55 but i think i need to retire my 32 bit forths and get with the program lol 20:37:02 so porting x4 to x64 20:38:24 anyone here use dropbox? 20:38:30 yeah I do. 20:38:34 is it possible for me to give my sister access to my dropbox? 20:38:43 Yes you can share to an email address. 20:38:51 Can pick specific folders. 20:38:54 she is about to get a cd/dvd for some software i bought 20:39:01 want her to make an ISO and drop it in the box 20:39:19 That should be fine. Will take a while to upload it but it will get there. 20:39:36 she has a fast pipe :) 20:39:46 just bought an updated registration for IDA pro 20:39:50 It's the uplink rating by dropbox. 20:39:58 my old license was SOOOO old i was not even eligable for the discount lol 20:40:17 start upload, go to sleep. text me when done :P 20:42:17 yep that'll work. 20:43:19 --- quit: jsoft (Ping timeout: 256 seconds) 20:49:20 Retro 2020.7 is out. Tarball at http://forthworks.com/retro/r/RETRO12-2020.7.tar.gz . Add .pub or .sig to the URL to get the public key and signature for verification of the archive. 20:49:34 * crc returns to quietly lurking 20:50:32 crc - welcome back! Wow mark & crc all in the same day! :-) 20:51:11 proteus-guy: I always lurk here or watch the logs 20:51:54 just have a lot of days where typing is too painful to write much :( 20:52:10 crc, medical problems? sorry to hear it. 20:53:24 Yes, severe carpal tunnel; it's become worse in the last few years 20:57:39 crc, oh man that's no fun. Where do you reside? 20:58:07 Just outside Philadelphia, Pennsylvania, USA 20:58:58 --- join: jsoft joined #forth 20:59:52 I've read about some stem cell treatments for CPS that sound very promising. 21:00:44 CTS I mean. 21:10:09 back 21:12:14 wb tabemann 21:12:22 howdy 21:12:23 hey guys 21:13:02 that really sucks with the carpal tunnel 21:13:05 proteus-guy: it'll be quite a which before I'll be able to get any treatment for it 21:15:50 crc why is that? 21:17:14 Cost of treatment; my medical insurance has a high up front deductible that I can't afford 21:17:52 Have you ever explored these treatments and seen how much they cost? 21:21:02 high deductables are the thing in the US these days 21:23:44 A couple of years ago, I looked into surgery to correct it. I was given estimates from a couple of surgeons of $7k-$12k per wrist. I'd have hit my out of pocket max deductible at $13500, but I don't have $13k. Additionally, I'd be missing work, which I can't afford to do. 21:25:21 Surgery is so very different and expensive compared to stem cell treatments. 21:27:07 wow you've got a high deductable! 21:27:21 IIRC my deductable is somewhere around ~$4K 21:30:03 --- quit: proteus-guy (Ping timeout: 260 seconds) 21:30:09 Good mornings 21:30:15 Or afternoons or whatevers 21:31:11 My deductible sucks. It's why I seldom seek medical treatment for issues. (E.g., I'm diabetic. I switched to using less effective generic insulins a few years ago because it was too costly to get the better ones, even with insurance.) 21:33:56 hey jsoft 21:34:08 Hi jsoft 21:34:29 this is why we need socialized medicine 21:34:40 agreed 21:35:04 crc why is typing painful? 21:35:19 oooh ouch! 21:35:53 mark4: I have severe carpal tunnel, which has been worsening over the last three years 21:36:33 and... now I've implemented >NAME 21:37:21 crc i do constultant work at %50+ an hour and if i am working more than 50 miles from home i get per-diem which means that about half of that is NOT taxable (not just not taxed, not taxable) 21:38:03 i can put you in contact with my agency and if you do this work you would be taking home 2k+ a week 21:38:18 I made changes to improve ergonomics in my workspaces, using keyboard layouts to reduce typing and finger movement based on heatmaps of my code and writings, and now work on an editor for the same purpose 21:38:34 and maybe the medical benefits have better deducables i dont know i did not get medical 21:39:48 would you have problems moving around the country working contracts? 21:40:31 Yes. I have a wife and kids; relocating would be difficult for them 21:40:39 not relocating 21:40:45 your home would stay there :) 21:40:59 but you might go work for 6 months in east podunk idaho 21:41:11 even that is likely a bit much 21:41:31 not if it gets yoou what you need to fix your issues 21:41:45 As to travel, I don't drive, which complicates that a bit 21:42:01 there are likely jobs with better benefits locally 21:42:05 this time last year i had almost nothing in my bank account. if i lost my job today i could survive for maybe 3 years with what i have now 21:42:17 dont drive? 21:42:27 that might be a problem :) 21:42:28 no license 21:42:34 aha 21:42:42 --- join: proteus-guy joined #forth 21:42:46 wb 21:42:53 well i drive my car and i have no plates, no inspection sticker, no title... . . 21:42:58 but i do have insurance 21:43:25 umm how haven't you been pulled over yet? 21:43:34 We have a van, my wife uses it 21:43:52 i was working in austin texas for 6 months driving to and from work and cops ignored me 21:44:23 i drove from tx to nc when that was done and i was pulled over in i forget which state for doing 55 in a 35 and got a warning. 21:44:27 no plates lol 21:44:40 if i get pulled over i have a defense 21:44:54 I can walk or bike to anywhere I need to go (though biking isn't happening right now due to my right hand being particularly bad in the last month) 21:45:36 williams v. fears. shapiro v. thompson. thompson v. smith. dickey v. davis (landmark). crandal v. nevada. people v. nothause. UNITED STATES V. GUEST!!!! and thats just off the top of my head 21:45:55 Or take public transit; there's a bus stop literally in front of my home, and a train station three houses away 21:46:33 not sure i would want to take public transport in Philly without a gun on my hip lol 21:47:04 As noted, I'm just outside philly, and not near the violent parts :) 21:47:12 to me my sticker costs like $78 21:47:17 which is nothing 21:47:29 whereas a ticket is likely going to be a couple hundred 21:48:13 i get pulled over and im filing a non divisible action against the cop, the d.a, the judge and the state. 21:48:37 WHEN i win, what ever the jury awards me each and every individual defemdamt owes me that much 21:48:54 then i ask for a preservation of assets order against them all 21:49:02 including the state 21:49:15 that's quite a bit of a headache when a sticker costs pretty little though 21:49:58 not if it gets me $50k per day for the entire time im either physically or constructively imprisoned (PER DEFENDANT!!!) 21:50:18 and i would consider myself constructively imprisoned for the entire time from the date of the arrest to the jury award 21:50:34 and i cannot be non suited. no mere bar corporation shill can dismiss my case 21:50:57 well -- if i was DUMB enough to hire some other bar corporation shill then the judge can dismiss 21:51:07 you're probably going to get a citation, not be imprisoned 21:51:31 no ill be going to jail because when the cop pulls me over im not answering any qyestions or giving any documentation or performing any tests 21:51:34 go get your super 21:51:58 and when he arrests me i DEMAND to be taken immediately befor a magistrate. if he does not tahts a violation of due process 21:52:21 question 21:52:27 do you have a law degree 21:52:29 texas actually has a statute that requires a cop to take you IMMEDIATELY before a magistrate on demand or he can lose his job 21:52:38 dont need a degree in law to know law 21:53:24 actually chapter 543 says if the officer does not take you immediate before a magistrate when you demand it he IS subject to removal from office 21:53:29 not MIGHT BE subject 21:53:58 also do not need a law degree to know that i have an inalienable right to the FREE use of the roads which I OWN 21:54:09 its established law that the People own the roads 21:55:06 that's a lot of trouble to go through just to not get a license plate and a sticker 21:55:36 accompanying this need of the federal government (meaning the need to have it) the court (meaning SCOTUS) recognized a co-relative right (NOT privilege) of the people to move uninhibited throughout the land... 21:56:05 meaning uninhibited by code, rule, regulation, ordinance, statute, prcedure, executive order or jack booted gestapo thugery 21:56:33 i might be a PITA but i only have to go through it once because once i have won that case i have CASE LAW on my side 21:56:54 cop pulls me over. i hand him a copy of the courts ruling and warn him. dont fuck up or i bankrupt you 21:57:18 i was pulled over in texas once and refused to ID. i was charged with failure to ID 21:57:33 guy in front of me goes up to the judge and gets a year and a half in jail for failure to ID 21:57:53 i go up to the judge and challenge her jurisdiction based on certain case law and the constitution and... case dismissed 21:58:09 --- quit: WickedShell (Remote host closed the connection) 22:03:59 its not a get rich quick scheme, its not a means of saving me the cost of the plates 22:04:08 if you do not exercise a right you lose it 22:04:30 EVERYONE is convinced you are required to get plates, get a license, register your care... 22:04:47 that bullshit, the government has no jurisdiction over the land 22:04:49 NONE 22:05:27 thse roads belong to the people. article 2, section 3 of the constitution says i have a right to acquire posessions, that implies a right to make use of posessions 22:05:48 my car is a posession. how can you charge me a fee to use my car on my road 22:05:59 thats like charging me a parking fee to park in my driveway 22:06:14 now... commercial use of the highways is NOT a right 22:06:20 that they can tax, that they can regulate 22:08:31 erm actually not that article of the constitution lol 22:08:49 1:3? now i have to go remind myself lol 22:14:11 --- join: gravicappa joined #forth 22:15:27 --- quit: proteus-guy (Ping timeout: 256 seconds) 23:59:59 --- log: ended forth/20.08.01