00:00:00 --- log: started forth/15.02.19 00:11:59 --- quit: mnemnion (Remote host closed the connection) 00:12:32 --- join: mnemnion (~mnemnion@c-98-210-219-91.hsd1.ca.comcast.net) joined #forth 00:32:50 --- nick: ASau` -> ASau 01:30:19 --- quit: ASau (Remote host closed the connection) 01:31:31 --- join: ASau (~user@46.114.23.211) joined #forth 01:41:35 --- quit: ASau (Remote host closed the connection) 01:41:51 --- join: ASau (~user@46.114.23.211) joined #forth 01:43:51 --- join: nighty-_ (~nighty@hokuriku.rural-networks.com) joined #forth 02:37:52 --- quit: ASau (Remote host closed the connection) 02:51:56 --- join: true-grue (~grue@95-27-158-248.broadband.corbina.ru) joined #forth 03:32:06 --- nick: quuxman_ -> quuxman 03:48:37 --- quit: proteusguy (Remote host closed the connection) 04:34:56 --- join: proteusguy (~proteusgu@ppp-110-168-229-207.revip5.asianet.co.th) joined #forth 04:34:57 --- mode: ChanServ set +v proteusguy 05:18:28 --- join: joneshf-laptop (~joneshf@98.208.35.89) joined #forth 06:07:42 --- quit: mnemnion (Read error: Connection reset by peer) 06:07:56 --- join: mnemnion (~mnemnion@c-98-210-219-91.hsd1.ca.comcast.net) joined #forth 07:10:26 --- quit: protist (Quit: Konversation terminated!) 07:37:54 --- join: xtalmath (~xtalmath@ip-81-11-172-98.dsl.scarlet.be) joined #forth 07:39:17 --- quit: joneshf-laptop (Remote host closed the connection) 07:39:58 --- join: joneshf-laptop (~joneshf@98.208.35.89) joined #forth 08:00:21 --- quit: nighty-_ (Ping timeout: 246 seconds) 08:04:34 --- join: nighty-_ (~nighty@hokuriku.rural-networks.com) joined #forth 08:24:58 --- quit: darkf (Quit: Leaving) 09:20:15 --- quit: nighty^ (Remote host closed the connection) 09:22:29 --- join: blandflakes (4815c642@gateway/web/freenode/ip.72.21.198.66) joined #forth 09:37:31 --- quit: malyn_ (Ping timeout: 255 seconds) 09:40:15 --- join: malyn_ (~malyn@unaffiliated/malyn) joined #forth 10:04:02 --- quit: malyn_ (Read error: Connection reset by peer) 10:12:43 --- join: malyn_ (~malyn@unaffiliated/malyn) joined #forth 10:44:57 --- join: kumul (~mool@adsl-72-50-86-186.prtc.net) joined #forth 11:40:35 --- quit: fantazo (Quit: Verlassend) 11:51:00 --- quit: kumul (Ping timeout: 264 seconds) 12:14:43 --- join: JDat (~JDat@89.248.91.5) joined #forth 12:17:15 --- join: kumul (~mool@adsl-72-50-85-250.prtc.net) joined #forth 12:35:57 --- quit: kumul (Quit: Leaving) 13:03:37 --- quit: karswell (Ping timeout: 264 seconds) 13:18:24 --- join: Mat4 (~claude@ip18861915.dynamic.kabel-deutschland.de) joined #forth 13:18:26 hello 13:18:34 --- join: Zarutian (~Adium@168-110-22-46.fiber.hringdu.is) joined #forth 13:23:47 --- join: nighty^ (~nighty@static-68-179-124-161.ptr.terago.net) joined #forth 13:32:48 --- quit: JDat () 13:39:45 --- join: bedah (~bedah@g231052123.adsl.alicedsl.de) joined #forth 13:40:22 hey 13:48:30 hi bluekelp 13:48:47 I make some progess with my web design 13:58:10 Mat4: What tools do You prefer for web stuff? 13:58:53 vim 13:59:26 and an online documentation of CSS 14:03:06 need some sleep, ciao 14:03:09 --- quit: Mat4 (Quit: Verlassend) 14:30:57 * Zarutian uses TextWrangler and what he knows of HTML 4.0 for web stuff ;-Þ 15:05:05 how good is gforth at optimized compilation? when words are compiled into the dictionary, are they compiled to machine language? 15:07:18 --- quit: nighty-_ (Quit: Disappears in a puff of smoke) 15:16:48 --- quit: Zarutian (Quit: Leaving.) 15:27:05 --- quit: mnemnion (Remote host closed the connection) 15:27:38 --- join: mnemnion (~mnemnion@c-98-210-219-91.hsd1.ca.comcast.net) joined #forth 15:34:34 --- join: kumul (~mool@adsl-72-50-84-186.prtc.net) joined #forth 15:35:14 --- quit: joneshf-laptop (Read error: Connection reset by peer) 15:35:29 --- join: joneshf-laptop (~joneshf@98.208.35.89) joined #forth 15:43:47 --- quit: blandflakes (Quit: Page closed) 15:47:48 --- quit: mnemnion (Read error: Connection reset by peer) 15:47:58 --- join: mnemnion (~mnemnion@c-98-210-219-91.hsd1.ca.comcast.net) joined #forth 16:10:50 --- join: chouser (~chouser@184.17.233.12) joined #forth 16:27:23 --- quit: true-grue (Read error: Connection reset by peer) 16:29:58 --- join: malyn- (~malyn@unaffiliated/malyn) joined #forth 16:30:36 --- quit: malyn_ (Read error: Connection reset by peer) 16:35:39 --- quit: chouser (Ping timeout: 256 seconds) 16:37:55 --- join: MrMobius_ (~MrMobius@50-195-233-75-static.hfc.comcastbusiness.net) joined #forth 17:00:28 --- join: chouser (~chouser@c-68-44-5-241.hsd1.nj.comcast.net) joined #forth 17:23:18 xtalmath: forth compilation isn't like C or other "compiled" languages. generally forth words "compile" to a list of other words' addresses 17:23:27 especially in indirect threaded forths 17:23:48 or in direct threaded. nevermind my mention of indirect. 17:24:04 yeah, I just read that 2 minutes ago ;-) I had not reached that part of the book yet when I asked the question 17:24:19 haha. no worries. 17:24:25 I still have no clue what the difference between direct and indirect threading is 17:24:44 also not yet seen any threading words in gforth yet 17:25:06 i used to worry about the speed of dict lookups w/a linked list and wanted to optimize until i realized it doesn't slow the perf of the forth down at runtime, etc. 17:26:06 you won't - threading in forth doesn't mean "run on separate cores" like in C-land. it's a term to describe how the execution threads its way from word to word to do stuff 17:26:43 --- quit: chouser (Ping timeout: 240 seconds) 17:26:47 --- join: johnmark_ (~johnmark@c-73-51-235-57.hsd1.il.comcast.net) joined #forth 17:26:48 so dict lookups are only important while compiling right? that's also why redefining a word W does not change other words which used the old W, since they still contain the old xt pointers? 17:27:22 yes (to all) 17:27:47 after you finish the book, i recommend reading through the source of a forth. i personally like jonesforth because it's documented in a way i found easy to follow reading from top to bottom 17:28:21 is jonesforth or any forth large? it takes a day or so to read through? 17:28:29 that will give you a good idea of how things work under the hood and the assembly knowledge require isn't much. jones holds your hand through that 17:28:38 ok 17:28:40 How do I get an input statement in FORTH? INPUT "Weight on Earth?";W 17:29:21 bluekelp: is the threading in the sense of "multiple cores" possible with forth? 17:29:29 jonesforth is fairly small. depending on how deep you try and understand you can spend anywhere from a few hours to days 17:30:11 xtalmath: yes- but i'm not aware of any "userland" forths doing it. generally the ones that run on bare metal and "own" the cpu would be the ones i'd expect to operate that way 17:30:15 bluekelp: I'm also curious how machine language is entered in words 17:30:34 http://rosettacode.org/wiki/User_input/Text#Forth 17:31:36 other forths will multi-task by "context switching" between words and switch to new stacks. or have a form of cooperative multi-tasking where the QUIT word switches, etc. 17:31:50 but i don't have any experience with multi-user forths 17:32:11 oh ok 17:32:28 there's an implementation of retro in go that supposedly has multiple instances of the vm... i haven't really looked at it. 17:34:03 it's because someone was talking about a dev board, with an IC on it that runs like 144 2/3 Ghz "forth" cores. that sounded quite amazing, but I always conflated forth and fortran. this person then pointed out that forth was something else entirely, and the past 2 or 3 days I've been looking up forth, reading the starting forth 17:34:27 the IC's cost like 20$ a piece at 10-pack volume 17:35:18 the ga144? 17:35:41 gforth is looking for a float 200e0 6e0 f/ f. How do in INPUT a float? 17:35:44 I still find it a bit hard to believe, I know its a naive comparison, but 144*2/3 Ghz = about 100 Ghz 17:35:52 bluekelp: yes ga144 17:35:54 not sure about IC price but it's the only one i'm aware of that's currently on the market as a "forth core" 17:37:08 --- join: chouser (~chouser@c-68-44-5-241.hsd1.nj.comcast.net) joined #forth 17:37:14 bluekelp: not sure what the catch is, also not sure how the memory bandwidth for so many 'cores' (?) can be satisfied. or is that because its a stack machine with relatively few random accesses? 17:38:38 this chip sounds too good to be true 17:38:48 it must be me interpreting something strangely 17:39:48 i don't know much about the chips or memory addressing either 17:40:09 iirc they're quite low power (power consumption) too 17:40:20 yeah, but I should first focus a bit more on the language, and then look at the chip's datasheets 17:41:12 yes, I also read low power. If I compare with a random current quad core ARM thats often 4*2Ghz... 17:41:34 --- quit: impomatic (Read error: Connection reset by peer) 17:41:47 perhaps the chips take 20 cycles on average per instruction :) 17:42:35 ttmrichter tried to get a ga144 demo board project going but found them a difficult/impossible vendor to work with so i don't think they're destined for world domination. their own demo board is too expensive for most of us to bother with 17:42:59 yeah, the person I was talking to had one, but also said it was quite expensive 17:43:04 those ga144s are "asynchronous" first of all meaning the dont share a universal clock or anything like any other architecture. I dont know exactly what effect that has. 17:43:30 and iirc you need a special forth, based on colorforth, to use to get the chip to sing; perhaps that's just the vendor's preferred dev tool though and other forths would be easy enough to do 17:43:47 also, iirc each "core" has 64 words of program and 64 of stack space, so no sharing although they can pass data to adjacent cores. passing data to farther cores requires passing it along all cores in between 17:44:19 MrMobius_: I think most multicores are asynchroneous, often cores can sleep independently, or run at different rates 17:44:21 and, there is a custom board built for it for about $40 that comes with the chip so you dont have to buy 10 of them 17:44:30 --- join: impomatic (~chatzilla@87.113.239.117) joined #forth 17:45:08 there is a guy who got one running and built a little ram for it as a hobby project if you google around some 17:45:12 MrMobius_: 64 words sounds low? 17:45:43 not sure what kind of applications one can make on that? 17:45:58 xtalmath: i suppose. not even the people who made the chip can tell anyone what the hell to use it for. maybe there is some application where each core does something relatively simple but can be parallelized like in a graphics card 17:46:26 xtalmath: right, hence the fact that they dont sell very well. there is no "wow" demo project the people who sell it have to convince people to buy it 17:46:35 yeah, it sounds a bit like between fpga and processor 17:47:14 heh, used as an fpga at least its better documented, and one doesnt need xilinx? lol 17:47:26 64 32bit cells? 17:47:34 perhaps. unless you are running a multi-tasking OS or doing scientific calculations or something i think it is hard for people to figure out what to do with more than one core 17:48:27 yeah, I cant really imagine many applications, perhaps radar processing or dataflow smth 17:48:54 unless the chip is optimized to add fat cache or RAM 17:49:09 sure. for $40 you can play with it though. seems like a neat toy if you have the money. 17:49:26 I thought the dev board was much more expensive 17:49:36 or the 40$ one is a breakout board by another party? 17:49:52 right, breakout 17:50:29 hm, might buy one of those, but I guess its RS232 and not USB... hmmm 17:52:09 xtalmath: the memory bandwidth is small because each core has its own ram. (but it's a very small amount) 17:53:33 tangentstorm: you mean that the original unknown application probably had low bandwidth requirement? 17:54:00 beats me 17:54:04 I dont think there was an original application 17:54:31 I think there must be, but for some reason they are not allowed to talk about it, else they would definitely promote it as a use case 17:55:24 I don't think people invest money in designing a 144 core IC without having at least 1 valid use case 17:55:57 the guy is a millionaire from all his patents and wanted to make a chip 17:56:10 ya, its the guy who invented forth so he can do whatever he wants 17:56:36 although he has designed lots of other forth based architectures 17:56:44 MrMobius_: when you said 64 words stack space, you mean 64*4 bytes? 17:56:47 so not totally without precedent 17:57:01 xtalmath: dunno, try looking at the PDFs on their site 17:57:06 oh the inventor of forth is behind the ga144? 17:57:24 yes 17:57:56 yes. chuck designed the f18a - and 12x12 of those make up the ga144 17:58:08 a word on the ga144 is 18 bits, if i recall correctly. 17:58:17 144*(64+64)*4=72KB 17:58:27 * tangentstorm thinks that's where the 18 comes from in f18a.. not 100% sure. 17:58:37 oh ok 17:59:48 but: each word can hold like 5 instructions i think? 18:00:02 so not a lot of data but lots of code. 18:00:42 My laptop CPU: L1d cache: 32K, L1i cache: 32K, L2 cache:1024K 18:02:46 perhaps the forth inventor is into bitcoin mining :) 18:03:45 for every ga144 he sells, he can make 3 for himself or smth 18:04:28 --- quit: chouser (Ping timeout: 245 seconds) 18:04:55 his name's chuck moore.. http://colorforth.com/ 18:05:10 ok i'll try to remember the name 18:06:11 family of Moore from Moar's law? 18:06:57 no that's gordon moore of intel. 18:07:04 --- join: darkf (~darkf___@unaffiliated/darkf) joined #forth 18:07:06 no relation as far as i know. 18:07:10 ok 18:12:14 L1d and L1i cache are data and instruction cache? 18:14:27 I'm trying to see the analogy between ga144 and my CPU a bit, and it looks a bit like ga144 RAM is on the order of L1 cache memory size 18:14:55 (I made a calculation mistake for the 72KB which assumed 32bit words instead of 18 bit words) 18:16:58 each of those cores also has ROM on it. 18:17:31 different cores contain different code in the rom, depending on where they are on the board. 18:18:03 or i guess which ports they touch 18:19:08 yeah, the web page also says very flexible IO pin mapping, so it really seems like some processorbased fpga-like thing... 18:20:19 perhaps one could write a VHDL => ga144 implementation lol 18:23:17 maybe 18:35:40 --- quit: MrMobius_ (Read error: Connection reset by peer) 18:38:12 heh US EAR ECCN 3A991A.3 these chips are export controlled 18:39:44 I can't find the meaning of that export control code 18:50:03 3A991A.3 = "More than one data or instruction bus or serial communication port that provides a direct external interconnection between parallel “microprocessor microcircuits” with a transfer rate of 2.5 Mbyte/s." 18:51:09 must insure every processor with externally accessible data/instruction bus has a hardware backdoor or smth? 18:52:43 they also seem very suspicious of "Digital integrated circuits based on any compound semiconductor having an equivalent gate count of more than 300 (2 input gates)." 18:52:54 lol those export regulations are entertaining to read 18:53:22 --- quit: kumul (Quit: Leaving) 18:54:48 I can't really imagine congress deciding on these regulations, who makes them up? 18:56:03 or are patent properties fed into export regulations, such that anyone who manufactures a device self-reports his patent infringements lol? 18:57:00 iirc they're there to help stop other countries from developing crypto, weapons, and radar systems. at least w/export controls someone somewhere could track a sudden increase in purchasing and then we wouldn't suddenly be surprised by 2,000 enemy robots attacking our secret antarctic bases 18:57:04 or perhaps its just a wish-list of new technologies/manufacturing methods 18:57:37 our secret antarctic bases... hmm 18:57:48 oops - pretend i didn't mention those 18:58:14 bluekelp: that almost implies NSA formulates the export regulations? 19:00:23 if so, export regulations say a lot of what's on their minds... 19:02:46 or perhaps its much more mundane, a form of advertising like flashing goods, playing hard to get, to boost export sales :) 19:03:05 "you can watch but not touch" :P 19:07:40 obviously the NSA is worried about enemy robots attacking secret bases in a place that shall not be named 19:07:57 hollow earth ? 19:10:56 I think the ga144 is used for a specific secret purpose, and listed under a trivial regulation so as to not betray the original usage 19:11:43 --- join: chouser (~chouser@c-68-44-5-241.hsd1.nj.comcast.net) joined #forth 19:11:46 it might be self-listed; not sure where the burden lies but i'd assume on the chip OEM and not the regulatory agency (to list, or state it is controlled) 19:12:15 oh today I looked up the local jobs database, and the only job offer mentioning "forth" was one for a company that designs and sells kitchens, using forthcad to render them... seems like no forth jobs in belgium... 19:14:57 people in this channel are forth enthusiasts, or you guys earn money with forth specifically? 19:15:49 i think it's mostly enthusiasts but i'd like to hear from anyone using it at work 19:22:07 I am semi cringing when I read chuck moore's blog :S 19:25:33 --- join: saml_ (~saml@cpe-24-102-97-97.nyc.res.rr.com) joined #forth 19:28:34 i have never seen a forth job. 19:34:33 hmm apparently the ga144 is a 18 by 8 array 19:42:06 "The chip is not the chip." hmm 19:47:04 why cry? other than the outdated look it's not that bad ;) 19:47:22 chuck does come across as a pessismist from his own web site, yes 19:47:34 in person (from videos) he seems much more normal 20:08:16 --- join: ASau (~user@46.114.23.211) joined #forth 20:11:58 --- quit: dys (Ping timeout: 252 seconds) 20:25:40 --- quit: johnmark_ (Quit: Leaving) 20:50:44 --- quit: chouser (Ping timeout: 240 seconds) 21:31:19 --- join: chouser (~chouser@c-68-44-5-241.hsd1.nj.comcast.net) joined #forth 21:36:32 do I understand correctly that most of the execution time in a forth system is spent calling a word, until the lowest level words defined as machine language, and then returning from words or progressing to the next word? 21:37:10 so it seems like it is rather scripted? 21:45:00 --- quit: saml_ (Ping timeout: 246 seconds) 21:47:26 --- join: true-grue (~grue@95-27-136-26.broadband.corbina.ru) joined #forth 22:11:15 --- join: gabriel_laddel (~user@unaffiliated/gabriel-laddel/x-9909917) joined #forth 22:16:41 --- join: karswell (~user@201.67.208.46.dyn.plus.net) joined #forth 22:34:04 --- join: darkf_ (~darkf___@2601:7:1801:a8ae:7dc2:148d:631a:1504) joined #forth 22:34:19 --- quit: darkf (Ping timeout: 250 seconds) 22:34:21 --- quit: darkf_ (Changing host) 22:34:21 --- join: darkf_ (~darkf___@unaffiliated/darkf) joined #forth 22:36:18 --- nick: darkf_ -> darkf 22:44:41 I'm not sure what you mean by "rather scripted" here. 22:49:35 I mean that except for basic words like perhaps - (minus) etc there is no use of the processors registers, so all the "architecture/call hierarchy" and next word calling is not really compiled, just literally subroutines calling subroutines, and only the "leaves" of subroutines perform actual work? 22:50:57 if you look at a disassembly of a compiled c program, you'll see relatively few calls and returns, most instructions operate on registers consecutively 22:51:39 while if I look at the dictionary and the code of each "word" I think I will see mostly calls, correct? 22:52:21 --- quit: gabriel_laddel (Ping timeout: 245 seconds) 22:52:49 Not calls, no, unless you're subroutine-threading. 22:52:53 You're more likely to see jumps. 22:53:13 But yes, Forth is generally classified as an interpreted language, not a compiled one. 22:53:16 ok then jumps, most of the time its jumping 22:53:27 oh ok 22:53:28 Forth is an abstraction of an abstract machine, basically. 22:54:22 Now there are different implementation strategies (indirect threading, direct threading, subroutine threading, token threading, various combinations and hybrids of these) and there are environments that will do more traditional compilation by unthreading all that stuff and putting relevant code inline. 22:54:34 I really like how there is no need for shell scripts, and the shell is the same as the programming environment, I just wish this could be combined with actual compilation to machine language? 22:54:38 In the code output by those environments you'll see more C-like stuff. 22:55:15 ttmrichter: so I assume these different implementations correspond to different compilers in the forth environment? 22:55:25 If you turned Forth into a traditional compiled language, though, I think you'd be throwing away the parts that are good and keeping the parts that make it a tad difficult. 22:55:27 and a different EXECUTE? 22:55:56 There are probably thousands (literally) of Forths out there. It seems a rite of passage for a certain breed of geek to make a Forth. :) 22:56:14 Not so much nowadays (although it's still there), but in the '80s it was hard to find a programmer who hadn't. 22:56:17 ive been thinking, someone must have named on rutherforth 22:57:13 ttmrichter: is there a place that explains the different implementation strategies? 22:57:19 Yes. Hold on. 22:58:27 http://www.bradrodriguez.com/papers/moving1.htm 22:59:52 ttmrichter: thanks 23:00:54 ttmrichter: you also hinted at traditional compilation would be throwing away good parts, which good part would be lost as an example ( I'm very new to forth ) 23:03:32 --- join: darkf_ (~darkf___@unaffiliated/darkf) joined #forth 23:03:45 Well, the "see" word would be a bitch to write in a binary-compiled word. 23:04:01 Let's use this word definition as an example: 23:04:06 : SQUARE DUP * ; 23:04:15 (It's the one used in that article series I pointed you at.) 23:05:25 I dont know the see word 23:05:28 If you used "see" on that word, the implementation of the runtime would just have to take the word's definition, find the code field, walk the list of pointers, reverse-lookup those pointers in the dictionary and quickly print off the constituent words. 23:06:14 yes, there would need to be source backups 23:06:15 See gives you a listing of a word. 23:06:31 Or there would have to be some way to annotate your compiled words. 23:06:34 Or ... 23:06:40 (There's about a thousand ways to do it.) 23:07:05 yes, I was thinking about implementing a "see" then, but was waiting for the book to define it 23:07:06 But anything you do will take the already-bloated code of your compiled version and bloat it further. 23:07:13 Which book? 23:07:15 --- quit: darkf (Ping timeout: 250 seconds) 23:07:26 starting forth 23:07:26 And that "already-bloated" thing is the next piece. 23:07:31 I'm at the IO section 23:08:01 Forth is a very small language and Forth programs tend to take a very small amount of space. 23:08:16 ttmrichter: so the word form is always more compact than theoretical compiled forms? 23:08:29 I have on my system three Forths for embedded systems that will fit into a tiny 32-bit MCU (4KB RAM, 16KB Flash) with plenty of room for a user program. 23:08:38 Not always, but usually, yes. 23:09:04 Again, using the SQUARE definition above. 23:09:28 SQUARE would have to be decompiled into DUP and * contents. 23:09:46 DUP and * would likely be primitives. 23:10:17 So every time you use square, instead of having one pointer (32-bits on the aforementioned MCU) you'd have the full binary code for DUP and *. 23:10:19 pop , mov, mul yeah not much to derive the original word sequence from 23:10:51 Now the MCU in question uses Thumb2, so mul would be... about 48 bits long. 23:10:58 *, I mean. 23:11:11 DUP would be about the same size, I suspect. 23:11:13 --- nick: darkf_ -> darkf 23:11:33 So your net cost each time you use SQUARE would be a +150% premium. 23:11:49 You now have to balance cost of execution against cost of space. 23:12:23 And in a machine that has 20KB total storage, only 4KB of which is meaningfully modifiable at runtime, you're probably more interested in space. 23:12:32 ttmrichter: since RAM is slower than cache memory, does compacter code mean less stalls? or the instruction cache becomes too random for forth to profit in this sense? 23:13:03 yes, I agree on space constraint issue 23:13:44 do say hard drive microcontrollers typically run forth? 23:14:06 Probably not. 23:14:26 Actually, I can go so far now as to say definitely not, given that someone hacked one and installed Linux on it. :) 23:14:46 The one he hacked had a Cortex-M3 MCU and two Cortex-A cores. 23:14:51 yeah, I remember reading that 23:15:21 what about usb flash memory sticks? I hear they run some tiny OS? 23:16:33 The ones I know of have super-fast 8051 clones on them with bizarre extensions. Don't know what software they run. 23:16:34 do you know of everyday items that sometimes use forth? 23:17:08 Either UPS or Fedex (can't recall which) use Forth in their little signature pads. 23:17:16 When you sign for a package you're using a Forth system. 23:17:36 yeah, recently signed one such signature pad 23:17:43 I also know of a few warehousing systems that shunt goods around using bar code readers and actuators driven by Forth. 23:18:21 I think nowadays is mostly PLC in factory automation, could be wrong though 23:20:17 A lot of "PLCs" are actually microcontrollers fronting as ladder-logic devices. 23:20:37 thanks for the porting forth guide, this looks real interesting 23:20:43 Oh, another place Forth is used is pretty far out there. 23:20:46 Literally, I mean. 23:20:48 space 23:20:51 yeah philae 23:20:55 :) 23:20:56 Right. 23:22:51 is it easier to formally verify forth code than other languages? 23:25:22 I guess for every word desirable guarantees could be proven, and for higher level word's guarantees can be proven in terms of the guarantees of the lower level words ? 23:26:52 I don't do formal verification so can't really help there. 23:26:58 it would require the programmer to generate a proof for every word's desired guarantees though 23:29:46 ttmrichter: oh, I really recommend studying metamath at least once in your life, it's open source, it has a minimal (python) implementation (more verbose original in c) of about 300 lines, and a free book explaining the proof checker, and a creativecommons database of 18000 axioms , theorems and their proofs. 23:30:07 --- join: fantazo (~fantazo@089144198233.atnat0007.highway.a1.net) joined #forth 23:30:38 I read the book in 2 days, and translated the minimal implementation to another language to force myself to interpret every step (which I must sometimes have lightly skipped reading the book). 23:32:00 the reward: at the end you have rewritten the proof checker and can test it against the database: result I understand the proof checking process, and know with high certainty that the 18000 theorems follow from the axioms, even though I hardly know any of the theorems, let alone their proofs! 23:33:54 ttmrichter: it's also a crazy worldview changer, the fields proof checkers could be used in theory, like smart contracts, or law (replace judges with proof checker), science (force explicitly stating the assumptions, or else you fail to arrive at the conclusions) 23:35:19 metamath can work on any formally described belief system, it does not have to be mathematics (which is the supplied database) 23:35:53 xtalmath: The problem is that I really, really, really, really, really, really do not enjoy mathwank. 23:35:58 we could create a new medium, beside audio, video,... credo. people can subscribe to belief systems 23:36:02 ttmrichter: ok lol 23:36:22 ttmrichter: neither not enjoy logic? 23:36:34 As soon as you start talking about "theorems" I start looking at interesting reading like spec sheets on SPI flash parts. 23:36:55 (And you have NO idea how boring SPI flash data sheets are...) 23:37:15 ttmrichter: may I try to convince you of the importance of proof checkers with one little argument? 23:37:38 You may, but it won't work. 23:38:04 You can blame the maths teachers over the years who convinced me math was at best a necessary evil (emphasis on evil). 23:38:17 When maths teachers learn to educate, perhaps then maths won't be something people hate with such a passion. 23:39:47 every form of communication (like reading spec sheets, or talking on IRC) implies that the content is true. without a distinction between true/false (i.e. as soon as true and false can be proven equivalent in a belief system, i.e. a proof of inconsistency) then every form of communication within this belief system loses value, since its both true and false 23:40:32 if we all started formalizing our belief systems, or at least subscribing to popular maintained ones, then people could search for inconsistencies in other's belief systems, forcing them to drop an axiom/assumption 23:41:03 with proof checkers this can be done in an objective way 23:41:22 An objective and INCREDIBLY tedious and boring way, yes. 23:41:23 today mathematicians and logicians are in an ivory tower 23:41:41 When that "tedious and boring" thing is dealt with, maybe we'll see more of it. 23:42:00 I have a friend who's a huge fan of Coq. (Insert 12-year old sniggers here.) 23:42:14 Every time he shows me things he can do with Coq, I roll my eyes. 23:42:35 Because what he's showing me is that it takes 50 lines or more to make a function that provably only adds two to a passed-in number. 23:42:41 hm, I don't know Coq, Haskell etc 23:42:45 I'm ... not seeing the benefits. 23:43:14 I start seeing massive scaling problems when you have literally a 25:1 ratio of proof to stuff that actually does things. 23:43:34 well, I can imagine that when we start all holding cryptocurrency, people will want proof there software is secure in certain senses... 23:44:54 Why? 23:45:14 People don't have proof now that their "physical" (most of which isn't) currency works and is secure. 23:45:27 You overestimate people's care for this kind of stuff. 23:45:34 Look at the Bitcoin madness. 23:45:46 Bitcoin is CERTAINLY not proved. (And its a complete mess.) 23:46:07 I know Bitcoin is not proofchecked, this is kind of the argument 23:46:19 And yet you have a bunch of hipster yahoos clinging to their Dunning-Krugerrands like it's literal gold. 23:47:18 ttmrichter: that is more about comparative immeasurable security, people guess between security grade of economic agreements, and traditional banking vs bitcoin 23:48:10 the moment people run formally verified OS with formally verified clients for cryptocurrency, I think a shift would occur 23:48:22 So never. 23:48:37 Because formally verified OSes have gone nowhere. 23:48:40 since the listed implementations would then contain a formally verified system 23:48:52 Formally verified software in general has gone nowhere except in some very, very, very niche fields. 23:49:16 And part of that lies with the fact that formal verification is tedious, slow, painful, and unable to keep up with the ever-shifting demands of a market. 23:49:50 By the time you formally verified, say, a *ix kernel and its attendant device interfaces, you'd be 30 years behind the state of the art in hardware. 23:50:16 In the time it takes you to formally verify your kernel, there'd be USB 7.0 with a spec document that is larger than planet Earth. 23:50:17 ttmrichter: why verify a *ix kernel? I was hoping a forth environment 23:50:31 Doesn't matter what you verify. 23:50:47 By the time you verify it (with current tooling) you're about five generations behind. 23:51:10 wait, you seem to mean general NP problems 23:51:21 No, I mean the ever-shifting world of hardware and software. 23:51:22 I mean the programmer is also a mathematician 23:51:28 You'll always be behind the times. 23:51:45 (And, incidentally, I've seen the code produced by mathematicians. It's utter crap.) 23:52:09 I don't mind if my wallet is a bit out-dated, as long as I can have a different system for pr0n, games, ... 23:52:10 Do a search on "Cabal Hell" and you'll see one example among millions. 23:53:02 I have the impression you really hate mathematics in general? 23:53:28 things like physics as well? 23:54:06 No. 23:54:12 I quite liked physics. 23:54:29 I don't understand what physics without mathematics is? 23:54:30 I just gritted my teeth while I learned the maths necessary to learn and use physics. 23:54:33 Same with computing. 23:54:45 I gritted my teeth and learned the maths I needed to program. 23:54:54 But maths as a goal unto itself? Yeah. I despise it. 23:55:07 Maths is a necessary evil to me. 23:55:26 I may have to learn it. I do not enjoy the process, however, and I never forget that "evil" part of it. 23:56:44 ttmrichter: I am not advocating maths as a goal unto itself. remember when I said mathematicians and logicians currently in ivory tower? with proof checkers we can start expressing formal sentences with mundane meanings, and still be able to force adherents of a belief system to recognize presence of an inconsistency 23:57:13 this has the potential of merging belief systems 23:57:20 When proof checkers start being usable instead of outweighing actual working code 25:1 then they might catch on. 23:57:41 And when the proof checking process is taught by people who actually understand their fellow human beings. 23:57:53 Maths is one of the worst-taught disciplines in the academic world. 23:58:12 (And when you see how almost anything is taught in the academe, that's a damning statement!) 23:58:38 The seed for the hatred of maths in most people is planted long before they reach double-digits in age. 23:58:52 ttmrichter: one would not need to install the proofs along with the code, just check the proofs once 23:59:38 --- quit: chouser (Quit: Leaving.) 23:59:39 ttmrichter: you need like 0 maths to understand a proof checker, its practically substitution, it is only logic 23:59:55 And it's boring as shit. 23:59:59 --- log: ended forth/15.02.19