00:00:00 --- log: started forth/21.04.26 00:08:25 --- join: dave69 joined #forth 00:08:42 never heard about proof assistants implemented in forth, is there one with public source? 00:08:44 --- quit: dave0 (Disconnected by services) 00:09:43 --- nick: dave69 -> dave0 00:15:07 I'd imagine you could implement something like Abella in Forth "without an extraordinary amount of work" 00:15:41 but it's not really "native ground," so to speak; you're usually doing a bunch of term manipulation, which imo works best with a GC, 00:15:49 s/,$// 00:26:21 remexre: I've wanted to formally verify compilation to a stack machine for a while, should be a fun exercise 00:26:31 for expressions it's easy, with control constructs it's a bit harder 00:27:35 yeah, ditto; I've been meaning to try and write up a semantics for my forth, prove my implementation correct against the ARM ASL spec, then start proving things about programs 00:27:44 don't know if I should add a return stack as well heh, that does make things even harder 00:28:00 I think that if I "dip down to" the machine level, it should make control constructs (and hardware interactions!) much easier 00:28:11 oh great, what about a virtual machine? 00:28:20 or yeah you could again relate the VM against ARM 00:28:29 and compose the proofs 00:28:34 yeah 00:29:01 Yes, I see that Peano arithmetic supports a simple logical principle. I guess I'm just willing to accept arithmetic as "obviously correct." Maybe that's just a difference between an engineering field and a theoretical field - when going for an engineering knowledge you don't necessarily feel compeled to prove things from the *very* ground floor. You choose a "pragmatic starting point." 00:29:20 But I see that that's not appropriate for full mathematical rigor. 00:29:24 remexre: if you undertake the project let me know, i would want to contribute proofs and such as well 00:29:41 KipIngram: correct, for embedded I guess the hardware is taken as trusted according to the spec 00:30:01 and they do indeed use formal methods to check correctness of chips! (at least intel and AMD do) 00:31:07 remexre: I think for verifying assembly code they use Z mod 2^32 for arithmetic right? 00:32:48 siraben: Your Forth has no return stack? Or do you just mean that it's not user accessible? 00:33:26 KipIngram: oh I was talking about when I will specify and formally verify a language that compiles to a stack VM, it will have while loops, assignment, arithmetic expressions, but no procedures 00:33:30 siraben: yeah, it'll probably be my PhD thesis once I actually get around to it, lol 00:33:43 KipIngram: in my Forth I have the whole shebang, return stack and all 00:34:01 I think the SAIL people do Z mod 2^n, yeah 00:34:06 :-) 00:34:24 remexre: that'll be cool, a PhD made by a formally verified Forth! 00:34:30 I kind of feel like having the return stack exposed is more or less required to claim the name "Forth." 00:34:45 Forth makes it ideal in some ways, I know the compcert (formally verified C compiler) folks had such trouble with the C spec being imprecise and undefined 00:38:08 yeah, and being able to tweak the semantics if it makes verification easier helps a lot too :) 00:39:42 I'm sorta expecting it to be a pain that I have a max stack size, though hopefully I can write some ltac to just automate that? (if I'm using Coq that is; I'm considering Abella since I probably don't need too many metalogicy things?) 00:40:17 yeah I wonder what to do with max stack size 00:40:59 i'll let it be infinite first then maybe prove that "if the program uses at most N items on the stack, a stack size of N will allow it to terminate" 00:41:30 similar to how "if the program has enough gas, it will terminate with correct result" as in the IMP chapter in logical foundations 00:42:32 remexre: another minor difficulty is microcontrollers have finite memory, so you might want to do address arithmetic modulo the size 00:43:15 well, I've got virtual memory anyway, since I run at EL1 00:43:25 EL1? 00:43:40 ring0 in x86 terms? 00:43:48 ah I see, I wasn't familiar 00:44:24 yeah, arm does EL0 = userspace, EL1 = kernel, EL2 = hypervisor, EL3 = secure firmware thingy 00:45:12 this is cool as well: https://iron.ouroborus.net/ 00:46:08 supposed to bridge the Software Foundations material and current research 00:46:15 oh nice 00:46:23 tho minor oof at trac :P 00:46:32 Oh what about trac? heh 00:47:27 I've mostly used it for SVN repos, and now have a really negative association with it as a result... 00:47:35 tbh its issue tracking is fine / better than GH tho 01:25:08 --- quit: ovf (Read error: Connection reset by peer) 01:25:14 --- quit: Guest45273 (Read error: Connection reset by peer) 01:31:16 --- join: Guest45273 joined #forth 01:31:25 --- join: ovf joined #forth 02:25:58 --- quit: dave0 (Quit: dave's not here) 04:20:56 --- quit: sts-q (Ping timeout: 252 seconds) 04:32:01 --- join: sts-q joined #forth 05:42:00 --- join: tech_exorcist joined #forth 06:01:16 --- join: f-a joined #forth 06:09:43 --- quit: f-a (Read error: Connection reset by peer) 06:14:06 --- join: f-a joined #forth 06:21:19 --- quit: f-a (Quit: leaving) 06:30:42 --- quit: andrei-n (Ping timeout: 252 seconds) 07:15:57 --- join: andrei-n joined #forth 08:16:30 --- join: f-a joined #forth 08:33:00 --- quit: Guest45273 () 08:33:50 --- join: Guest45273 joined #forth 08:34:33 --- quit: Zarutian_HTC (Ping timeout: 240 seconds) 08:34:42 --- quit: Guest45273 (Client Quit) 08:35:12 --- join: rann joined #forth 08:48:15 --- join: Zarutian_HTC joined #forth 09:19:22 --- mode: ChanServ set +v mark4 09:21:14 --- quit: Zarutian_HTC (Ping timeout: 240 seconds) 09:22:10 --- quit: f-a (Quit: leaving) 10:02:37 --- quit: gravicappa (Read error: Connection reset by peer) 10:07:38 --- join: gravicappa joined #forth 10:26:07 --- join: f-a joined #forth 10:33:25 --- join: Zarutian_HTC joined #forth 10:40:22 --- quit: Zarutian_HTC (Ping timeout: 265 seconds) 10:50:55 --- join: Zarutian_HTC joined #forth 11:22:34 --- quit: gravicappa (Ping timeout: 240 seconds) 11:59:48 siraben: I don't see anything at https://iron.ouroborus.net/ . 12:05:29 DKordic: try http://iron.ouroborus.net/ 12:07:12 --- join: gravicappa joined #forth 12:08:03 I think it's a great project, there needs to be more intermediate-advanced material like it 12:16:34 --- quit: f-a (Read error: Connection reset by peer) 12:20:46 --- join: f-a joined #forth 12:21:54 --- quit: gravicappa (Ping timeout: 240 seconds) 12:23:11 siraben: That worked. Thank You. 12:34:48 --- quit: f-a (Ping timeout: 240 seconds) 12:36:46 --- join: f-a joined #forth 13:05:14 --- quit: andrei-n (Quit: Leaving) 13:46:00 remexre: What software are you running that has those rings? 13:46:36 --- quit: mtsd (Ping timeout: 245 seconds) 13:54:33 my forth runs at EL1, since I'm writing an OS in it 13:55:28 Oh, that's nice. So you're writing all the device drivers and so on yourself? 13:56:26 yep 13:56:42 That's fantastic - what machine does it run on? 13:56:45 though, good odds I won't be supporting anything other than virtio and a basic serial driver for a while 13:57:00 right now just qemu, though with some tweaking I can boot it on the rk3399 13:57:25 Where did you find documentation on all the boot-up details? 13:57:49 Decades ago I could all of that in bookstores, but I don't know where to find it now. 13:57:59 partly the arm manual, partly experimentation, partly the sources of {u-boot,qemu,linux} 13:58:02 There used to be a LOT of nice "low-level" books. 13:58:39 I'm very impressed. That's the kind of thing I'd love to do someday but just have never found the time. 13:58:56 Multi-core? 13:59:41 nope, though I'm going for an IPC-heavy microkernel design, so it shouldn't be "that hard" -- I'd just designate a special area for cross-cpu IPC, and run one copy of the kernel per core 14:03:01 Definitely update us now and again - I look really forward to watching you bring that up. :-) 14:03:44 I eventually want to push my Forth to bare metal, but for now it uses a handful of MacOS syscalls to interact with the hardware. I emulate disk blocks in a big "blocks.dat" file. 14:04:27 So I'm working on "everything else," and then someday I'll have a clean, well-defined (and small) set of words that I'll need to re-write to deal with actual hardware. 14:04:38 oh, nice; yeah, I'm probably emulating blocks too, but probably only supporting nvme at first (allegedly it's really simple?) 14:06:19 You know, I should know that, because our SSDs present NVMe to the host. I think I've got a copy of the spec around somewhere - do you have that? 14:07:32 https://wiki.osdev.org/NVMe has links + info 14:12:32 Ah, here's my link: 14:12:34 https://nvmexpress.org/wp-content/uploads/NVM-Express-1_4-2019.06.10-Ratified.pdf 14:13:22 Anyway, I'm very very excited about your project - I'm sure I can learn some good stuff from you over time. 14:14:21 hopefully I can teach you useful stuff then lol; I'm not really a super-expert on this stuff either though 14:14:58 Well, maybe we can figure some of it out together. Just the fact that you're doing this encourages me to perhaps give it a go. 14:21:37 --- quit: tech_exorcist (Quit: tech_exorcist) 14:22:32 --- join: tech_exorcist joined #forth 14:35:17 --- quit: tech_exorcist (Ping timeout: 252 seconds) 14:35:28 I have two major goals for mine "on the other end." I'm adding an extra formal layer to the system - I'm implementing the primitives using a set of macros that I call "portable instructions." I haven't done it perfectly yet; a few times I've been chasing a bug and just wanted to get the code in. But I'll go back and fix that at some point. The idea is that the only thing I should have to port to move the 14:35:30 system to ARM is those macros. So that's one goal. The other is to eventually migrate all of the source into the system itself and have it able to rebuild itself. 14:36:59 Part of the reason I wanted that portable instruction layer is that I tend to write very primitive-heavy systems. I want the best possible performance, so I do a lot more as primitives than I absolutely have to. So I just don't want that to be the porting layer. 14:36:59 --- quit: Zarutian_HTC (Read error: Connection reset by peer) 14:37:05 --- join: Zarutian_HTC joined #forth 14:37:40 The idea behind the macro layer is that it generates more or less optimal primitives, at least on x64 and ARM. 14:37:47 I haven't even started an ARM version yet. 14:43:56 --- quit: jedb (Quit: Leaving) 14:44:32 --- join: jedb joined #forth 14:45:55 --- quit: jess () 15:06:27 --- join: dave0 joined #forth 15:06:51 maw 15:14:01 --- quit: f-a (Quit: leaving) 16:15:09 --- nick: crest_ -> crest 16:19:03 --- quit: DKordic (Ping timeout: 240 seconds) 16:37:02 --- quit: dave0 (Quit: dave's not here) 16:48:00 not forth, but made in forth: http://www.call-with-current-continuation.org/strand/strand.html 17:23:23 --- quit: rixard (Read error: Connection reset by peer) 17:28:00 --- join: rixard joined #forth 17:40:40 --- quit: Keshl (Read error: Connection reset by peer) 17:40:58 --- join: Keshl joined #forth 17:46:40 Oh, nice. 18:39:23 --- quit: Zarutian_HTC (Read error: Connection reset by peer) 18:39:40 --- join: Zarutian_HTC joined #forth 18:58:47 --- join: boru` joined #forth 18:58:50 --- quit: boru (Disconnected by services) 18:58:52 --- nick: boru` -> boru 19:12:47 --- quit: jedb (Quit: Leaving) 19:13:07 --- join: jedb joined #forth 19:42:54 --- quit: sts-q (Ping timeout: 240 seconds) 19:50:42 --- join: sts-q joined #forth 20:09:11 --- quit: MrMobius (Read error: Connection reset by peer) 20:10:23 --- join: MrMobius joined #forth 20:10:35 --- join: gravicappa joined #forth 20:18:29 --- quit: Zarutian_HTC (Ping timeout: 252 seconds) 20:21:57 --- join: dave0 joined #forth 20:33:38 --- quit: dave0 (Quit: dave's not here) 20:36:45 --- join: Zarutian_HTC joined #forth 20:39:33 --- quit: jedb (Ping timeout: 240 seconds) 20:56:06 --- join: jedb joined #forth 21:01:10 --- join: mtsd joined #forth 21:42:49 --- quit: jn__ (Ping timeout: 250 seconds) 21:58:02 is there a really detailed guide-book on how to implement your own Forth? 21:58:57 I've got the programmer's handbook which I suppose might be enough, but it doesn't really explain the best order to approach implementing things 22:04:23 moving forth is the classic reference, if you haven't seen that 22:04:41 though I think most of its performance advice is pretty out-of-date, if you care about branch prediction 22:27:29 looks ancient, but at least the paperback is cheap 22:28:08 jonesforth has a lot of detailed comments in its source, it's based on x86 assembly 22:28:12 https://github.com/nornagon/jonesforth 22:33:32 okay, thanks 22:43:08 --- quit: gravicappa (Ping timeout: 260 seconds) 23:09:32 i was pondering coding my own AVR forth 23:10:31 i really like FlashForth but unfortunately it depends on a proprietary compiler which goes against my ideals 23:14:05 I think in theory it could be built with avr-gcc but I haven't been able to figure out how yet. 23:15:27 up until recently it could only be assembled with the avrstudio assembler. The author recently rewrote it for microchip's XC8 compiler 23:15:56 which I guess is a little better because XC8 is uses avr-gcc for some of the backend stuff 23:16:38 i thought I would try amforth instead but amforth is also dependent on avrstudio assembler 23:17:01 --- join: andrei-n joined #forth 23:17:56 which leaves only AVR-forth, which can be built through the Arduino IDE, but hasn't been maintained for 7 years, and is missing a few nice features - like the ability to compile words 23:18:42 * lispmacs curtails rant 23:23:34 --- quit: rpcope (Ping timeout: 240 seconds) 23:29:13 --- join: rpcope joined #forth 23:31:34 --- quit: hosewiejacke (Remote host closed the connection) 23:32:55 --- join: hosewiejacke joined #forth 23:59:59 --- log: ended forth/21.04.26