| 00:10.21 | *** join/#utah olli (~olli@c-71-195-232-74.hsd1.ut.comcast.net) |
| 00:36.53 | *** join/#utah kendsnyder (~kendsnyde@65-100-194-109.slkc.qwest.net) |
| 01:32.52 | *** join/#utah Sargun_Screen (~sargun@atarack/Staff/Sargun) |
| 01:34.10 | *** join/#utah davad (~davad@c-98-202-243-63.hsd1.ut.comcast.net) |
| 01:36.03 | *** join/#utah VanHelsing (~vanhelsin@97-126-220-20.slkc.qwest.net) |
| 01:40.07 | *** join/#utah davad (~davad@98.202.243.63) |
| 03:29.29 | *** join/#utah jnbek (~jnbek@pdpc/supporter/active/jnbek) |
| 03:39.22 | *** join/#utah olli (~olli@c-71-195-232-74.hsd1.ut.comcast.net) |
| 04:01.23 | *** join/#utah olli (~olli@c-71-195-232-74.hsd1.ut.comcast.net) |
| 04:41.01 | *** join/#utah dfinn (~Adium@c-67-186-246-200.hsd1.ut.comcast.net) |
| 04:44.21 | *** join/#utah olli (~olli@c-71-195-232-74.hsd1.ut.comcast.net) |
| 05:05.17 | *** join/#utah jalbretsen (~jalbretse@c-174-52-67-72.hsd1.ut.comcast.net) |
| 05:57.25 | *** join/#utah TodPunk (~Tod@50-198-177-185-static.hfc.comcastbusiness.net) |
| 06:17.11 | *** join/#utah b4dave_4 (~smuxi@71-35-235-211.slkc.qwest.net) |
| 12:13.41 | *** join/#utah emcnabb (emcnabb@nat/redhat/x-yxwypzkacuzruqth) |
| 12:13.42 | *** mode/#utah [+v emcnabb] by ChanServ |
| 12:35.59 | *** join/#utah jsmith (~jsmith@fedora/jsmith) |
| 12:56.55 | *** join/#utah olli_ (~olli@c-71-195-232-74.hsd1.ut.comcast.net) |
| 13:15.51 | *** join/#utah pdayton (~pjdayton@208.54.5.229) |
| 13:48.31 | *** join/#utah kendsnyder (~kendsnyde@65-100-194-109.slkc.qwest.net) |
| 14:03.13 | *** join/#utah pdayton (~pjdayton@67.21.63.152) |
| 14:06.53 | *** join/#utah bgerber (~gerberb@suse103.mwiap.com) |
| 14:15.00 | *** join/#utah macnewbold (~macnewbol@c-98-202-181-28.hsd1.ut.comcast.net) |
| 14:15.06 | *** join/#utah TimRiker (~TimRiker@bzflag/projectlead/TimRiker) |
| 14:15.06 | *** mode/#utah [+o TimRiker] by ChanServ |
| 14:17.41 | *** join/#utah mrpull (~jpollmann@216.51.56.98) |
| 14:19.25 | *** join/#utah opapo (~quassel@204.113.97.235) |
| 14:40.52 | *** join/#utah macnewbold (~macnewbol@66.219.204.99.provo.dynamic.broadweavenetworks.net) |
| 14:41.45 | *** join/#utah jalbretsen (~jalbretse@sonic.itransact.com) |
| 14:44.52 | *** join/#utah smcquay (~smcquay@17.193.12.131) |
| 14:45.30 | *** join/#utah kendsnyder (~kendsnyde@67.214.245.39) |
| 14:56.14 | *** join/#utah tiwula (~lane@70.89.246.241-Busname-UT.hfc.comcastbusiness.net) |
| 15:29.44 | *** join/#utah kendsnyder (~kendsnyde@67.214.245.39) |
| 15:31.04 | *** join/#utah emcnabb (emcnabb@nat/redhat/x-apsoxesrkuvrjjbr) |
| 15:31.05 | *** mode/#utah [+v emcnabb] by ChanServ |
| 15:41.41 | *** join/#utah undertakingyou (~undertaki@danix.eaerich.com) |
| 15:55.17 | *** join/#utah tiwula (~lane@70.89.246.241-Busname-UT.hfc.comcastbusiness.net) |
| 16:12.11 | *** join/#utah NoCoolName_Tom (~NoCoolNam@64.124.34.2) |
| 16:17.16 | levi | Interviewers don't always try to demonstrate their intellectual superiority, but they often try to figure out the limits of what you know. |
| 16:42.22 | ldav15 | <PROTECTED> |
| 16:42.48 | skrike | "People are going to misquote me on the internet." --Socrates |
| 16:43.28 | ldav15 | Probably |
| 16:47.53 | skrike | http://i.imgur.com/ZTXWGpS.jpg |
| 16:50.20 | Migs | hahaha |
| 16:50.21 | *** join/#utah NoCoolName_Tom (~NoCoolNam@64.124.34.2) |
| 16:57.47 | *** join/#utah VanHelsing (~vanhelsin@97-126-220-20.slkc.qwest.net) |
| 16:58.45 | *** join/#utah SunSparc (~jonathan@69-27-175-74.acedatacenter.com) |
| 17:07.57 | *** join/#utah redbeard2 (~jphall@63.230.12.160) |
| 17:08.15 | *** part/#utah redbeard2 (~jphall@63.230.12.160) |
| 17:12.46 | youtah | Do I dare mention *anything* regarding the Zimmerman Trial? |
| 17:13.06 | romanovic | ~censor youtah |
| 17:13.08 | jlp_znc | oh, you dare |
| 17:13.25 | youtah | lol |
| 17:22.05 | levi | So, it's kind of funny. I've been looking into the BLISS language, which was a DEC systems programming language that was somewhat popular on PDP computers until Unix and C came around, and mostly what people think is notable about it is that all variable references evaluated as storage locations rather than the values at those locations. That's definitely interesting, but it seems the really cool part is not talked about much: It's got |
| 17:22.05 | levi | a method of separately specifying the storage format/accessors of a data structure and its semantics. |
| 17:30.15 | levi | So, if you need an array with a specific kind of memory layout, you just code the row/column accessors for it appropriately, and there you go. Your algorithm using the data structure stays the same. |
| 17:31.26 | levi | It also had a symmetric coroutine feature, which would allow you to create a new stack at a given storage location for a given function, and later you could exchange active stacks. |
| 17:39.42 | errstr | isn't that how coroutines are typically implemented? a function copies the stack/environment and yields control to another portion of the program, when it is invoked again, the stack at the earlier point is recovered? |
| 17:41.01 | errstr | at least that's how i've understood how coroutine/cps/generators were always implemented |
| 17:44.45 | errstr | well, to be fair, you can optimize memory usage by only storing the deltas for the continuation to rehydrate the stack. but, the concept is still the same. |
| 17:46.28 | *** join/#utah opapo (~quassel@204.113.97.235) |
| 17:59.02 | jxqz | levi: so you make an abstract algorithm for any kind of uniform input data? |
| 17:59.31 | jxqz | that seems like it's going to have limitations on any algorithm that expects certain features of the data |
| 17:59.36 | levi | Yes, that's precisely how they're typically implemented. But most languages at the C level don't support any transfer of control at the procedure level aside from the standard function call. |
| 17:59.53 | youtah | Fixed: <jxqz> levi: so you make an abstract algorithm for any kind of unicorn input data? |
| 18:00.06 | jxqz | youtah: candycorn data |
| 18:00.24 | youtah | lol, so I actually read Unicorn the first time, Had to go back and take a second glance |
| 18:01.32 | levi | Data structures are accessed through a uniform kind of expression. It looks like an array dereference, but you can have multiple comma-separated parameters inside the brackets. You get to control, in the structure definition, how those parameters are combined to yield the storage location of a particular structure element. |
| 18:02.49 | jxqz | interesting |
| 18:03.57 | jxqz | does that make a structure in BLISS somewhat like a class in C++? |
| 18:04.39 | levi | More like a struct with getter/setter parameters that are implicitly called by dereferencing a struct member. |
| 18:04.57 | jxqz | yes |
| 18:05.27 | levi | Also kind of like the getf/setf functionality in Common Lisp. |
| 18:06.47 | levi | It has always irked me that C has really weak data structure facilities. It's often, at the OS level, critical to have precise control over the memory layout of structures, and C doesn't give you that outside of compiler-specific extensions. |
| 18:07.54 | jxqz | *strong* types |
| 18:07.55 | jxqz | ! |
| 18:08.06 | levi | No, I'm not talking about types at all. |
| 18:08.07 | jxqz | just have that going through my mind right now |
| 18:08.24 | levi | BLISS is completely type-less, in fact. |
| 18:08.30 | jxqz | indeed |
| 18:08.56 | jxqz | but the notion of typing is central to computer theory |
| 18:09.04 | jxqz | why? |
| 18:10.06 | Gate_ | levi: solution: duck typing..... oh wait ;) |
| 18:11.09 | Gate_ | levi: you can have precise control of memory layout of structures if you choose it. |
| 18:11.12 | levi | Because static type systems correspond to correctness properties of the programs, and that's an interesting thing to research. |
| 18:12.36 | jxqz | that levi, always having the answers |
| 18:12.57 | levi | Gate_: Not without some combination of awkward code or non-standard language extensions. |
| 18:14.04 | Gate | levi: what control are you looking for that you don't have? My C might be a bit rusty, but as I recall struct definition is both precise and predictable. How you construct it determines its exact storage layout |
| 18:14.58 | levi | Gate: The compiler may introduce padding between struct fields in the storage layout. This is predictable on a per-compiler basis, but not specified by the programmer or language standard. |
| 18:15.03 | Gate | Or are you trying to control dynamically sized types such as strings that you want inline with the rest of the memory? |
| 18:15.21 | Gate | I see what you mean, then. |
| 18:16.11 | Gate | I used to miss C. Then I realized I didn't. |
| 18:16.16 | levi | Also, C bitfields are near-useless. |
| 18:16.34 | levi | At least if you care *which* bits are being used. |
| 18:17.28 | *** join/#utah pdayton (~pjdayton@67.21.63.152) |
| 18:17.39 | fugue88 | Predictable on a per-compiler [and per-architecture] basis. |
| 18:18.32 | fugue88 | For example, even if you stick with gcc, going from x86-32 to x86-64, your structs could pack differently because of the different word size. |
| 18:19.00 | levi | The fact that you have to do manual bitmasking and shifting operations to get at bitfields is incredibly annoying, and has led to a profusion of different idioms for doing it that all have different interfaces. |
| 18:20.20 | levi | C is a terrible language; it's roughly applicable to a wide field of applications, but it's not actually *good* for any of them. |
| 18:26.16 | levi | Somewhere in C++ there's an efficient and clean systems programming language just begging to be set free, but it somehow manages to be *worse* than C in some respects. |
| 18:31.59 | jlp_znc | levi: regarding your statement about "have to do manual bitmasking and shifting operations", that's also one of the strengths of C. I once had to implement a data storage layer where the underlying storage could contain numeric (long, short, and floating point) data in various formats (i.e. different endianness, DECFLOAT vs. IEEE) and being able to access the bits directly made it possible. Never could have done that in Pascal in a million years |
| 18:32.52 | levi | Anyway, over the weekend I started working through Benjamin Pierce's textbook 'Software Foundations', which covers the semantics of programming languages, including type systems, via the Coq interactive proof system. It's pretty neat stuff. |
| 18:32.59 | *** join/#utah kim27 (~kim27@host-166.arcadia-srv-216-83-132.fiber.net) |
| 18:33.52 | errstr | i loved his "Types and Programming Languages" book |
| 18:34.01 | levi | jlp_znc: Depends on the Pascal you used. I'm pretty sure you could do bitmasking and shifting in many Pascals. But that's just saying Pascal is at most equally bad as C at accessing arbitrary bitfields. |
| 18:34.55 | levi | errstr: I've read through a good bit of that as well, but the advantage of Software Foundations is that you can work through the proof exercises and be sure you got them right. |
| 18:35.33 | errstr | there's nothing stopping you from opening up ghci and verifying the math behind the lambda calculus |
| 18:36.14 | levi | Running some tests is not the same thing as doing the proof exercises in the book. |
| 18:36.45 | jxqz | is always jealous of what levi does |
| 18:37.09 | levi | And Coq is essentially a dependently-typed functional programming language, not too unlike Haskell except with a more powerful type system, along with some added layers to help you build proofs with it. |
| 18:37.42 | levi | So... 'opening ghci and veryfing the math behind the lambda calculus' is more or less what you do with Software Foundations. |
| 18:38.02 | errstr | sure, coq and agda are both super strongly typed languages, but haskell's typing system is strong enough to ensure that your math is correct |
| 18:38.02 | levi | The entire book is a literate Coq script. |
| 18:38.13 | errstr | that's interesting |
| 18:38.39 | jxqz | mathematica makes you feel impressed by doing stuff like that |
| 18:38.54 | jxqz | 'just put the text in comments!' 'that's so amazing!' |
| 18:39.15 | levi | Haskell's type system is fine for verifying the correctness of Haskell programs, insomuch as you can encode interesting properties of your program at the type level, but not for understanding the math *behind* the type system. |
| 18:40.51 | levi | Writing a Haskell program is decidedly not the same thing as proving that the new type system you devised for your language is sound. |
| 18:41.59 | errstr | category/order theory math translates directly to haskell, in fact it looks almost exactly the same expressed on paper as it does in haskell. i disagree that you can't express type systems and ensure their correctness within haskell. |
| 18:41.59 | levi | If you look at the exercises in the Types and Programming Languages book, the vast majority of them ask you to prove some property of whatever language you're working with at the moment, which is not going to happen in ghci, though ghci might help you with the intuition on how to approach the proof. |
| 18:42.20 | errstr | i'm definitely not arguing that agda/coq aren't better suited |
| 18:42.30 | levi | You can implement a type checking algorithm in Haskell just fine. |
| 18:44.03 | levi | errstr: I suppose I should ask if you actually worked through the proof exercises in TaPL in the manner in which you're suggesting? |
| 18:45.03 | errstr | no, it's written in ocaml which uses the an ML-like type system like haskell |
| 18:45.34 | levi | So I'm at a loss as to why you're suggesting that *I* could do the exercises that way. |
| 18:46.40 | errstr | not suggesting that at all, i was just making a comment about using haskell as a correctness checker |
| 18:46.46 | *** join/#utah pashdown (freenode@166.70.135.175) |
| 18:47.11 | errstr | i found it invaluable with my thesis |
| 18:47.38 | levi | What properties of correctness were you checking in that case? |
| 18:47.53 | errstr | since i implemented my interpreter for dalvik in a non-typed language: Racket, i found bugs in my math->code using haskell, and found it great at checking correctness |
| 18:48.16 | levi | I guess you did this in the days before typed-racket? |
| 18:48.49 | errstr | no, typed-racket was around, but i used just plain racket. haskell was for proving my galois connections |
| 18:49.04 | errstr | from concrete to abstract semantics |
| 18:49.31 | levi | Well, that's pretty cool, and I have no doubt that Haskell was an effective tool for that. |
| 18:49.43 | errstr | i should have used haskell for the entire process, but i was unfamiliar with it when i started my thesis |
| 18:49.59 | errstr | and put too much work into it before it was apparent there were errors |
| 18:51.31 | errstr | basically, i was unconvinced that strongly typed languages were particularly useful, until i worked through my thesis. now i'm a convert. |
| 18:52.06 | levi | I am already a convert, I am just seeking a deeper understanding. |
| 18:52.29 | errstr | in fact, to bash C further: i assert that C's static *but* weak typing system is the source for a majority of security vulnerabilities over the years |
| 18:52.46 | levi | I fully agree. |
| 18:52.48 | errstr | the type is only a truthiness factor |
| 18:53.46 | errstr | and surprise: we've been able to mathematically infer exact types since the late sixties, why did C have to fail so badly at it? |
| 18:53.55 | jxqz | errstr: what's your thesis about? |
| 18:54.15 | errstr | static program analysis of dalvik byte code for detection of malware |
| 18:54.44 | errstr | http://blog.errstr.com/2013/04/06/concrete-to-abstract-semantics/ <-- the part that i used haskell for |
| 18:54.51 | levi | Anyway, I'm taking the approach that I'm taking because I don't currently feel comfortable enough doing mathematical proofs to do the proof-related exercises in TaPL by hand without someone checking them for me, and Software Foundations happens to have an automatic mechanism built-in for checking most all of the exercises. |
| 18:55.31 | levi | And I feel that I won't get the deep understanding of type systems that I'd like to get without getting comfortable with the mathematical foundations in the process. |
| 18:55.44 | youtah | is yak shaving, no thanks to Java |
| 18:56.50 | errstr | oh god, don't get me started on Java... "Let's implement generics! I know, let's use type erasure... nothing could go wrong!" |
| 18:57.00 | youtah | lol |
| 18:57.35 | jxqz | wants to go to a user group meeting where levi and errstr debate proof theory |
| 18:58.31 | levi | Hah, I am merely a neophyte in the area of mathematical proofs. It would probably not be an interesting debate. |
| 18:59.06 | errstr | levi: going through Types and Programming Languages and then SICP in that order, gave me a good starting point for understanding the foundations of the math behind typing. I think it would be fun to go through Software Foundations |
| 18:59.15 | jxqz | levi: there's nobody at UU, sadly, in either the math or philosophy departments that does anything even close to what I want to do |
| 18:59.30 | errstr | UU == University of Utah? |
| 18:59.31 | levi | jxqz: What it is that you want to do? |
| 18:59.40 | jxqz | proof theory |
| 18:59.50 | jxqz | errstr: yes |
| 18:59.58 | levi | And what do you mean by proof theory? |
| 19:00.00 | jxqz | why am I in cosmology then? |
| 19:00.15 | jxqz | all of it. I'll eat the whole sandwitch |
| 19:00.20 | jxqz | sandwich |
| 19:00.38 | levi | Because you can impress people at parties with vague talk about cosmology, but not so much with proof theory. |
| 19:00.51 | jxqz | haha, cosmology gets way more money |
| 19:01.14 | errstr | jxqz: actually, if you are interested in Category/Group theory, the U has a great PL program: Matt Flatt and Matt Might (my research prof) are leaders in the field |
| 19:01.32 | levi | By proof theory, do you mean mathematical foundations? I am just not really sure what 'proof theory' means as a field of study. |
| 19:01.38 | jxqz | levi: survival in academia is all about convincing the lame people with dollarz that your project is wicked cool |
| 19:02.08 | levi | Survival as an industry programmer is pretty much the same way. :P |
| 19:02.12 | jxqz | you *must* *must* always advertize that your project might just be able to detect dark matter and dark energy |
| 19:02.19 | errstr | jxqz: have you taken Foundations of Analysis at the U? |
| 19:02.24 | jxqz | errstr: both |
| 19:02.34 | jxqz | I got a BS in phys and math |
| 19:02.55 | errstr | ah: I both loved and hated FoA |
| 19:02.56 | jxqz | errstr: yes, yes. Moar category theory plz |
| 19:03.09 | jxqz | errstr: who were your professors? |
| 19:03.25 | jxqz | I had DeFernex and Taylor |
| 19:03.35 | errstr | Y.P. Lee |
| 19:03.56 | jxqz | there are goodo professors and there are difficult professors in the math dept |
| 19:03.57 | errstr | i just took the first semester, since it covered up to what i needed for my PL studies |
| 19:04.09 | jxqz | you missed all the best stuff |
| 19:04.13 | jxqz | :) |
| 19:04.49 | youtah | CURSES JAVA AT THE TOP OF HIS LUNGS |
| 19:04.57 | errstr | heh, i also wanted to graduate on time :)... i took FoA in my second-to-last semester and had my last bit of CS work to complete along with my thesis for the last semester |
| 19:04.59 | youtah | well, at least on Ubuntu |
| 19:07.52 | *** join/#utah RyanE (~RyanE@rberick.dsl.xmission.com) |
| 19:09.22 | levi | Anyway, there seems to be some interesting work in mathematical foundations that's recently been published in the book 'Homotopy Type Theory and Univalent Foundations'. You might find it interesting, if you haven't seen it already, and you can download the book freely. |
| 19:09.36 | *** join/#utah JalenJade (~JalenJade@c-24-10-186-68.hsd1.ut.comcast.net) |
| 19:11.33 | jxqz | levi: definitely interested |
| 19:11.37 | levi | I found a book that introduces category theory at a very basic level that it appears I might be able to follow. I have a somewhat fuzzy basic understanding of category theory, but I don't understand it well enough to derive any sort of benefit from it. |
| 19:11.57 | jxqz | it's a few abstractions away from ordinary math work |
| 19:11.59 | levi | jxqz: homotopytypetheory.org |
| 19:12.35 | jxqz | levi, errstr: this is the foundations of analysis text used by UU: http://jxqz.us/analysis/ |
| 19:13.04 | jxqz | it's understandable, has worked examples and homework assignments |
| 19:14.16 | errstr | speaking of HOTT and Coq: https://github.com/HoTT/HoTT/blob/master/README.markdown |
| 19:14.45 | levi | jxqz: Software Foundations appears to be kind of like that, but it develops the mathematics necessary for analysis of program semantics instead of the mathematics necessary for doing calculus; and it's all done within the Coq framework. |
| 19:15.34 | jxqz | mathematicians love to write functions like f: R --> [0,\infty) rather than f(x) = x^2, but this notation was originally invented for category theory |
| 19:16.11 | jxqz | yeah, the focus on calculus is only interesting if you're into analysis |
| 19:16.33 | youtah | Package "openjdk-7-jre" is virtual. |
| 19:16.35 | levi | My problem with mathematical homework assignments is that I don't have anyone to grade them for me. :) |
| 19:16.39 | youtah | Thanks! WTF does that mean? |
| 19:16.49 | jxqz | levi: I'll grade them for you :) |
| 19:16.55 | jxqz | if I can understand it, that is |
| 19:17.04 | levi | youtah: It means that there are a number of concrete packages of different names that provide that virtual package. |
| 19:17.13 | levi | youtah: So you need to pick one of those to install instead. |
| 19:17.43 | youtah | lol, it is a graphical prompt with only an "okay" button |
| 19:18.06 | levi | Oh, well, I have no idea then. Good luck! |
| 19:18.41 | ldav15 | youtah: The GUI might provide a way to search the provides of that package |
| 19:18.49 | jxqz | the problem with java is that it's not well-defined package-wise. I remember Bryan Sant explained it all on the plug list several years ago and then I understood |
| 19:19.02 | levi | jxqz: Well, I *think* that working through proofs in Coq is helping me get a better handle on constructing proofs in general, at least those of the sort typically done in programming language work. |
| 19:19.19 | youtah | and I am on Lucid |
| 19:19.36 | jxqz | levi: doesn't the language verify your proof for you? :) |
| 19:19.40 | jxqz | to some extent anywya |
| 19:19.46 | youtah | I am thinking that 7 isn't available on ludicrous errrr.... lucid |
| 19:20.01 | levi | jxqz: It does completely verify the proof for you, but it also automates parts of it. |
| 19:20.41 | jxqz | levi: are you familiar with Whitehead and Russel's Principia Mathematica? |
| 19:20.42 | levi | So, even while stepping through it interactively, it can be somewhat different from following a standard informal written proof. |
| 19:21.27 | jxqz | that's part of the stuff I'm interested in |
| 19:21.31 | levi | And, at least given my current level of skill with it, sometimes the parts that are hard about constructing the proofs in Coq correspond to trivial parts of constructing them by hand. |
| 19:21.56 | jxqz | noway, always choose formal over informal |
| 19:22.00 | levi | But at least afterward you're fairly confident you didn't do something stupid. |
| 19:22.32 | levi | I mean, sometimes it's difficult to tell Coq which part of the expression to rewrite based on a previously proved theorem. |
| 19:26.04 | levi | To some degree, you can throw stuff at the system and see what sticks, and not really understand what you're doing. Writing an informal proof along with the formal one can help to solidify the thought process involved in proving it, to ensure you understand each step you're telling Coq to take. |
| 19:32.30 | levi | Anyway, I eventually want to work through Pierce's Software Foundations and Types and Programming Languages as well as Robert Harper's Practical Foundations for Programming Languages. |
| 19:37.37 | jxqz | what about knuth's book |
| 19:37.52 | jxqz | you know, The Book |
| 19:38.30 | levi | It's not really about programming languages, at least not the part published so far. |
| 19:38.56 | jxqz | I've never read it |
| 19:39.00 | levi | The algorithms are specified in prose and flowcharts, and the implementations are in a custom assembly language. |
| 19:40.16 | levi | Oh, I missed your question a while back about Principia Mathematica. I know *of* it, but I have not looked at the actual contents. |
| 19:40.32 | jxqz | it's a derivation of the foundations of mathematics |
| 19:40.39 | levi | Right. |
| 19:40.58 | jxqz | modified Peano language, 2nd order logic, proving some basic theorems |
| 19:41.03 | levi | I've read some of Russel's more philosophical work, though. |
| 19:42.03 | levi | I've proved a bunch of basic theorems about a Peano-representation of Naturals via Software Foundations exercises. |
| 19:43.04 | jxqz | there's no way I'd be able to grasp it on my own without my mathematical backgroud |
| 19:43.39 | levi | Yeah, I knew enough to not even bother looking at the text itself at my current level of mathematical sophistication. |
| 19:45.10 | jxqz | I'm kind of serious about having some kind of logic/formal linguistics user/community group though |
| 19:45.15 | jxqz | if there isn't one already |
| 19:48.26 | errstr | yeah, once i got into the deeper aspects of galois' work, it was above my mathematical sophistication. i had to trust that it was right. |
| 19:49.07 | jxqz | ooh, yes, galois |
| 19:49.57 | jxqz | errstr: Galois theory is used to factor polynomials? |
| 19:50.07 | errstr | i can wrap my head around proofs based on it, but getting into the proofs about it, i feel lost. perhaps that second semester of FoA would have helped |
| 19:50.35 | jxqz | I can understand galois theory only because I had 2 semesters of algebra |
| 19:50.45 | errstr | hrm, jxqz: i'm only familiar with its application in category/type theory |
| 19:52.08 | jxqz | well, I'm sure it's application is far broader than Galois' original work |
| 19:52.15 | errstr | i don't think two semesters of algebra would suffice for understanding lattices |
| 19:52.23 | errstr | jxqz: yes, far broader |
| 19:52.31 | jxqz | depends on what you're doing with them |
| 19:52.59 | jxqz | wikipedia seems to think that modern galois theory is a mapping of field theory onto group theory |
| 19:54.28 | errstr | the importance of galois connections in the work i did is in proving that a particular partial function from a -> a* (where a* is an abstract type) and a* -> a is correct |
| 19:54.39 | jxqz | there's this guy, John Baez, that is enjoying using category theory to construct physics, whatever that means |
| 19:55.55 | jxqz | (phyics being a very small nuclear set of postulates, some group theory, some Lie theory, and applied topics from differential topology) |
| 19:56.56 | jxqz | even quantum loops, supersymmetry, and string theory do not radically alter this basic foundation of physics |
| 19:57.45 | jxqz | and there's obviously ths functional analysis aspect to it |
| 20:09.42 | levi | jxqz: You might enjoy following the n-category cafe blog and its associated wiki. |
| 20:19.34 | *** join/#utah jima_ (jima@utah.b0rk3d.com) |
| 20:21.19 | *** join/#utah Sargun_Screen (~sargun@atarack/Staff/Sargun) |
| 20:22.32 | *** join/#utah davad (~davad@c-98-202-243-63.hsd1.ut.comcast.net) |
| 20:25.37 | levi | One of the exercises in Software Foundations that was kind of fun was to create a binary representation of the natural numbers and then a conversion from the peano to binary representations and some proofs about it. I made a small error in my representation definition, which manifested in a contradiction in my proofs, so I knew I had to go back and fix it. |
| 20:27.24 | jxqz | ever heard of the p-adic numbers? |
| 20:27.54 | jxqz | it's an algebraic completion of the rational numbers alternative to the real numbers (the continuum) |
| 20:27.57 | *** join/#utah olli_ (~olli@c-71-195-232-74.hsd1.ut.comcast.net) |
| 20:28.24 | levi | Nope. |
| 20:28.36 | jxqz | well, now you have |
| 20:28.38 | *** join/#utah olli_ (~olli@c-71-195-232-74.hsd1.ut.comcast.net) |
| 20:28.49 | levi | My exposure to mathematical stuff has been very limited. :( |
| 20:29.46 | jxqz | the math department here has several colloquia per week. You could just show up and nobody would notice :) |
| 20:33.36 | levi | I would be completely lost. |
| 20:33.45 | levi | Here's another fun thing: http://logitext.mit.edu/logitext.fcgi/tutorial |
| 20:36.14 | *** join/#utah woolcap (~orbit@192.150.9.201) |
| 21:05.12 | *** join/#utah NoCoolName_Tom (~NoCoolNam@64.124.34.2) |
| 21:11.49 | *** join/#utah emcnabb (~emcnabb@cpe-065-190-142-224.nc.res.rr.com) |
| 21:11.49 | *** mode/#utah [+v emcnabb] by ChanServ |
| 21:25.42 | *** join/#utah jima (jima@utah.b0rk3d.com) |
| 21:25.54 | *** join/#utah VanHelsing (~vanhelsin@97-126-220-20.slkc.qwest.net) |
| 21:30.04 | *** part/#utah woolcap (~orbit@192.150.9.201) |
| 21:45.20 | *** join/#utah Newsome (~sorenson@dsl081-138-007.chi1.dsl.speakeasy.net) |
| 21:45.58 | jxqz | ubuntu has decided to stop recognizing my webcam. I had to manually load the what seem to be the appropriate drivers, but there's no notice of it in /dev, lshw, or lspci |
| 21:46.16 | jxqz | is there something else I can try? |
| 21:46.18 | levi | errstr: Hah, I didn't realize the lattices you were talking about were posets. I read an introduction on those in one of the programming language foundation books I have started, but I'm not sure which. |
| 21:46.49 | levi | jxqz: Is it a usb webcam? If so, look in lsusb. |
| 21:47.27 | *** join/#utah mahelious (~mahelious@50-198-180-125-static.hfc.comcastbusiness.net) |
| 21:48.59 | errstr | levi: yeah, they are fascinating models for type theory |
| 22:00.41 | levi | As I recall, the justification for their introduction went something like this: "Mathematics defines functions over sets; but in a programming language, the things we call functions aren't defined over true mathematical sets, so we can't directly use theorems relating to set-based functions to reason about programming functions. But it turns out that there are some mathematical models for collections of things that do correspond to the |
| 22:00.41 | levi | domain/co-domain of programming functions, so we can use theorems about them instead!" |
| 22:00.54 | levi | And then, down the rabbit-hole we go... |
| 22:06.49 | fungus | jxqz, if you webcam is USB, lsusb will be better for you. If it isn't listed there at all, then it's a USB issue, not a driver issue. |
| 22:06.58 | levi | So, as I am now in charge of a regular meeting time at The Transistor about programming languages, would you guys be interested in participating in/contributing to some more theory-oriented meetings? So far, we have mostly just introduced the basics of various programming languages at an introductory level, but I would be interested in discussing some deeper stuff if there's sufficient audience. |
| 22:13.29 | *** join/#utah mahil (~mahelious@50-198-180-125-static.hfc.comcastbusiness.net) |
| 22:14.20 | *** join/#utah mahil (~mahelious@50-198-180-125-static.hfc.comcastbusiness.net) |
| 22:48.17 | jxqz | levi, fungus: already looked |
| 22:48.36 | jxqz | it's probably usb, builtin to the lid of the computer |
| 22:49.36 | jxqz | levi: yes |
| 22:50.55 | jxqz | but it still should show up in lshw |
| 22:56.58 | levi | Beats me. |
| 22:57.43 | jxqz | this is why all that theoretical stuff is useless and you're supposed to be solving practical problems |
| 22:59.25 | levi | Oh, I have spent plenty of time beating my head against practical things. I like to switch things up occasionally, though. |
| 23:27.46 | *** join/#utah NoCoolName_Tom (~NoCoolNam@64.124.34.2) |
| 23:40.34 | shalkie | jxqz: dmesg | grep -i cam |
| 23:40.44 | shalkie | See if there is any mention from the kernel. |
| 23:41.40 | *** join/#utah jalbretsen (~jalbretse@c-174-52-67-72.hsd1.ut.comcast.net) |
| 23:54.24 | *** join/#utah pdayton (~pjdayton@206.29.182.237) |
