00:00:00 --- log: started retro/10.10.17 09:19:34 good afternoon 09:36:37 hi crc 09:52:36 http://singinst.org/research/researchareas 09:52:55 * Programming Languages that Combine Efficiency with Provability of Program Correctness. In the interest of AGI safety, it would be desirable if our AGI software programs could be proved to correctly implement the software designs they represent. However, currently, there is no programming language that both supports proof-based program correctness checking, and is sufficiently efficient in terms of execution to be usable for pragmatic AGI pur 09:53:44 I'm not sure how to begin to tackle that one. 09:57:27 Small, well-factored words seem like a good start. 09:59:43 there was a guy in #forth a couple years back looking to adapt forth into a provable language 10:01:22 hmm. how does provability work? what does it entail? 10:05:03 generally, formal mathmatical proofs IIRC 10:05:40 there's some discussion from 2000 at http://www.advogato.org/article/120.html 10:12:38 http://www.c2.com/cgi/wiki?UnitTest is interesting 10:28:45 I've never done anything significant with unit tests; though toka did have a test set that was useful in catching a couple of bugs 10:30:17 it seems they could be useful when you have a really big project with many people contributing. 10:58:58 http://www.freepatentsonline.com/7243086.html looks interesting 11:00:35 * docl realizes that reading patents would be a great form of mental exercise... 11:01:39 docl: i guess it just depends on what patents you read, it could also destroy your brains! 11:01:49 :) 11:02:15 patents and scientific papers seem to me to be written in something vaguely english-like, but not english. 11:02:34 I suppose they are simply above my grade-level, so to speak. 11:03:00 i was writing a paper just now :) 11:03:16 cool, what on? 11:04:03 foucist: you might be interested in the patent as it involves evolutionary computation (or so my cursory skimming tells me) 11:04:05 "Influence of strain rate and near-to-room temperatures on tensile properties of Ti-6Al-4V" 11:04:35 cool, materials science 11:04:44 yep 11:06:39 * docl googles, finds wikipedia on Titanium Alloy 11:07:49 ok, now I see the numbers mean 6% aluminum, 4% vanadium. 11:09:11 Grade 5, most commonly used alloy 11:09:27 looks like some pretty interesting stuff. 11:11:20 it is very common. normally when you hear something is made os titanium is in fact ti64 11:11:30 makes sense 11:17:08 strain rate would be how quickly the strain is applied? 11:17:30 yes 11:19:34 how do you test that? you have a machine that yanks on it at various speeds, and see at what point it breaks? 11:30:49 so... to make provably correct code, you start with a specification and a program. then you randomly mutate it and select the descendants that formally prove to match the closest to the specification. 12:01:49 --- quit: yiyus_ (Remote host closed the connection) 12:47:09 --- join: yiyus_ (1242712427@je.je.je) joined #retro 13:36:10 * crc has been sick; if this fever won't break soon I may have to go to the doctor :( 13:37:32 yikes, that sounds bad 13:40:41 my temperature was 105.9 this morning; still at 101 after six tylenol, and several hours of rest. It stayed around 102 friday and saturday. 16:49:11 crc: ouch, pretty bad, 3 days is a pretty long time 16:49:19 hope you get well soon 16:49:55 just sleep a shitload and drink gingerale or watered down pop or something 16:50:20 that's pretyt much all i do when i have a fever 16:51:10 docl: imo, i don't consider that style of writing to be "above" your grade-level, but rather, below it 16:52:02 the writers are deliberately doing that for a couple reasons, for obfuscation purposes and to appear more professional 17:06:03 hmm. 17:06:24 deliberate obfuscation? 17:09:10 Well it seems like an analog to math. I know math makes sense to a mathematician. And when I study it hard enough, it makes sense to me (or in theory would if I did). But it doesn't exactly leap off the page at me. 17:09:54 Yet, if the mathematicians stuck to english descriptions, I don't think they would get nearly as much done. 17:14:37 Are patent lawyers in a similar situation? 17:15:23 Their goal is protecting their client by describing the invention in a way such that noone else can later claim to have invented it. 17:16:00 hence we get language like: ' 17:16:04 While this invention has been described in conjunction with the exemplary embodiments outlined above, various alternatives, modifications, variations, improvements, and/or substantial equivalents, whether known or that are or may be presently unforeseen, may become apparent to those having at least ordinary skill in the art. Accordingly, the exemplary embodiments of the invention, as set forth above, are intended to be illustrative, not limiting. V 17:23:07 It's truly maddening to have to read such stuff. But it works for the purpose it was designed for, which wasn't to describe the invention but to defend the inventor's legal interests. 17:23:20 I assume scientific papers are unreadable for similar reasons. 17:24:44 i.e. there are matters of prestige, and unimaginative competitors who would not respect the idea if it were worded more simply and straightforwardly. 17:27:44 So the casual reader who might be tempted to make some stupid criticism is warded off by being too daunted to read through the paper. The reader who does read and understand either agrees or has a very serious critique. 17:29:07 * docl is partly venting at people who clearly don't understand, yet feel qualified to criticize cryonics, despite the variety of accessible and easy to read explanations of exactly what you need to know on the topic. 17:30:09 actually, it could be that the existence of idiot-accessible literature *really* makes matters worse by inviting idiots to criticize a thing :p 17:31:43 (No, that's dark side thinking. Bad docl!) 17:33:04 foucist: you've read about the dunning-krueger effect? http://en.wikipedia.org/wiki/Dunning%E2%80%93Kruger_effect 17:40:17 Not that I like software patents or anything. 18:46:20 docl: i would expect the vast majority of people are completely unaware of cryonics and think it's a scifi thing :P 18:48:20 docl: just sell it as "death insurance" and people will buy it 18:48:32 use familiar terms like that instead of 'cryonics' :P 18:52:31 haha 18:53:12 srsly 18:53:20 <- marketer 18:54:40 :) 19:20:30 http://gist.github.com/631552 some notes on the combinators 20:31:16 crc: looks interesting 22:35:57 --- join: ncv (~neceve@unaffiliated/neceve) joined #retro 23:59:59 --- log: ended retro/10.10.17