You made metafilter again:
http://www.metafilter.com/mefi/40453 |
| |
2244. jcreed (wittgenstein.wv.cc.cmu.edu) –
16 Mar 2005 12:26:21
[ Very Big ]
The nanobots are lulling you into a false sense of security. Watch out for the red-green-blue-gray-goo! |
| |
2243. Tom 7 (h-68-166-177-37.phlapafg.dynamic.covad.net) –
16 Mar 2005 11:00:47
[ NEW: Escape Beta 2! ]
Hmm. Well, Escape updates itself, so I'm not sure what sense that would make (you'd install in escape-200503150, but later you'd have 200601010 in there). How does this make including a game in a distro easier, or why does it make you roll your eyes to not do it? (Just curious.) |
| |
versioned, i presume, as in "escape-1.0.0.tar.gz" for example, with the top directory being "escape-1.0.0" rather than "escape-src". It seems to be normal practice for linux software. Not wanting to be a snob, but when i see a tarball unpack to "foogame" rather than "foogame-x.y.z" i give a little sigh and roll my eyes. ;) |
| |
Here in Australia, where we write dates as dd/MM, pi approximation day is the 22nd of July. |
| |
Here in Australia, where we write dates as dd/MM, pi approximation day is the 22nd of July. |
| |
2239. Tom 7 (gs82.sp.cs.cmu.edu) –
15 Mar 2005 13:55:32
[ HSE: Real Books ]
NOT EVEN LIGHTNING BOLT. |
| |
2238. Tom 7 (h-68-166-177-37.phlapafg.dynamic.covad.net) –
14 Mar 2005 19:24:26
[ Pi day... awesome! ]
No indeed. ;)
But maybe it can last until I graduate... |
| |
I don't guess the doubling pattern can continue indefinitely though, unless the people there are <i>really</i> amazing, though. |
| |
2236. Tadbot (pcp0010451887pcs.walngs01.pa.comcast.net) –
14 Mar 2005 14:12:17
[ Pi day... awesome! ]
Dave put a couple pix at http://vaxcave.com/index.php?p=314 |
| |
2235. Tadbot (pcp0010451887pcs.walngs01.pa.comcast.net) –
14 Mar 2005 14:01:55
[ Pi day... awesome! ]
r0x. A nice Π party. Celebrate it yearly. Smath can visit annually.
Aronofsky, Darren's cinematic Max vs Ant arthouse film - supply it!
Anyway, how's Dan now? Nerdcore job or working 9-5? |
| |
2234. ndm (c-67-165-67-55.client.comcast.net) –
14 Mar 2005 14:00:00
[ Pi day... awesome! ]
yeah, where's the pics? |
| |
2233. FARINA00 (host226-98.pool8536.interbusiness.it) –
14 Mar 2005 13:08:58
[ Pi day... awesome! ]
PIctures! |
| |
2232. Tom 7 (h-68-166-177-37.phlapafg.dynamic.covad.net) –
14 Mar 2005 00:30:27
[ Very Big ]
I think it's "Digital light processing" or something like that. It's a MEMS technology which uses an array of (millions of) miniature mirrors on a chip that can be tilted to different angles in order to reflect different amounts of light. A color wheel sends red, blue, green, and white light alternatingly to bounce off the chip and onto the surface. It's generally better than LCD because it doesn't require three different imaging devices per pixel (so there is greater pixel density for cheaper), and the colors all end up exactly on top of one another, and the pixels can be larger. Anyway, it looks sweet. |
| |
2231. jcreed (pool-70-17-165-61.pitt.east.verizon.net) –
13 Mar 2005 23:35:19
[ Very Big ]
What does DLP stand for? |
| |
2230. Tom 7 (h-68-166-177-37.phlapafg.dynamic.covad.net) –
13 Mar 2005 00:26:18
[ NEW: Escape Beta 2! ]
I haven't heard of versioned tarballs, and can't find something easily on google that explains it. Any tips, anyone? |
| |
2229. Tom 7 (h-68-166-177-37.phlapafg.dynamic.covad.net) –
13 Mar 2005 00:23:02
[ Spring Break! ]
In fact, Twelf does already have constraint domains for integers (and soon, I believe, integers-modulo-2^n), although the coverage checker currently doesn't work on these. |
| |
Ever heard of versioned tarballs... try to use them... it's a great help to us who try to provide the game in a distro... |
| |
2227. Andrew (yale128036074005.student.yale.edu) –
12 Mar 2005 14:19:52
[ Spring Break! ]
As I said, it depends on what you are doing. For something like assembly, with lots of arithmetic and little substitution, I think Coq is a lot better.
Also, there is no reason Twelf cannot have an arithmetic decision procedure, whereas there is a reason Coq cannot have HOAS, but your query seems more pragmatic than that. |
| |
2226. Anonymous (dsl-80-45-182-153.access.as9105.com) –
12 Mar 2005 10:40:07
[ FLAMING TEXT ]
This is shit |
| |
2225. adamc (12.45.39.194) –
11 Mar 2005 23:04:51
[ Spring Break! ]
So my statement about "the functional subset of OCaml" was inaccurate. In my defense, I did preface it with the get-out-of-jail-free-card "basically." :-)
What I really meant is that you can use the basic ML syntax that you're used to instead of having to express all recursion as calls to fold functions, or otherwise indicating primitive recursion explicitly.
In response to Andrew: I'm still not convinced that substitution lemmas alone make Twelf worth using. An arithmetic decision procedure is such a time saver for proving facts about assembly programs. Coq also has a bag of other very useful tactics, including one that uses a complete propositional logic decision procedure (combined with definition unfolding and other low-cost tactics) to solve as much of a goal as it can and then decompose the rest into simplified subgoals. |
| |
I've got a machine-head. It is better than the rest.
Green to red. Machine-head.
And I walk from my machine.
Indeed, I walk from my machine. |
| |
2223. Tom 7 (gs82.sp.cs.cmu.edu) –
11 Mar 2005 17:26:40
[ shhhhh. ]
I think it's more like formally proving that it's incorrect. |
| |
2222. Andrew (yale128036074005.student.yale.edu) –
11 Mar 2005 16:54:08
[ Spring Break! ]
"Do you think a Twelf expert will be as or more efficient at proving complex theorems as a Coq expert?"
It depends on what you are doing. Twelf gives you certain substitution lemmas for free. If you aren't using those, you are probably better off using Coq, simply because it is a bit more mature, so there are more libraries, more automation, etc.
"Doing proofs by hand certainly helps me to understand the structure of the proof and diagnose problems"
You can always write explicit proof terms in Coq, and I know somebody who prefers to do this. (You are writing a functional, not a logic program, but this is mostly a matter of syntax, given that Twelf, I believe, internally translates the logic program into a functional one.)
"Like Jason said, unless you have a clear specification of when the theorem proving will be successful, I do worry about issues of maintainability over time. I think really writing down the proofs by hand is superior in this regard."
You can get the explicit proof term generated by a tactic, if you are worried about tactics changing over time. I've found that automation is nice because it makes your proofs more robust with regards to small changes in your system. With tactics, your proofs will still sometimes break, but without them, they will always break.
"One can certainly do HOAS in ML."
Sort of, but you can't really go under the lambda except in a very limited fashion. |
| |
2221. Andrew (yale128036074005.student.yale.edu) –
11 Mar 2005 16:28:59
[ shhhhh. ]
You should formally prove the correctness of SSH in Coq, then extract an OCaml program from the proof. |
| |