IRC log started Sun Mar 5 00:00:00 2000 [msg(TUNES)] permlog 2000.0305 12:10am -:- _ruiner_ [DIY@ppp117.wi.centurytel.net] has joined #tunes -:- SignOff _ruiner_: #TUNES (destroy what destroys you) -:- SignOff air: #TUNES (http://www.qzx.com/ :: sleep) -:- smoke [smoke@15dyn134.delft.casema.net] has joined #tunes -:- eihrul [lee@usr5-ppp44.lvdi.net] has joined #tunes -:- lar1 [larman@1Cust196.tnt26.sfo3.da.uu.net] has joined #tunes Guten tag! -:- AlonzoTG [Alonzo@216-164-135-248.s629.tnt4.lnhva.md.dialup.rcn.com] has joined #tunes 09:40am -:- SignOff smoke: #TUNES (One day sheep will rule the world) -:- smoke [smoke@15dyn134.delft.casema.net] has joined #tunes -:- tcn [r@cci-209150250130.clarityconnect.net] has joined #tunes -:- Fufie [stig@129.177.44.38] has joined #tunes -:- SignOff AlonzoTG: #TUNES (Have Nice Day :)) -:- hcf [nef@me-portland-us842.javanet.com] has joined #tunes yay, tunes-cvs@ got spammed spammed? how? why? who? :) From: Date: Sun, 5 Mar 2000 07:39:08 Subject: AD:Family Reunion T Shirts & More 12:20pm hmm, how appropriate that it gets sent to tunes-cvs heh.. how many people actually subscribed to that? tcn: 8 you never know when the cvs repository is going to have a get together with older source branches and versions... what source branches? 12:30pm * tcn/#tunes wonders why anyone sends spam still.. are there really enough morons to buy the shit? Must be... 12:40pm -:- SignOff Fufie: #TUNES (afk for a few days) tcn: no, there are only morons who buy a spamming package :) smoke: oh yeah :) Most of the spam is advertising for spamming software/services 12:50pm BBL -:- SignOff lar1: #TUNES (Leaving) Any interest in programming TUNES in earnest? 01:00pm i'd love to help, but lack initiative to start on something that is, i have lots of other projects to attend to, and can't bear another big project. yeah -:- SignOff tcn: #TUNES (Ping timeout for tcn[cci-209150250130.clarityconnect.net]) -:- tcn [r@cci-209150250055.clarityconnect.net] has joined #tunes as I was saying 01:10pm I don't expect much progress on Tunes without more involvement from Fare.. he's the visionary, and he knows what he's doing.. most of the other people have a lot to learn. or they have their own projects :) i'd say a common goal wouldn't harm the tunes project hehe oh I'm saying this because of a discussion on comp.lang.forth some talk about virtual memory being inefficient, and how all that is unnecessary with security-by-proof TUnesy stuff I should be saying this to tunes@tunes.org 01:20pm -:- SignOff hcf: #TUNES (Ping timeout for hcf[me-portland-us842.javanet.com]) this is being logged. by security-by-proof you mean strict typing ? -:- hcf [nef@me-portland-us842.javanet.com] has joined #tunes -:- air [brand@p0wer.qzx.com] has joined #tunes maybe it could be done without typing... 01:30pm I hate types... they just complicate things. every proof about programs is typing can Forth programs be proofed? well, types are there, whether you hate them or not in forth? -:- AlonzoTG [Alonzo@216-164-138-135.s135.tnt5.lnhva.md.dialup.rcn.com] has joined #tunes tcn: sure so a forth program can be proved by inferencing types? or could it be simpler, like forth itself? yes, and using combinatory logic 01:40pm -:- SignOff smoke: #TUNES (Ping timeout for smoke[15dyn134.delft.casema.net]) -:- NetSplit: irc.linux.com split from lewis.openprojects.net [01:47pm] -:- BitchX+Deb1an: Press Ctrl-F to see who left Ctrl-E to change to [irc.linux.com] -:- Netjoined: irc.linux.com lewis.openprojects.net -:- smkl [sami@glubimox.yok.utu.fi] has joined #tunes -:- Plundis [plundis@130.238.23.252] has joined #tunes -:- abi [nef@bespin.dhs.org] has joined #tunes -:- eihrul [lee@usr5-ppp44.lvdi.net] has joined #tunes -:- tcn [r@cci-209150250055.clarityconnect.net] has joined #tunes -:- hcf [nef@me-portland-us842.javanet.com] has joined #tunes -:- air [brand@p0wer.qzx.com] has joined #tunes -:- AlonzoTG [Alonzo@216-164-138-135.s135.tnt5.lnhva.md.dialup.rcn.com] has joined #tunes -:- smoke [smoke@16dyn188.delft.casema.net] has joined #tunes re wb tcn: are you a `tunes member' ? :) excuse my ignorance, i'm only a learner -:- SignOff hcf: #TUNES (Ping timeout for hcf[me-portland-us842.javanet.com]) -:- hcf [nef@me-portland-us842.javanet.com] has joined #tunes smoke: yeah, I joined in '98 that makes me a newbie :) tcn: what are your interests ? 02:10pm my computing interests? * AlonzoTG/#tunes left clicks on tcn windows lamer! ;) I thought you only used DOS tcn: yes ah i ping-timeouted before this came through: i've had some discussion with my topology prof on typing, but he didn't see much fun in them then again, math proof is something else than automatic program proof smoke: i'm a pragmatist.. i'm big on simplification.. For awhile I thought automatic proof was _more_ complication.. but if it eliminates the need for hardware-level protection and the software to deal with it.. it would simplify things.. 'course, I could always do without protection 02:20pm hehe.. run crappy/untrusted programs with runtime protection, good stuff with no protection i'm having trouble picking the best language from Common Lisp and Haskell i had the impression that the biggest difference was in the typing system om It is practically impossible to ensure that nontrivial programs have no bugs. 02:30pm alonzo: using decent typing would eliminate at least a few alonzo: or at least, that's what the gurus say :) hehe i really couldn't tell myself. if we can ensure that one program won't step on another, that's good enough tcn: what do you mean by that ? talx86 can ensure that already om.... well I have a problem when programming... I mean when I write stuff it's just a string of numbers.... what's talx86? When one program spews out a string of numbers, how does all of this fancy "typing" mumbo jumbo get transferred to the recipient? I don't think it can happen... =P abi: tal? tal is typed assembly language at http://www.cs.cornell.edu/talc/default.html hmm.. lots of proof systems work going on at Cornell alonzo: i think it's impossible to proof the logical corectness of a program alonzo: ie - proving that it does what it should according to the author couldn't be automated (correct me if i'm wrong, i'd be surprised) it is possible to proof every feature of a program, but very hard to do that automatically 02:40pm smoke: Godel proved that :) it would be infinitely difficult tcn: what proof would that be ? to proof any program would be impossible i mean if you want a program to display a happy smiling face, it'd be insane to go proof if the face looks happy or no :) for example it is quite easy to prove that a sorting program is correct He (mathematically) proved the impossibility of proving any program smkl: how would you proof that automatically ? tcn: that would contradict what smkl is about to say (?) with curry-howard isomorphism ... it's probably proovable that it wouldn't interfere with other programs in the system. * tcn/#tunes nods smkl: then you'd compare it to another sorting algorithm? there doesn't exist an axiom set that is complete and there exists a proof checking or making (which one) algorithm ? smoke: nope, you would compare it with specification of sorting tcn: are you referring to the same theorem which states that not everything of a (well enough) system can be proved in itself ? smoke: I think so.. the famous "Godel's theorem" tcn: well then, there could be programming languages which are less powerful than the systems godel described tcn: it's doubtful if they would be of any use though :)) I think Church and Turing independently proved the same hting hmm now we're confused :) * smoke/#tunes would really like to understand godels proof.. i wonder how many years from now i get it :) smoke: Java is a 'secure' language that trades usefulness for security gödels theorem means that there can't exist a type system that can be used to make proofs about every possible program tcn: i suppose java is way more powerful then the minimal system yes, I believe java is "sufficiently powerfull" Godel's theorem seems sorta philosophical... it says to me "math and science will never replace art" =) church and turing thesis is that the expressive power of turing machine and lambda calculus are equal and complete and there can't be a type system for them tcn: oh i don't like those implications. I do tcn: godel only proved something about very specific systems. -:- SignOff hcf: #TUNES (Ping timeout for hcf[me-portland-us842.javanet.com]) well he used specific systems but his proof was general. 02:50pm tcn: given another (fundamentally different) logic, you may want to derive different philosophical thoughts -:- hcf [nef@me-portland-us842.javanet.com] has joined #tunes it hasn't been proven that godel was universally right ;) hehe but that logic would have the same kinds of limitations as any other. are we having fun yet? alonzo: why? it's the nature of formal systems. I am attempting to define and describe an "informal system" on my website. =) haha alonzo: i meant something we don't understand as logic. alonzo: imagine how really weird aliens living upside down and inside out all day would reason (especially the inside out is important :-0 well as you can see i'm getting tired and should get some sleep now. thanks for the interesting discussion :) would they have numbers? smkl: only 3 probably any form of reason would have the same limitations. -:- SignOff smoke: #TUNES (z) man, I finally found a subject that I can debate and now he leaves. =P heh well, it would be sorta hard to make godel numbers if you only had 3 yep. Godel numbering still escapes me... =\ gonna hafto get more hofstadter. -:- SignOff AlonzoTG: #TUNES (Have Nice Day :)) but perhaps there is some other way to reason about recursion and self ref now he leaves :) 03:00pm -:- SignOff hcf: #TUNES (Leaving) -:- SignOff tcn: #TUNES (ircII EPIC4pre2 cLIeNUX. Can you say that?) -:- AlonzoTG [Alonzo@216-164-138-36.s36.tnt5.lnhva.md.dialup.rcn.com] has joined #tunes -:- future [xdef@mfd-dial2-5.cybercom.net] has joined #tunes -:- future is now known as present -:- rares [rares@wtrb-sh8-port186.snet.net] has joined #tunes -:- rares [rares@wtrb-sh8-port186.snet.net] has left #tunes [Segmentation] -:- SignOff eihrul: #TUNES (Ping timeout for eihrul[usr5-ppp44.lvdi.net]) -:- eihrul [lee@usr5-ppp20.lvdi.net] has joined #tunes -:- NetSplit: tolkien.openprojects.net split from varley.openprojects.net [05:59pm] -:- BitchX+Deb1an: Press Ctrl-F to see who left Ctrl-E to change to [tolkien.openprojects.net] -:- Netjoined: tolkien.openprojects.net varley.openprojects.net -:- air [brand@p0wer.qzx.com] has joined #tunes -:- SignOff eihrul: #TUNES (Read error to eihrul[usr5-ppp20.lvdi.net]: EOF from client) -:- eihrul [lee@usr5-ppp20.lvdi.net] has joined #tunes -:- SignOff AlonzoTG: #TUNES (Ping timeout for AlonzoTG[216-164-138-36.s36.tnt5.lnhva.md.dialup.rcn.com]) -:- AlonzoTG [Alonzo@216-164-138-36.s36.tnt5.lnhva.md.dialup.rcn.com] has joined #tunes hmm * AlonzoTG/#tunes left clicks on eihrul -:- linkos [linkos@gemini.truserve.com] has joined #tunes * AlonzoTG/#tunes greets "Salutations linkos!" :-) 06:40pm -:- SignOff eihrul: #TUNES (Read error to eihrul[usr5-ppp20.lvdi.net]: EOF from client) -:- eihrul [lee@216.24.141.20] has joined #tunes -:- lar1 [larman@dialup-209.245.136.108.SanJose1.Level3.net] has joined #tunes -:- linkos [linkos@gemini.truserve.com] has left #tunes [] -:- witten [witten@un.torsion.org] has joined #tunes -:- SignOff eihrul: #TUNES ([x]chat) -:- future [xdef@209-6-184-165.c3-0.wth-ubr1.sbo-wth.ma.cable.rcn.com] has joined #tunes -:- SignOff present: #TUNES (Ping timeout for present[mfd-dial2-5.cybercom.net]) -:- witten [witten@un.torsion.org] has left #tunes [] -:- SignOff lar1: #TUNES (Read error to lar1[dialup-209.245.136.108.SanJose1.Level3.net]: Connection reset by peer) -:- lar1 [larman@dialup-209.245.128.210.SanJose1.Level3.net] has joined #tunes * AlonzoTG/#tunes just posted to the list. =P whats happening 08:50pm * AlonzoTG/#tunes greets "Salutations future!" :-) -:- _1BadDude [Alonzo@216-164-138-36.s36.tnt5.lnhva.md.dialup.rcn.com] has joined #tunes <_1BadDude> =\ -:- SignOff AlonzoTG: #TUNES (Ping timeout for AlonzoTG[216-164-138-36.s36.tnt5.lnhva.md.dialup.rcn.com]) <_1BadDude> It was the server!!! <_1BadDude> =P ?!@# hey 1baddude ur on rcn i see it was down all day for me tech support said thus: 'they were doing some maintenance, and when they tried to reboot, it wouldn't boot' uhhuh Heh 09:00pm <_1BadDude> it came up at 1:00 PM here... <_1BadDude> the fuckers should have done it incrementally. <_1BadDude> =\ done what? an incremental screw-up? brb, im gonna see if my cablemodem works now -:- SignOff future: #TUNES (Read error to future[209-6-184-165.c3-0.wth-ubr1.sbo-wth.ma.cable.rcn.com]: EOF from client) 09:10pm -:- SignOff _1BadDude: #TUNES (Have Nice Day :)) -:- SignOff lar1: #TUNES (Leaving) -:- smoke [smoke@16dyn188.delft.casema.net] has joined #tunes [msg(TUNES)] newlog 2000.0306 IRC log ended Mon Mar 6 00:00:02 2000