00:00:00 --- log: started forth/20.09.18 00:08:40 --- quit: proteus-guy (Ping timeout: 272 seconds) 00:55:02 --- join: proteus-guy joined #forth 01:53:12 --- quit: jimt[m] (Quit: killed) 01:53:17 --- quit: Blue_flame (Quit: killed) 01:53:18 --- quit: alexshpilkin (Quit: killed) 01:53:32 --- quit: siraben (Quit: killed) 02:07:50 --- quit: reepca (Read error: Connection reset by peer) 02:15:06 --- join: alexshpilkin joined #forth 02:19:40 --- quit: alexshpilkin (Remote host closed the connection) 02:23:31 --- join: jimt[m] joined #forth 02:32:59 --- join: Blue_flame joined #forth 02:32:59 --- join: siraben joined #forth 02:33:05 --- join: alexshpilkin joined #forth 03:15:13 --- join: mtsd joined #forth 03:19:41 --- quit: DKordic () 03:33:36 --- join: xek joined #forth 04:04:23 --- quit: proteus-guy (Ping timeout: 260 seconds) 04:05:23 --- quit: xek (Ping timeout: 256 seconds) 05:13:24 --- join: proteus-guy joined #forth 05:36:05 --- nick: cmtptr -> cmt-ptr 05:36:10 --- nick: cmt-ptr -> cmt_tpr 05:36:16 --- nick: cmt_tpr -> cmtptr 05:36:32 --- nick: cmtptr -> cmt\ptr 05:36:34 --- nick: cmt\ptr -> cmtptr 05:37:48 --- nick: cmtptr -> cmt|ptr 05:38:00 --- nick: cmt|ptr -> cmtptr 06:15:53 --- join: Zarutian_HTC joined #forth 06:27:08 --- quit: dave0 (Quit: dave's not here) 06:36:47 --- join: xek joined #forth 06:39:42 --- quit: mtsd (Quit: Leaving) 06:47:44 --- quit: Chobbes (Changing host) 06:47:44 --- join: Chobbes joined #forth 06:52:59 --- quit: cantstanya (Remote host closed the connection) 06:55:43 --- join: cantstanya joined #forth 06:59:48 --- quit: Zarutian_HTC (Ping timeout: 265 seconds) 07:09:35 --- quit: xek (Ping timeout: 264 seconds) 07:28:30 --- quit: cantstanya (Remote host closed the connection) 07:30:48 --- join: cantstanya joined #forth 07:35:49 --- join: Zarutian_HTC joined #forth 07:38:52 --- quit: WilhelmVonWeiner (Read error: Connection reset by peer) 07:39:01 --- quit: presiden (Read error: Connection reset by peer) 07:40:47 --- quit: nmz (Ping timeout: 240 seconds) 08:16:30 --- join: xek joined #forth 08:17:31 --- quit: xek (Client Quit) 08:40:20 --- join: WilhelmVonWeiner joined #forth 09:01:26 --- quit: Zarutian_HTC (Ping timeout: 240 seconds) 09:30:18 --- quit: Lord_Nightmare (Quit: ZNC - http://znc.in) 09:32:45 --- join: Lord_Nightmare joined #forth 09:48:50 --- join: WickedShell joined #forth 09:50:55 --- join: Zarutian_HTC joined #forth 10:11:43 --- quit: gravicappa (Ping timeout: 272 seconds) 10:12:55 --- join: gravicappa joined #forth 10:13:11 --- quit: Zarutian_HTC (Quit: Bye) 12:12:28 --- join: reepca joined #forth 12:15:56 --- quit: reepca (Remote host closed the connection) 12:24:40 --- join: reepca joined #forth 12:40:35 --- join: presiden joined #forth 13:11:58 --- join: X-Scale` joined #forth 13:12:34 --- quit: X-Scale (Ping timeout: 256 seconds) 13:12:51 --- nick: X-Scale` -> X-Scale 13:26:09 --- quit: jsoft (Ping timeout: 272 seconds) 14:15:28 --- quit: gravicappa (Ping timeout: 256 seconds) 17:53:21 proteusguy, as it is an L1 board, it won 17:53:26 't work out of the box 17:53:48 however, assuming the L1 is a Cortex-M3 MCU, it could probably be reworked to support it 17:54:13 primarily with changes to the flash controller driver, processor clock setup, and serial driver 18:02:43 --- join: boru` joined #forth 18:02:46 --- quit: boru (Disconnected by services) 18:02:48 --- nick: boru` -> boru 18:03:55 --- join: dave0 joined #forth 18:26:25 --- join: nmz joined #forth 18:50:15 --- quit: WickedShell (Remote host closed the connection) 18:59:45 --- join: boru` joined #forth 18:59:48 --- quit: boru (Disconnected by services) 18:59:50 --- nick: boru` -> boru 19:11:46 --- join: jsoft joined #forth 19:28:19 --- join: iyzsong joined #forth 20:42:24 --- quit: _whitelogger (Remote host closed the connection) 20:45:23 --- join: _whitelogger joined #forth 20:54:50 --- quit: Croran (Ping timeout: 260 seconds) 21:10:03 --- join: Croran joined #forth 21:23:18 --- quit: dave0 (Quit: dave's not here) 21:50:57 --- join: gravicappa joined #forth 22:19:17 --- quit: remexre (Remote host closed the connection) 22:24:49 --- join: remexre joined #forth 22:42:17 tabemann, oh great! Can't wait to get my boards and try it. Was looking at your repo. Moved the license to GPL3 from MIT a while back. Any change of a reconsideration? We don't allow GPL3 in our environments. 22:56:14 remexre: Yay, got a dependent type system (λΠ) working using bidirectional type checking 22:56:53 turns out type checking dependently typed languages requires reducing type to normal form before checking for equality 22:57:46 and checking terms for equality can be more complicated if a named representation is used, if debruijn is used then it's just == 22:58:42 might try adding the equality type, natural numbers then maybe length-indexed vectors 22:59:01 siraben: yeah, there's a {gross,clever} trick where you do different de brujin levels in the envt and indices in terms, too 22:59:15 which iirc is so shifting levels is a no-op 22:59:25 (I just use names though, heh) 22:59:37 i'm using the bound library https://www.schoolofhaskell.com/user/edwardk/bound , which deals with this 22:59:38 it's so nice 23:00:18 succ'ing an entire tree takes O(1) 23:05:08 nice 23:05:44 er, though succ wouldn't be an example where you hit the unfortunate case 23:06:01 it'd be turning x into (fun fresh_var => x) that's expensive 23:06:32 or vice versa, which ofc is happening all the time in beta reduction 23:07:14 ah, so in the bound library this is handled by the `abstract` and `instantiate` functions 23:08:10 ah, okay; haven't had a chance to look through it, building a new server rn 23:09:11 cool 23:10:28 yeah, 24 cores, 288G ram; gonna be a new build box for lab + my forth projects 23:11:02 considering trying to use angr to... "formally verify" isn't the right phrase, with the level of assurance it'd give me 23:11:23 what's angr? 23:11:30 but to give a more-formal-than "it looks right" guarantee that complicated stuff I implement is correct 23:11:39 a symbolic execution engine from... ucsb? 23:11:56 oh, interesting 23:12:09 so I can take an ELF file and ask, "what would the machine state have to be for $bad_thing to happen in $func" 23:12:22 and it uses an absurd amount of ram and maybe finds a thing 23:12:30 does it use abstract interpretation? 23:12:56 maybe one of the analyses does, but the "main thing" is symbolic execution 23:13:14 where you just translate instructions to functions you give to an SMT solver, and it does the heavy lifting 23:13:38 ah, of course 23:15:07 i've thought about assigning a small-step operational semantics to Forth, or has that already been done? 23:15:34 oh, I've seen a paper... lemme see if I can find it 23:15:46 afaik there's exactly one work that models forth well enough for RDROP EXIT to work 23:15:57 er, that's maybe an exaggeration 23:16:09 but stuff that's "not OK in C-land" in general 23:16:30 Looking around there only seems to be small step semantics for expressions or functional languages in terms of stack machines 23:16:35 Right 23:17:47 http://www.complang.tuwien.ac.at/anton/euroforth/ef12/papers/stoddart.pdf gives an axiomatic semantics for Forth 23:18:56 ah neat, I hadn't seen this one before 23:19:27 I can't find the paper on my phone, so I'll send it once I'm at a normal PC 23:20:07 Oh oops it's not axiomatic semantics, the paper says it's "prospective value semantics" 23:21:50 Ok, I'd be curious to see the paper you're referring to 23:59:59 --- log: ended forth/20.09.18