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!

2213. Anonymous (12-203-201-140.client.insightbb.com) – 08 Mar 2005 19:23:24 [ 30 Days Has September ]

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.

2210. Tom 7 (gs82.sp.cs.cmu.edu) – 08 Mar 2005 15:29:59 [ Spring Break! ]

I don't know much about Coq, so I can't compare the two systems. Do I remember right that you don't get higher order abstract syntax as an encoding and reasoning tool "for free"? If so, that would be a major problem for the kind of work I'm doing.

Twelf proofs are a kind of logic program, yes. It's actually a fairly natural way of capturing the reasoning that I do when proving things on paper, which is nice. I don't see why that would be any trouble, more or less than it is worth. A functional language would perhaps be better still, and I think this is seen as one of the future directions for Twelf in the community (ie Delphin).

I use Twelf to prove things, and I prove things both to assure myself that they are true, and to understand why they are true (or, understand why not, when they aren't). Doing proofs by hand certainly helps me to understand the structure of the proof and diagnose problems (or form new ideas), at the cost of, well, doing the work of proving things by hand.

If I were just trying to get proofs of theorems, or test their validity, automated theorem proving (perhaps using tactics) would probably be expedient. 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.

2209. Anonymous (83.detroit-21rh15-16rt.mi.dial-access.att.net) – 08 Mar 2005 15:24:28 [ Head is shaved. ]

i think you look sexy, keep it shaved!!!!

2208. jcreed (wittgenstein.wv.cc.cmu.edu) – 08 Mar 2005 11:29:11 [ Spring Break! ]

There is also a theorem prover in twelf, which, given a goal, sometimes comes up with (what is really a logic program) proof of that goal.

There is a general question you seem to be asking an instance of. It's "In technique A I must create Xs "by hand", and in technique B I use some tools to create them "automatically". Isn't technique B clearly superior?"

While I don't doubt that, all other things being equal, computers automating more things is great, it seems like there are some costs to worry about. (I haven't actually had a lot of experience with Coq or other tactic-based provers, so I'd love to hear about your experience using them)

If the relevant tactics are specific, then I may suffer a "thinking cost" in how to phrase my informal proof in terms of those tactics, just as I have to think about how to phrase it in terms of twelf logic programs.

If the relevant tactics are very general, (like, a single TRY-TO-PROVE-USING-BRILLIANT-INSIGHT tactic) then I may suffer a performance cost in the machine trying to figure out how to apply the tactic in order to get a proof. I

If the tactics change over time, then there's a maintenance problem to be dealt with or at least worked around, in that a proof script that worked in the past no longer works with the modified tactics. I've heard rumors that this has been a problem with OTTER, but I don't know how accurate they are.

Anyway, after thinking about it for a bit, I'm sympathetic to the idea that representing proofs as hand-coded logic programs is certainly not the single most natural way of formalizing proofs. However, just like arguments about "expressiveness" and "naturalness" of programming languages, I don't know how to evaluate claims that a particular tactic-based system has a better set of building blocks. If you look past direct human use of the twelf metaproving system, its mathematical cleanliness has some benefits in terms of other programs manipulating and proving things about its structures. It might be rather hard to show that some particular tactic, say, terminates, but given the style of the algorithms that twelf uses, I imagine it would be rather easier there to prove such properties.

2207. adamc (206.169.168.190) – 08 Mar 2005 10:58:48 [ Spring Break! ]

Here's a question for hardcore Twelf fans, assuming some might be reading this:

Is it accurate to say that proving things in Twelf always means writing logic programs? If so, doesn't this bring you much more pain than it's worth, compared to tactic-based theorem provers? Do you think a Twelf expert will be as or more efficient at proving complex theorems as a Coq expert?

2206. jcreed (pool-151-201-59-13.pitt.east.verizon.net) – 08 Mar 2005 09:09:11 [ Spring Break! ]

Premises go above the bar, conclusions below it, and ridiculous ideas go in it.

2205. Tom 7 (h-68-166-177-37.phlapafg.dynamic.covad.net) – 08 Mar 2005 08:57:24 [ Spring Break! ]

Nearby we also have "Edinboro" (pronounced phonetically) and "Versailles" (also pronounced phonetically!) There's probably a Washington and a Springfield in every state.

It did eventually rain, though not as hard as I thought it would.

2204. Arthur (ctwboo101.ctw.utwente.nl) – 08 Mar 2005 02:56:22 [ Spring Break! ]

I didn't know there was a Palestine in Pittsburgh's neighborhood! And a Washington. How many Washingtons would there be in America?

And did it rain yet?

2203. Tom 7 (h-68-166-177-37.phlapafg.dynamic.covad.net) – 06 Mar 2005 10:36:12 [ NEW: Escape Beta 2! ]

Right, like that.

2202. jcreed (wittgenstein.wv.cc.cmu.edu) – 05 Mar 2005 18:02:18 [ NEW: Escape Beta 2! ]

Selection rectangle!

2201. Anonymous (pcd671036.netvigator.com) – 05 Mar 2005 02:53:11 [ FLAMING TEXT ]

yeah what the heck is this

2200. Tom 7 (gs82.sp.cs.cmu.edu) – 04 Mar 2005 17:51:07 [ NEW: Escape Beta 2! ]

mjn: I implemented eyedropper as the middle mouse click, so that will be part of the next version, too. I want to reserve right click for something a bit more critical, though I don't know what that is, yet. ;)

2199. Tom 7 (gs82.sp.cs.cmu.edu) – 04 Mar 2005 17:38:15 [ NEW: Escape Beta 2! ]

Satyap: You can save yourself from having to resolve 90% of the level by using the 's' and 'r' keys to save and restore a partial solution, respectively. The next version of the game (which may be a while because I've already committed to introducing robots in that version) will have undo (press 'u'), at least if you don't die. It's already in my development copy.

For sharing the player data, you can just copy the satyap.esp (or similar) file between the two machines. The players.esd is just an index of all the players that you have, so once each copy knows about that player, it will just read the .esp file and never needs to be copied.

The next version has switched to a text file format for the player file, which allows for the possibility of merging changes in two places (using diff/patch) or checking the player file into some version control system like CVS, which is what I do.

2198. Tom 7 (gs82.sp.cs.cmu.edu) – 04 Mar 2005 17:32:30 [ 10,000! ]

I see no Tom 7 music in your top 13,000!!