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. |
| |
2220. Tom 7 (h-68-166-177-37.phlapafg.dynamic.covad.net) –
09 Mar 2005 22:42:54
[ Spring Break! ]
Yeah, I think those are fair criticisms. But anyway, like I said, the way I use it isn't to produce machine-checkable proof certificates, but to work the problem in a very detailed way, with help from the computer. (It would be great, though, if Twelf could output certificates for its totality checking!)
I must misunderstand something you're saying, though--how is it that Coq allows you to use the "complete functional subset of O'Caml" but that you can't do HOAS? One can certainly do HOAS in ML. Is it that you kist can't induct over the things afterwards? |
| |
2219. jcreed (wittgenstein.wv.cc.cmu.edu) –
09 Mar 2005 20:52:10
[ Spring Break! ]
I can't help but agree with you about arithmetic. Soooo boring to prove those theorems by hand.
I really should play with Coq some, to see whether I miss much in the way of HOAS. Already to formalize a lambda calculus where beta-normal eta-long forms are maintained syntactically (due to Kevin Watkins) you kind of have to do an amount "real work" to define substitution even in twelf that's roughly proportional to how complicated your syntax is.
|
| |
2218. adamc (206.169.168.190) –
09 Mar 2005 12:30:05
[ Spring Break! ]
I've used Coq to prove soundness of TALx86 for our local Foundational PCC system. From what I've heard of other efforts that use Twelf, it seems like this was measurably more pleasant.
About the "thinking cost": When you want to prove something about arithmetic that you would say is "obvious" in an informal proof, it sure is nice to invoke the tactic for the Omega procedure, instead of writing a logic program. :-) This is an example where I think everyone agrees that the thinking would be a bad use of time.
Also, in the context of mobile code security, you focus more on a small TCB for the end-user, so it's sort of inconsequential whether anyone "understands" a proof that a system is sound, modulo issues of revising the proof due to changes in the system. For the same reason, we don't worry overly much about the performance costs of tactics, since each tactic produces an efficiently-checkable standalone proof in the end. Similarly for the question of whether tactics terminate.
For mature systems like Coq, the tactics aren't changed in backwards-compatibility-breaking ways. When they recently changed the syntax, they included a translator from the old syntax, and my old proofs worked in the substantially refactored new version without manual intervention.
It's true that you can't use higher-order abstract syntax with Coq. The reason is based on the neat result that, while simply-typed lambda calculus is strongly normalizing, it becomes Turing complete-ish when you add the simplest formulation of recursive types. Coq uses syntactic restrictions to keep the calculus strongly normalizing, even with recursive types. I think this is morally equivalent to the Twelf totality checker, and it seems to me to be better integrated into the core logic. There is no way to type-check a Coq function definition if the function isn't total, for instance, even though you can basically use the complete functional subset of OCaml in such definitions.
I use hand-rolled syntactic substitution in place of higher-order abstract syntax. The added cost is basically just defining a substitution function, figuring out what lemmas I need about it, and what inductive hypotheses I need for their proofs. The proofs themselves are automated. |
| |
2217. Tom 7 (h-68-166-177-37.phlapafg.dynamic.covad.net) –
09 Mar 2005 09:18:00
[ Spring Break! ]
Did you mean... hamburgler? |
| |
2216. Arthur (ctwboo101.ctw.utwente.nl) –
09 Mar 2005 06:36:24
[ Spring Break! ]
Your search - gomburgible - did not match any documents. |
| |
2215. jcreed (h-68-166-177-37.phlapafg.dynamic.covad.net) –
09 Mar 2005 01:07:00
[ Spring Break! ]
Impossible! Everything I say is perfectly and immediately gomburgible. |
| |
2214. heather (cobamide.bio.pitt.edu) –
08 Mar 2005 20:07:44
[ Spring Break! ]
So fitting to see Jcreed and Tom7 break into conversation that I don't begin to understand on Tom 7's Radar! |
| |
FBGFNDFKFJIEAJLGVAFDHYUFIKJIAFu9poepibgkiowyug908riyhiwr8y9gtroig98rew78gt90t8y857u89tguwrty897thy90wr789rw77u8trw898t9yy8957t |
| |
2212. FYTF876WE89F78W (12-203-201-140.client.insightbb.com) –
08 Mar 2005 19:23:07
[ 30 Days Has September ]
rsdgytvukhdjkfysduuvoijdfhuicyofuviy8od8iosdfuio98ODFIEUFV8I7YDFOEWFUEW689 |
| |
2211. Quincunx (cpe-24-25-175-211.maine.res.rr.com) –
08 Mar 2005 16:53:56
[ Spring Break! ]
So fitting to see a radar image in Tom 7 Radar. |
| |