Thursday, April 12, 2007

coq's -ness-nesses

In response to Stefano's reply to my post about Coq:


Usually such pieces of software are more seen as academic toys, seeing it promoted as a geeky software is a joy to me.

I really hate to detract from your happiness -- but I definitely had the word "math" implicitly stuck before "geek toy". :) Most coders that I've met are, at best, indifferent to mathematics, outright hostile at worst, so I doubt that coq will get far outside of small niches where the benefits are irresistable (security software, maybe? -- and of course pure math). I read up on this stuff despite it being utterly useless for anything I'm likely to be paid to do (unless I return to academia) because I'm a hopeless weenie loser who likes math. :P


Coq is not really a programming language (even if the CoqArt book says so, to attract the developer community), it is mainly a proof assistant; i.e. a software in which you give definitions, state theorems and prove them.

Well, this all depends on how you define programming language, which is one of those never-ending definitional questions. But using my general conception of what a programming language is, I actually have noticed two programming languages inside Coq.

  1. The more interesting one (IMO) is the proof language they call "Gallina" and the "Vernacular", in which you construct proofs by reducing your goal to a tautology. The goal here seems to be to compute a well-typed term in Coq's core calculus, and you generally construct programs interactively: Coq shows you the current program state (expressed as one or more goals and a set of local hypotheses) and you manipulate it by (e.g.) applying lemmas to yield new known facts.

    I think this language is fairly weak viewed as a programming language. It's completely unreadable and the proofs generated don't correspond to the reasoning process one normally follows when working out a proof. I am less annoyed by it now that I've learned how to do forward reasoning :), but it seems like backwards reasoning is really pushed, and that just seems .. well .. backwards to me. There's also a strong tendency to use implicitly generated names for things and to just "know" what the state of the system after issuing a command will be; as far as I can tell, the only way to understand a Coq proof is to step through it in coqide.

    While it's nice to be able to "trust the kernel", it would also be nice to be able to "read a proof" directly. Among other things, their inscrutability makes me think that Coq proofs would be annoying to maintain over time. This is not necessary for stuff that's part of Principia Mathematica, but seems likely if you're developing a new theory -- in particular, I would shudder (theatrically) at the mere thought of including embedded Coq proofs in my programs.

    Some additional brief comments on this were written by Nick Benton and put on the Web under the title of Machine Obstructed Proof.

  2. The other sense is that Coq directly embeds a strongly normalizing variant of System F (I think? -- at least the simply typed LC with some type parametricity) with primitive recursion over inductive structures. This isn't Turing-complete (of course!), but I would certainly call it a real programming language.

    As you note, though, this is less interesting unless you want to prove facts about your programs.


Regarding the synergy of Coq with OCaml: yes, you can prove in Coq the correctness of OCaml program, but actually not more than you can do with programs written in other programming languages

I was specifically thinking about Concoqtion; I have no idea how other projects compare, and I apologize if I incorrectly summarized it!


At 12:47 AM, Blogger oakleyses said...

kate spade handbags, prada outlet, nike air max, louis vuitton, nike air max, louis vuitton outlet online, burberry outlet online, burberry outlet online, tiffany and co jewelry, michael kors outlet, gucci handbags, tory burch outlet, louis vuitton outlet, chanel handbags, jordan shoes, longchamp outlet online, nike shoes, louboutin shoes, red bottom shoes, coach outlet store online, kate spade outlet online, polo ralph lauren outlet, oakley vault, coach outlet, prada handbags, coach purses, louis vuitton handbags, longchamp handbags, christian louboutin outlet, oakley sunglasses, cheap oakley sunglasses, michael kors outlet online, michael kors outlet online, louis vuitton outlet, polo ralph lauren, christian louboutin shoes, michael kors outlet online, ray ban outlet, nike free, longchamp outlet, michael kors outlet store, michael kors outlet online, coach outlet, true religion, ray ban sunglasses

At 12:47 AM, Blogger oakleyses said...

abercrombie and fitch, longchamp pas cher, north face, vans pas cher, nike free, nike air max, longchamp, tn pas cher, hollister, air max pas cher, michael kors canada, chaussure louboutin, oakley pas cher, sac vanessa bruno, ray ban uk, louis vuitton uk, hollister, new balance pas cher, lululemon, nike free pas cher, north face pas cher, scarpe hogan, nike trainers, air max, nike roshe, ralph lauren pas cher, barbour, nike huarache, burberry pas cher, guess pas cher, nike air max, true religion outlet, longchamp, lacoste pas cher, sac michael kors, ralph lauren, louis vuitton pas cher, michael kors uk, nike blazer pas cher, mulberry, nike air force, air jordan, hermes pas cher, louis vuitton, nike roshe run, timberland, sac louis vuitton, ray ban pas cher, converse pas cher, true religion outlet

At 12:48 AM, Blogger oakleyses said...

herve leger, soccer jerseys, uggs outlet, jimmy choo shoes, lululemon outlet, nfl jerseys, canada goose pas cher, vans outlet, soccer shoes, roshe run, valentino shoes, moncler, rolex watches, chi flat iron, uggs on sale, canada goose, north face outlet, ghd, new balance outlet, north face jackets, mcm handbags, ugg soldes, moncler, canada goose uk, mont blanc pens, beats headphones, canada goose outlet, celine handbags, instyler ionic styler, ferragamo shoes, ugg boots, bottega veneta, ugg, moncler outlet, abercrombie and fitch, ugg outlet, wedding dresses, mac cosmetics, birkin bag, reebok outlet, canada goose outlet, insanity workout, moncler, giuseppe zanotti, asics shoes, hollister, canada goose outlet, babyliss pro, marc jacobs outlet, p90x workout

At 2:23 AM, Blogger Unknown said...

jordan 13
asics running shoes
cheap jordans
polo ralph shirts
jordan retro 3
rolex watches
louis vuitton outlet
michael kors purses
ray ban sunglasses outlet
tods outlet
michael kors handbags
michael kors handbags
ray ban sunglasses discount
nike outlet store
coach factory outlet
vans shoes
true religion jeans
kevin durant shoes
replica watches
michael kors outlet
oakley sunglasses
louis vuitton outlet
michael kors outlet online
louis vuitton
nike factory outlet
christian louboutin outlet
juicy couture
kate spade handbags
kobe shoes 11
longchamp outlet
ralph lauren polo
true religion jeans
nike outlet
louis vuitton handbags
kate spade
insanity workout
ray ban sunglasses
beats headphones
gucci handbags

At 10:42 PM, Blogger John said...

true religion outlet
nike max
san diego chargers jerseys
nike outlet online
nike sneakers
michael kors bags
mont blanc
nike free run
timberland outlet
nike shoes


Post a Comment

<< Home