00:00:00 --- log: started forth/21.07.05
00:43:06 --- quit: j0anna (Ping timeout: 120 seconds)
01:49:14 --- join: j0anna joined #forth
03:36:37 <cbridge_> <siraben> remexre: this is insanely impressive https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.25.3322&rep=rep1&type=pdf
03:37:16 <cbridge_> <siraben> I've been looking for such a text on and off for a while, Forth presents a unique formalization challenge if one wants to do it faithfully (that is, taking into account immediate/compile modes, adding words to the dictionary and so on)
03:38:26 <cbridge_> <siraben> Notably here they use the π-calculus to encode the semantics which is normally used for concurrent processes, I guess that turns out to be pretty natural for Forth.
03:41:31 <cbridge_> <siraben> "The next step is to translate our specification into a format suitable
03:41:31 <cbridge_> <siraben> for a proof assistant such as Coq [3] or Isabelle [10], so that it could be used as a basis for the formal verification of safety properties of Forth programs."
04:11:25 --- join: Glider_IRC__ joined #forth
04:14:18 --- quit: Glider_IRC_ (Ping timeout: 120 seconds)
06:29:06 --- quit: Vedran (Ping timeout: 120 seconds)
06:44:46 <cmtptr> ttmrichter, you have something against a nation celebrating its winning a war for sovereignty?
07:02:51 <cbridge_> <eris[m]1> its a bit ironic really 
07:06:36 <cbridge_> <eris[m]1> freedom for me but not for thee
07:08:27 <cbridge_> <eris[m]1> the only day ill celebrate is 9/9
07:38:30 --- join: Vedran joined #forth
07:53:34 <cbridge_> <nihilazo> I don't really get 4th July but hey, it's an excuse for food and  seeing folks so I'm not gonna complain about it
07:53:41 <cbridge_> <nihilazo> (although I'm not in the US so I don't celebrate it)
07:54:12 <cbridge_> <eris[m]1> hallo, nihilazo 
07:54:15 <cbridge_> <nihilazo> much the same way I feel about religious holidays, people deserve excuses to celebrate even if I disagree with the thing they're celebrating
07:54:17 <cbridge_> <nihilazo> hi
07:54:30 <cbridge_> <eris[m]1> funny to run into you here 
07:54:44 <cbridge_> <nihilazo> I'm surprised that it's funny, bc I feel like I talk about forth a reasonable amount
07:54:47 <cbridge_> <nihilazo> but hi
07:55:04 <cbridge_> <eris[m]1> haha, fair 
07:56:03 <cbridge_> <eris[m]1> america's pontification(funny word!) about freedom is very funny to me 
07:56:30 <cbridge_> <eris[m]1> considering the historic & current violations of freedom the american government partakes in 
07:57:10 <cbridge_> <nihilazo> yeah, I would agree w/ that
07:57:27 <cbridge_> <nihilazo> but I don't disagree with 4th july. It's a celebration of a thing that isn't real, but so are most celebrations
07:57:39 <cbridge_> <nihilazo> even birthdays were made up by the calendar
07:57:44 <cbridge_> <nihilazo> (well, made up when we invented the calendar)
07:57:56 <cbridge_> <eris[m]1> birthdays are a scam made by the birthday cake industry to sell more birthday cakes 
07:58:01 <cbridge_> <eris[m]1> and calendars 
07:58:03 <cbridge_> <nihilazo> :O
07:58:13 <cbridge_> <eris[m]1> obviously 
07:58:16 <cbridge_> <nihilazo> birthdays are a scam made up by mathematicians to invent more paradoxes
07:58:23 <cbridge_> <eris[m]1> fucking maths 
07:58:58 <cbridge_> <nihilazo> mathematicians: quick, we need some reason to talk about probabilities of things occuring in common among a random set in a sample
07:59:01 <cbridge_> <jhswartz> is this the part where you sell the birthday scammers some software written in forth?
07:59:11 <cbridge_> <nihilazo> mathematicians: *invents the birthday*
07:59:16 <cbridge_> <nihilazo> I mean, you could make a birthday paradox calculator in forth
07:59:19 <cbridge_> <nihilazo> might be a fun exercise
07:59:37 <cbridge_> <nihilazo> dunno
08:00:22 <cbridge_> <eris[m]1> personally, ive never seen a maths 
08:31:18 --- quit: Glider_IRC__ (Ping timeout: 120 seconds)
08:39:44 --- join: Glider_IRC_ joined #forth
09:01:01 --- join: Crab01 joined #forth
09:01:19 <Crab01> Hiya
10:43:21 <cbridge_> <remexre> siraben: huh, looking at figure 2, is there a fixed number of processes? I guess it could kinda make sense by analogy to how the actual hardware works, but "feels weird" to use pi-calc if you don't need to spawn new things
10:43:32 <cbridge_> <remexre> I'm definitely not well-versed in it at all though, heh
10:44:34 <cbridge_> <siraben> remexre: I also am not familiar with pi-calculus, and thinking about it more it's not clear to my why this concurrent channel-based model is better than say, standard operational semantics with different modules
10:47:17 --- quit: Crab01 (Ping timeout: 120 seconds)
12:29:08 --- quit: j0anna (*.net *.split)
12:29:23 --- join: j0anna joined #forth
12:32:50 --- quit: lonjil (*.net *.split)
12:32:50 --- quit: Glider_IRC_ (*.net *.split)
12:32:50 --- quit: iv4nshm4k0v (*.net *.split)
12:33:18 --- join: Glider_IRC_ joined #forth
12:36:40 --- join: lonjil joined #forth
12:36:40 --- join: iv4nshm4k0v joined #forth
13:40:39 <cbridge_> <dave0> maw
13:45:28 <cbridge_> <crc> maw dave0
13:45:34 <cbridge_> <dave0> maw crc 
14:05:19 --- quit: Glider_IRC_ (Connection closed)
14:05:55 --- join: Glider_IRC joined #forth
14:15:49 <cmtptr> this "all holidays are made up" take sounds like what i've have said when i was 12 and edgy
14:17:03 <cbridge_> <eris[m]1> the difference here is 'people deserve excuses to celebrate' ;)
14:17:46 <cmtptr> of course all things noteworthy are only noteworthy because humans attribute noteworthiness to them.  july 4th is not "made up," the US was founded by revolution.  it's natural and healthy to celebrate that
14:18:59 <cbridge_> <eris[m]1> im not one to celebrate the founding of the US, but hey 
14:19:46 <cmtptr> you said it was ironic and then some weird comment about freedom
14:20:00 <cbridge_> <eris[m]1> yes
14:20:27 <cmtptr> july 4th is not about freedom, it's the birthday of the union
14:21:07 <cbridge_> <eris[m]1> union 😩
14:21:45 <cmtptr> yes that is a word that i wrote
15:48:22 <veltas> You people and your big endian calendars
15:51:45 <veltas> Yeah it is a special kind of stupidity to seriously dwell on how special dates are 'meaningless', although I don't imagine anyone in here really has done that
15:58:20 --- quit: lonjil (*.net *.split)
15:58:20 --- quit: iv4nshm4k0v (*.net *.split)
15:59:45 --- join: lonjil joined #forth
15:59:45 --- join: iv4nshm4k0v joined #forth
16:39:28 --- quit: Glider_IRC (Connection closed)
16:39:58 --- join: Glider_IRC joined #forth
19:41:07 <cmtptr> why would you want your calendar to be little endian??
19:42:29 <cbridge_> <siraben> ew little endian calendars
19:42:32 <cbridge_> <siraben> heya imode 
19:42:55 <cbridge_> <siraben> or worse, calendar notations without a clear endianness like MDY
19:42:57 <cmtptr> i'm a staunch supporter of the imperial units system and even i admit that we write dates backwards in the us
19:43:33 <cbridge_> <siraben> how are imperial units better than the metric
19:43:39 <cmtptr> or everyone else does, rather.  i personally write datea correctly: Y-M-D
19:43:50 <cbridge_> <siraben> subdivisions for length/liquids is not even uniform in imperial
19:44:13 <cmtptr> base 12 is better than base 10 fight me
19:44:32 <cbridge_> <siraben> it's not even consistent base 12 lol
19:44:38 <cbridge_> <remexre> isn't the argument usually that in practice being able to take a quarter of something is more useful than a sane system
19:45:25 <cbridge_> <remexre> third, sixth, whatever -- more factors is more useful for humans
19:45:25 <cbridge_> <siraben> discussing the weather with people in the US is confusing, maybe we should just use kelvin to fix 0
19:45:48 <cbridge_> <siraben> Sure, that's what proponents say
19:45:54 <cbridge_> <siraben> but calculations are terrible to do in imperial
19:46:02 <cbridge_> <remexre> yeah
19:46:12 <cmtptr> idk what the usual arguments are.  the truth is it doesn't really matter, people are plenty smart enough to use either one, imperial has been around for longer and there is no compelling reason to switch
19:46:14 <cbridge_> <siraben> If I lay down 1500 13-foot rods, what's the total length?
19:46:31 <cbridge_> <siraben> "no compelling reason to switch" meanwhile billions of people are on metric
19:47:14 <cbridge_> <siraben> let's not ignore the fact that current imperial/british customary units are defined in terms of metric, officially
19:47:31 <cmtptr> if billions of people jumped off a cliff, would you?
19:47:35 <cbridge_> <remexre> yeah tbh I'd be fine with that being the common state too
19:47:47 <cbridge_> <remexre> like, everything important is in kg/L/km, etc
19:47:53 <cbridge_> <siraben> if billions of people used a more uniform system for units, I would use it.
19:47:56 <cbridge_> <remexre> but recipes don't try to make me measure out things in metric...
19:47:56 <cbridge_> <siraben> imode: lmao
19:48:20 <cbridge_> <siraben> remexre: I feel like that's a convention rather than a technical issue
19:48:24 <cmtptr> if you laid down 1500 13-meter rods, what's the total length?
19:48:29 <cbridge_> <siraben> I've also heard that "mile" is more natural because it means "a thousand steps"
19:48:35 <cbridge_> <siraben> which is a terrible argument since each step is 1.6 m
19:48:54 <cbridge_> <siraben> cmtptr: 19500 m, just multiply
19:49:14 <cmtptr> how is that any different from your feet example?
19:49:15 <cbridge_> <siraben> imode: yeah hence why that argument doesn't really work
19:49:27 <cbridge_> <siraben> cmtptr: because let's have it in miles or kilometers
19:49:31 <cbridge_> <siraben> in KM, it's 19.5
19:49:34 <cbridge_> <siraben> what about in miles?
19:49:55 <cbridge_> <siraben> 1500 * 13 = 3.69 miles, wtf
19:50:08 <cmtptr> idc i like it just fine in feet
19:50:35 <cbridge_> <siraben> Yes.
19:50:50 <cbridge_> <siraben> Imagine if units of information had an imperial system, madness!
19:51:03 <cbridge_> <dave0> maw
19:51:06 <cbridge_> <siraben> mega/giga/tera-byte, SI prefixes FTW
19:51:24 <cbridge_> <siraben> remexre: I think the worst part is when they get combined
19:51:28 <cbridge_> <siraben> pounds per square inch
19:51:37 <cmtptr> did that mibi gibi bullshit ever get formally adopted
19:52:05 <cbridge_> <siraben> imode: so mebi/gebi stuff right?
19:52:11 <cbridge_> <siraben> gibi*
19:52:48 <cmtptr> is there someone named imode who is ignored by cbridge?
19:53:26 <cbridge_> <siraben> hm how would people do chemistry with imperial
19:53:51 <cbridge_> <remexre> same way people do accounting with roman numerals :P
19:53:51 <cbridge_> <siraben> you need kelvin, and a delta of 1 K = delta of 1 C
19:54:07 <cbridge_> <siraben> delta of 1 K = delta of ??? F
19:54:26 <cbridge_> <siraben> it's been around longer, ergo it must be better.
19:55:48 <cmtptr> why wouldn't you just stick with K?
19:55:54 <cbridge_> <siraben> imode: I grew up with metric, so when I saw imperial units for the first time I was like, this is probably some made-up example (like they do with random currencies etc. in kid's math problems)
19:56:19 <cmtptr> there's no reason the scale of kelvin has to be the same as the scale of celcius
19:56:33 <cbridge_> <siraben> but it is
19:57:17 <cmtptr> yes but i'm saying that's hardly a point for why metric is better for chemistry
19:57:27 <cbridge_> <siraben> does anyone know what the meaning of 0 F is?
19:57:58 <cbridge_> <siraben> cmtptr: because everything in thermodynamics and energy uses metric, otherwise you'd have to refine joule, watt, etc.
19:58:18 <cmtptr> you could just as easily define an absolute temperature unit based on fahrenheit
19:58:53 <cbridge_> <siraben> 0 F is -17.78 celsius, hm.
19:59:12 <cmtptr> sorry i'm typing on this goddamn motjerfuckibg touchscreen phone so i'm slow to respond
20:00:14 <cmtptr> both celsius and fahreneit are arbitrary scales
20:00:16 <cbridge_> <siraben> imode: is there subdivisions of length smaller than an inch
20:00:23 <cbridge_> <siraben> how do you talk about microns, nanometers
20:00:25 <cmtptr> mils
20:00:40 <cbridge_> <siraben> mils?
20:01:18 <cmtptr> why are you trying to shoehorn a units system where it doesn't make sense
20:01:37 <cmtptr> i never said there is no place for metric
20:01:45 <cbridge_> <crc> siraben: 0F was originally the temperature of a particular brine of water, ice, and ammonium chloride
20:02:30 <cbridge_> <MrMobius> ya imperial units are completely illogical and unreasonable
20:02:37 <cbridge_> <crc> oh, it's really arbitrary.
20:02:40 <cbridge_> <siraben> imode: also are your messages being relayed across the bridger?
20:02:40 <cbridge_> <MrMobius> almost as bad as the stupid system they use in europe for time
20:02:40 <cbridge_> <siraben> bridge*
20:02:47 <cbridge_> <siraben> cmtptr: are you able to see imode's messages?
20:02:52 <cmtptr> no
20:02:53 <cbridge_> <MrMobius> i mean how could anyone ever remember whether there's 6 or 48 or whatever it is hours in a day
20:03:00 <cbridge_> <siraben> lol ok
20:03:30 <cbridge_> <MrMobius> ya theres just no way a normal human could ever use anything but base 10...
20:05:05 <cbridge_> <siraben> imode: kinda easy when you wipe the servers
20:05:06 <cmtptr> all bases are base 10
20:05:12 <cbridge_> <siraben> oh I think if I mention imode then it doesn't send as well
20:05:31 <cmtptr> no i see you talking to imode
20:06:08 <cbridge_> <siraben> lol
20:39:40 --- join: Glider_IRC_ joined #forth
20:42:33 --- quit: Glider_IRC (Ping timeout: 120 seconds)
23:16:06 --- quit: iv4nshm4k0v (Ping timeout: 120 seconds)
23:26:34 <cbridge_> <hexagon5un> alexg_k: anyone using a forth on the ESP32? which one?  how well does it play with the WiFi/networking?
23:26:57 <cbridge_> <hexagon5un> (sorry, not to alexg_k -- he's not even here!)
23:45:33 <proteusguy> MrMobius - my uncle got a finger sliced off in a box cutting machine years ago. He now uses base 9.5. :-)
23:46:09 <proteusguy> To be honest it's probably more like base nine and three quarters.
23:59:59 --- log: ended forth/21.07.05