00:00:00 --- log: started forth/07.12.18 00:06:32 --- quit: maht_ (Read error: 110 (Connection timed out)) 00:54:33 --- join: ramkrsna (n=ramkrsna@unaffiliated/ramkrsna) joined #forth 01:11:10 --- quit: arke (":o") 02:39:27 --- quit: TreyB (calvino.freenode.net irc.freenode.net) 02:39:27 --- quit: lucca (calvino.freenode.net irc.freenode.net) 02:39:27 --- quit: rbarraud (calvino.freenode.net irc.freenode.net) 02:39:54 --- join: rbarraud (n=rbarraud@gateway.quickcircuit.co.nz) joined #forth 02:39:54 --- join: lucca (n=lucca@kuu.accela.net) joined #forth 02:39:54 --- join: TreyB (n=trey@cpe-66-87-192-27.tx.sprintbbd.net) joined #forth 03:09:38 --- join: ecraven (i=nex@eutyche.swe.uni-linz.ac.at) joined #forth 04:06:37 --- join: arke (n=arke@x415.vpn.hrz.tu-darmstadt.de) joined #forth 04:06:37 --- mode: ChanServ set +o arke 05:07:00 --- quit: ramkrsna ("Leaving") 05:21:10 --- join: tathi (n=josh@pdpc/supporter/bronze/tathi) joined #forth 05:21:10 --- mode: ChanServ set +o tathi 05:42:12 --- quit: ccfg (Remote closed the connection) 05:42:23 --- join: ccfg (n=pitkajus@tuomi.oulu.fi) joined #forth 06:04:30 --- quit: ygrek (Remote closed the connection) 07:09:56 --- quit: tathi ("leaving") 07:57:22 --- join: edrx (i=edrx@189.25.87.215) joined #forth 07:59:12 --- quit: tgunr () 08:09:33 --- quit: arke (Connection timed out) 08:21:02 --- join: tgunr (n=davec@70-41-240-186.cust.wildblue.net) joined #forth 09:00:57 --- part: edrx left #forth 10:02:38 --- quit: ecraven ("bbl") 10:04:21 --- join: yumehito (n=yumehito@b-internet.87.103.254.70.snt.ru) joined #forth 10:59:06 --- join: ygrek (i=user@gateway/tor/x-0be033a2e846e672) joined #forth 11:03:02 --- quit: nighty- ("Disappears in a puff of smoke") 11:03:14 --- join: nighty- (n=nighty-@66-163-28-100.ip.tor.radiant.net) joined #forth 12:00:34 --- quit: ygrek ("Leaving") 12:00:58 --- join: ygrek (i=user@gateway/tor/x-982c195b05d0ae1d) joined #forth 12:34:12 --- join: ecraven (i=nex@eutyche.swe.uni-linz.ac.at) joined #forth 13:37:22 --- join: arke (n=arke@p54A7CD63.dip.t-dialin.net) joined #forth 13:37:22 --- mode: ChanServ set +o arke 13:52:28 --- join: tathi (n=josh@pdpc/supporter/bronze/tathi) joined #forth 13:52:29 --- mode: ChanServ set +o tathi 14:06:02 --- join: doublec (n=doublec@202.0.36.64) joined #forth 14:32:43 --- quit: tgunr (Read error: 104 (Connection reset by peer)) 14:39:39 --- join: tgunr (n=davec@70-41-240-186.cust.wildblue.net) joined #forth 14:42:10 --- quit: tgunr (Connection reset by peer) 14:52:55 --- join: JoshGrams (n=josh@dsl-216-227-118-115.fairpoint.net) joined #forth 14:52:55 --- quit: tathi (Read error: 104 (Connection reset by peer)) 14:53:00 --- nick: JoshGrams -> tathi 14:53:01 --- mode: ChanServ set +o tathi 15:00:50 --- join: tgunr (n=davec@70-41-240-186.cust.wildblue.net) joined #forth 15:04:00 --- join: tgunr_ (n=davec@70-41-240-186.cust.wildblue.net) joined #forth 15:04:02 --- quit: tgunr (Connection reset by peer) 15:06:30 --- quit: tgunr_ (Connection reset by peer) 15:09:43 --- join: crest_ (n=crest@p5B10626E.dip.t-dialin.net) joined #forth 15:17:08 --- quit: Crest (Read error: 110 (Connection timed out)) 15:48:01 --- quit: doublec () 15:56:01 --- join: ziggurat (n=ziggurat@pool-71-164-227-62.dllstx.fios.verizon.net) joined #forth 16:15:46 --- join: tgunr_ (n=davec@70-41-240-186.cust.wildblue.net) joined #forth 16:22:37 Hey. 16:36:46 --- quit: ecraven ("bbl") 16:39:29 --- join: arke_ (n=arke@p54A7CD63.dip.t-dialin.net) joined #forth 16:51:29 --- quit: arke (Read error: 110 (Connection timed out)) 17:11:59 --- join: doublec (n=doublec@202.0.36.64) joined #forth 17:26:17 --- quit: tgunr_ (Read error: 104 (Connection reset by peer)) 17:28:31 --- quit: ziggurat ("This computer has gone to sleep") 17:32:30 --- quit: tathi ("leaving") 17:51:10 --- join: ziggurat (n=ziggurat@pool-71-164-227-62.dllstx.fios.verizon.net) joined #forth 18:02:17 --- quit: proteusguy (Read error: 104 (Connection reset by peer)) 18:03:50 --- join: starseeker (n=CY@ip72-218-17-237.hr.hr.cox.net) joined #forth 18:05:00 Hi all. Sorry if this is a silly question, but does anyone know of a Forth compiler that has been written using proof/verification techniques to be provably correct? 18:07:56 Not that I know of, but I'm interested in such research if you do find something 18:08:33 --- join: crest__ (n=crest@p5B10626E.dip.t-dialin.net) joined #forth 18:08:38 I'm pretty sure that similar but weaker stackmachine vm's have such formal methods available 18:10:09 kinda tricky searching, because of the english phrase "so forth" 18:11:20 most of what I see is more closely related to JVM research instead 18:11:55 starseeker: I suppose the main trickiness would be how handle non-compiled things like CODE/;CODE words 18:12:42 you'd either need two layers or consider only forths without those 18:13:25 There seems to have been some work done with scheme variations 18:14:19 I'm interested in the possibility of using a Forth environment to build a Lisp environment as a minimal path from machine language to Lisp 18:15:28 In theory, a verified Forth might be able to host a verified Lisp 18:16:15 --- quit: crest_ (Read error: 110 (Connection timed out)) 18:16:28 heh, the TUNES folks have been ranting about this for years 18:16:44 be sure Not to bring it up in #lisp, or you'll be flamed :p 18:17:11 Hehe 18:17:15 the approach there is generally to write everything in CL. nyef has had some success getting SBCL to run on bare hardware, for example 18:17:23 but that isn't provable in any way 18:17:40 as SBCL, while one of the best CL implementations, is a monster inside 18:17:47 That's what I've heard 18:18:06 Forth as a host for the first round Lisp compiler sounds a lot saner 18:18:23 * starseeker prefers not to translate anything as complex as sbcl directly to machine language... 18:18:30 maybe. Forth is technically a lot more than you need 18:18:38 Well, a Forth subset 18:18:56 Maybe some kind of Machine Forth rather than ANSI Forth 18:19:30 Forth seems like a very good minimalist path from machine to functional Turing complete interactive environment 18:19:34 well, it is a reasonable approach. You'd probably want to implement your GC in forth then 18:20:04 have you looked at Scheme48? it has an alternative approach you should at least examine first 18:20:10 :-) 18:20:15 That seems related to VLISP 18:20:21 Which caught my attention 18:20:44 there they define a subset of their language called TinyScheme, which they can compile directly to C with no gc needed; they then write the critical parts of their interpreter in that 18:20:51 but sadly it isn't a native-code implementation 18:20:51 --- join: proteusguy (n=proteusg@ppp-124.120.225.37.revip2.asianet.co.th) joined #forth 18:21:17 Yes. One of my design criteria would be starting with ONLY what the machine provides - no C compiler allowed 18:21:21 if you write a high-level compiler that then uses a GOOD forth implementation, you should be able to get excellent machine code out of it 18:22:10 How complex is a good Forth compiler? 18:22:44 depends on how many platforms it needs to work on, I imagine 18:22:57 I've not delved to far in that direction yet 18:23:05 others here have, and might be sources of better advice 18:23:32 there are a few reasonably fast, highly platform-independent forths with a variety of licenses and costs available 18:23:51 so you don't necessarily (and probably shouldn't) write your own unless you need to do so for security/proof reasons 18:24:11 I'm a bit torn in that respect. The Ultimate Goal would be a Computer Algebra System that delivers provably correct and trustworthy results, and to fully address the needs for that you have to go "all the way down" and make things not only correct but understandably correct 18:24:33 i understand the sentiment, but it's kinda rubbish 18:24:40 consider, you're Trusting the processor 18:24:47 Correct. 18:24:59 You trust either the processor or the human brain - both are hardware 18:25:07 but how was it designed? There are many bugs in processor design, and a long history of tragic failures there. 18:25:39 also, the line is a great deal more blurry now, as FPGA's are very cheap and popular, and most modern processors have re-programmable microcode 18:25:40 Indeed. So what must be done as the first step for the Forth layer is to define in logic the expected behavior of the machine instructions to be used, and set up tests for that behavior 18:26:19 is that necessary or useful? 18:26:44 For precise specification and verification of behaviors needed I had assumed it would be 18:26:50 I suppose this very quickly devolves into an epistemological debate :p 18:26:56 True :-) 18:27:27 I don't think you can completely prove the validity of a machine you are running within 18:27:43 No. 18:28:05 But you can define precisely what behaviors you are expecting 18:28:29 This can be done at a high level also 18:28:38 Correct - and it would need to be 18:28:42 sometimes a ridiculously high level, like Haskell, heh 18:29:12 All levels of the system would need rigorous specification, because each layer depends on the correct functioning of the layer below it 18:29:24 I'm not sure forth is your best approach for this 18:29:29 consider; it is untyped 18:29:32 As you correctly note, the hardware itself is somewhat intractable in the general solution, but it's better than nothing 18:29:44 --- join: tane`weq (n=tane@p5B15CDD4.dip.t-dialin.net) joined #forth 18:29:46 it is generally trivial to crash the vm 18:30:22 even if you restrict CODE words, the tendency is to manipulate pointers 18:30:44 the higher level languages you are talking about all use references (or similar) instead 18:31:06 Yes. Most work would be done at higher levels, but the foundation for those higher levels MUST be low level 18:31:08 You can prove code correct, however it is difficult 18:31:19 Indeed. 18:32:01 It may be as nutty as I've been told it is, but that doesn't make it less interesting (unfortunately) ;-) 18:32:32 * starseeker never seems to get interested in the easy stuff... :-( 18:34:16 The hope would be that once the proven code extends from the machine level to the high level needed for the mathematics, the system would be solid and only porting to new platforms would require the creation of new core behavioral code at the low level 18:35:28 Is the non-typed nature of Forth a serious hindrance for formal work? 18:37:17 Anyway, thanks much :-) 18:38:28 --- quit: ziggurat ("Leaving") 18:47:22 --- quit: tane (Read error: 101 (Network is unreachable)) 19:17:12 --- join: arke (n=arke@p54A7CA25.dip.t-dialin.net) joined #forth 19:17:12 --- mode: ChanServ set +o arke 19:28:57 --- join: doublec_ (n=doublec@202.0.36.64) joined #forth 19:34:10 --- quit: arke_ (Connection timed out) 19:44:49 --- quit: doublec (Read error: 110 (Connection timed out)) 19:49:58 --- join: nighty^ (n=nighty@sushi.rural-networks.com) joined #forth 19:50:35 --- quit: doublec_ () 20:46:01 --- join: ramkrsna (n=ramkrsna@unaffiliated/ramkrsna) joined #forth 21:26:23 --- join: Al2O3 (n=Al2O3@c-75-70-5-69.hsd1.co.comcast.net) joined #forth 22:32:25 --- quit: nighty^ ("Disappears in a puff of smoke") 22:46:35 --- join: yumehito_ (n=yumehito@b-internet.87.103.254.70.snt.ru) joined #forth 22:54:34 --- quit: yumehito_ (Remote closed the connection) 22:55:58 --- join: yumehito_ (n=yumehito@b-internet.87.103.254.70.snt.ru) joined #forth 22:57:46 --- quit: yumehito (Read error: 110 (Connection timed out)) 23:00:03 --- quit: yumehito_ (Remote closed the connection) 23:23:22 --- join: Baughn_ (n=svein@084202038064.customer.alfanett.no) joined #forth 23:29:37 --- quit: Baughn (Connection reset by peer) 23:35:20 --- quit: ygrek (Remote closed the connection) 23:59:59 --- log: ended forth/07.12.18