00:53 <tabemann> proteusguy, as it is an L1 board, it won

00:53 <tabemann> 't work out of the box

00:53 <tabemann> however, assuming the L1 is a Cortex-M3 MCU, it could probably be reworked to support it

00:53 <tabemann> primarily with changes to the flash controller driver, processor clock setup, and serial driver

05:41 <proteusguy> 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.

05:55 <siraben> remexre: Yay, got a dependent type system (λΠ) working using bidirectional type checking

05:56 <siraben> turns out type checking dependently typed languages requires reducing type to normal form before checking for equality

05:57 <siraben> and checking terms for equality can be more complicated if a named representation is used, if debruijn is used then it's just ==

05:58 <siraben> might try adding the equality type, natural numbers then maybe length-indexed vectors

05:58 <remexre> siraben: yeah, there's a {gross,clever} trick where you do different de brujin levels in the envt and indices in terms, too

05:58 <remexre> which iirc is so shifting levels is a no-op

05:59 <remexre> (I just use names though, heh)

05:59 <siraben> i'm using the bound library https://www.schoolofhaskell.com/user/edwardk/bound , which deals with this

05:59 <siraben> it's so nice

05:59 <siraben> succ'ing an entire tree takes O(1)

06:04 <remexre> nice

06:05 <remexre> er, though succ wouldn't be an example where you hit the unfortunate case

06:05 <remexre> it'd be turning x into (fun fresh_var => x) that's expensive

06:06 <remexre> or vice versa, which ofc is happening all the time in beta reduction

06:06 <siraben> ah, so in the bound library this is handled by the `abstract` and `instantiate` functions

06:07 <remexre> ah, okay; haven't had a chance to look through it, building a new server rn

06:08 <siraben> cool

06:10 <remexre> yeah, 24 cores, 288G ram; gonna be a new build box for lab + my forth projects

06:10 <remexre> considering trying to use angr to... "formally verify" isn't the right phrase, with the level of assurance it'd give me

06:11 <siraben> what's angr?

06:11 <remexre> but to give a more-formal-than "it looks right" guarantee that complicated stuff I implement is correct

06:11 <remexre> a symbolic execution engine from... ucsb?

06:11 <siraben> oh, interesting

06:11 <remexre> so I can take an ELF file and ask, "what would the machine state have to be for $bad_thing to happen in $func"

06:12 <remexre> and it uses an absurd amount of ram and maybe finds a thing

06:12 <siraben> does it use abstract interpretation?

06:12 <remexre> maybe one of the analyses does, but the "main thing" is symbolic execution

06:12 <remexre> where you just translate instructions to functions you give to an SMT solver, and it does the heavy lifting

06:13 <siraben> ah, of course

06:14 <siraben> i've thought about assigning a small-step operational semantics to Forth, or has that already been done?

06:15 <remexre> oh, I've seen a paper... lemme see if I can find it

06:15 <remexre> afaik there's exactly one work that models forth well enough for RDROP EXIT to work

06:15 <remexre> er, that's maybe an exaggeration

06:15 <remexre> but stuff that's "not OK in C-land" in general

06:16 <siraben> Looking around there only seems to be small step semantics for expressions or functional languages in terms of stack machines

06:16 <siraben> Right

06:17 <siraben> http://www.complang.tuwien.ac.at/anton/euroforth/ef12/papers/stoddart.pdf gives an axiomatic semantics for Forth

06:18 <remexre> ah neat, I hadn't seen this one before

06:19 <remexre> I can't find the paper on my phone, so I'll send it once I'm at a normal PC

06:19 <siraben> Oh oops it's not axiomatic semantics, the paper says it's "prospective value semantics"

06:21 <siraben> Ok, I'd be curious to see the paper you're referring to

16:43 <tabemann_> proteusguy: the change from BSD3 to GPL3 was motivated by that I borrowed a good amount of code from Mecrisp-Stellaris, which is GPL3 - I asked Matthias if he would relicense the code I was borrowing to BSD3/2/1 or MIT, but IIRC he said he was not going to relicense the flash driver code, which was a key part of what I was borrowing

16:50 <tabemann_> the problemm with rewriting the flash driver code is this sort of thing has an obvious way to do it

16:54 <tabemann_> make that proteus-guy:

18:16 <cmtptr> because we live in a litigious society

18:30 <proteusguy> I wasn't aware Mecrisp was GPL3. That's problematic. hrm....

18:46 <tabemann_> I myself would prefer that zeptoforth not be GPL3

18:47 <tabemann_> the problem with the flash driver code is there's only one way to really do it

18:47 <tabemann_> most of the code surrounding the flash driver core has been rewritten by me anyways

18:48 <tabemann_> what is left is essentially two words, "flash!" and "erase"

18:49 <tabemann_> then there's the double-cell arithmetic code, and that's because I don't really get how to do double-cell arithmetic primitives on Thumb-2

19:12 <Zarutian_HTC> cmtptr: you do, I dont

19:16 <tabemann> the thing for me is I'd like to get Matthias's permission on this, as I am already in contact with him, and also because in many cases a rewrite would be hard either because A) there's about one way to do it or B) I don't really get how to implement it on Cortex-M

19:33 <tabemann> bbl

20:34 <cmtptr> Zarutian_HTC, of course you do. you live on earth just like the rest of us

20:38 <Zarutian_HTC> cmtptr: litihious society is mostly confined to USA. Most companies elsewhere that modify open source software do send patches upstream and make the modified source code available. Usually they only care that the software has some sort of open source license.

20:50 <cmtptr> "litigious society is mostly confined to the us, but everywhere else they comply with the licenses anyway" strange argument but ok

21:20 <Zarutian_HTC> cmtptr: I understand the licenses and the reasons for them but not the irrational heat

21:23 <tabemann> free software licenses wouldn't be necessary were it not for copyright existing in the first place

21:25 <tabemann> the matter with free software licenses is that some people wish to prevent the incorporation of free software into proprietary software while others don't care

21:26 <tabemann> hence you get GPL versus BSD/MIT/Apache etc.

21:27 <tabemann> the problem with the former position is it prevents the incorporation of free software into other free software which isn't so restrictive

21:49 <cmtptr> yes

23:39 <Zarutian_HTC> tabemann: really? I have seen BSD and such licensed code pull in GPL code as compilation/static-libraries without any issues arising other than that any modification beyond the lib interface is upstreamed

23:40 <tabemann> I know you can pull in LGPLed code as shared objects without a problem

23:41 <Zarutian_HTC> any propertiery software wanting to use the BSD licensed software just have to either provide their own replacement for the GPLed code or be opensourced

23:42 <tabemann> with BSD licensed code wants to link with GPLed code the whole has to be released as GPL

23:42 <tabemann> same thing if BSD licensed code wants to statically link with LGPLed code

23:43 <tabemann> the exception is if BSD licensed code wants to dynamically link with LGPLed code

23:43 <tabemann> where then the BSD licensed part may remain BSD licensed

23:43 <Zarutian_HTC> nope, at least not in the European Economic Zone iirc what an copyright lawyer here told me and others

23:44 <Zarutian_HTC> the BSD part can remain BSD

23:47 <tabemann> https://en.wikipedia.org/wiki/License_compatibility#Kinds_of_combined_works

23:47 <crab1> Hello, #forth

23:47 <Zarutian_HTC> however the compilation artifact would be covered by GPL iff the GPL part was used

23:49 <tabemann> things work that way if the code you're linking with is LGPL

23:50 <Zarutian_HTC> you can look at it this way: the BSD part is like a story that refers to the GPL part as a different concurrent plot happening in the samw story world.

23:52 <Zarutian_HTC> you can release the BSD part, but to get the full effect/story-telling you either need the GPL part or a substitute

23:54 <tabemann> okay, from what it seems one can combine BSD and GPL code without having to relicense the GPL code if there is a "strong separation" between the wtwo

23:54 <tabemann> like between a process and an operating system

23:54 <tabemann> or between a kernel module and a kernel

23:55 <Zarutian_HTC> the "strong" seperation also applies to unikernels

23:57 <Zarutian_HTC> there you treat the source code parts as a combined recipie to produce the compilation artifact

23:58 <Zarutian_HTC> which in that case is the unikernel