Monday, April 09, 2007

Latest Shiny Geek Toy: coq

So, one of the reasons I've been a bit uncommunicative the last few weeks is that I've been getting my head around Coq, maybe one of the most fascinating pieces of software I've played with in a long time.

What is Coq? I don't know if I understand it well enough yet to give a complete description (the Coq tome only arrived in the mail on Friday and I have yet to make it past the introduction, what with taxes and so on). Here's my best shot:

Coq is a programming language where you write proofs as functions taking proofs of their preconditions and producing proofs of their results. That is, a proof that "If X is an integer, then X-1 < X" becomes a function that accepts a proof of "X is an integer" and produces a proof of "X-1 < X".

You can manipulate logical expressions more or less the way you expect. For instance, if you have in your hands a set S of natural numbers and a proof that "forall nonempty sets T of naturals, T has a least element", then you can bang these together to produce the least element of S (or rather, a proof that it exists).

I don't think this describes the theoretical underpinnings of Coq, but it does describe my experience of actually using it to prove stuff.

To get the hang of Coq, I'm working my way through basic automata theory -- regexps are done, but I couldn't work out how to express some finiteness constraints on FSMs without generating a lot of extra typing; hopefully the Coq book will have some hints. Once that's done, I'm actually tempted to try something more ambitious. [snip long digression] We'll see ... watch this space :).

It was a real rush, though, to code up these theorems and watch the computer verify them. What really fascinated me was how close to being a practical tool this is. Coq isn't at all a toy -- without quite getting all the theory yet, my intuition is that it can probably cover anything you can express in the predicate calculus (with sufficient amounts of typing, anyway), and while there are a few shortcomings, it's almost (IMO) at the point where anyone who knows some formal logic and has a little patience can prove interesting stuff. Even more suggestive of possibilities, there's a project (which I sadly haven't had time to look at) that integrates Coq with OCaml, so you can have proofs about your OCaml code verified at compile-time!

I could go on and on ... anyway, this is a really cool tool and I'd encourage any mathematically-minded person to give it a spin. The only sad thing is that I doubt I'll ever have the opportunity to explore this stuff in my day job unless/until I go back to school :-(.

Shortcomings of Coq specifically and the whole concept of correctness proofs on programs generally have been moved to a future blog post that may never appear depending on how ambitious I'm feeling this week. Rest assured that I'm aware of (some of) them, I just hit my self-imposed length limit.

[0] the reason being that I could only prove correct the formal underpinnings of the resolver; in practice, a lot of the bugs are in the interface to apt, or in apt itself, and I can hardly prove that code correct.

14 Comments:

At 10:53 PM, Anonymous Anonymous said...

"...one of the reasons I've been a bit uncommunicative the last few weeks is that I've been getting my head around Coq..."
I read that and laughed. :)

All jokes aside, that's an awfully cool toy.

 
At 2:32 PM, Anonymous Martijn Vermaat said...

A good deal of the course Logical Verification is concerned with Coq. Maybe you find the course notes interesting.

 
At 10:53 AM, Anonymous Anonymous said...

The hardware implementation of Coq is likely to get better penetration ;)

 
At 2:02 AM, Blogger Annie Monie said...

Conservation-conscious, Mother Earth types of geeks, on the other hand, admire all sorts of toys made of recycled materials. Examples of this are the Scrap Metal Sculpture® series of toys.

geeky toys

 
At 12:50 AM, Blogger Coach Factory 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:51 AM, Blogger Coach Factory 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:52 AM, Blogger Coach Factory 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 11:22 PM, Blogger John said...

michael kors outlet
north face
nike roshe run
ralph lauren uk
fitflop uk
nike store uk
ugg boots clearance
tory burch outlet
kobe bryant shoes
instyler max
hollister kids
coach outlet store online
adidas originals
ray-ban sunglasses
nike trainers
moncler outlet
pandora
nike huarache
sac longchamp pliage
uggs on sale
louboutin
ray bans
christian louboutin outlet
mont blanc
rolex watches
gucci shoes
nike air max
louis vuitton outlet
canada goose uk
nike cortez
swarov ski jewelry
2015922yuanyuan

 
At 8:04 PM, Blogger 风骚达哥 said...

20151014 junda
Louis Vuitton Handbags Factory Store
Louis Vuitton Bags On Sale
Louis Vuitton Bags Outlet Store
cheap ugg boots
louis vuitton outlet
Michael Kors Outlet Real Handbags Online
ugg boots
Air Jordan 3 III Retro Free Shipping
louis vuitton outlet
celine
Christian Louis Vuitton Red Bottoms
coach factory outlet
ray ban sunglasses uk
Ugg Boots,Ugg Boots Outlet,Ugg Outlet,Cheap Uggs,Uggs On Sale,Ugg Boots Clearance,Uggs For Women
Coach Outlet Store Online Handbags Clearance
canada goose outlet
ugg boots outlet
Abercrombie And Fitch Kids Online
true religion outlet
cheap jordan shoes
New Louis Vuitton Handbags Outlet
cheap uggs
nfl jerseys
canada goose jackets
Abercrombie and Fitch Outlet Sale
louis vuitton outlet
canada goose outlet
uggs australia
michael kors outlet stores
Coach Factory Outlet Online Sale

 
At 8:27 PM, Blogger oakleyses said...

uggs outlet, uggs on sale, ray ban sunglasses, ray ban sunglasses, louis vuitton, michael kors outlet online, oakley sunglasses wholesale, christian louboutin outlet, louis vuitton, uggs outlet, louis vuitton outlet, polo outlet, prada handbags, nike free, chanel handbags, longchamp outlet, michael kors outlet, replica watches, louis vuitton outlet, oakley sunglasses, michael kors outlet online, prada outlet, michael kors outlet online, longchamp outlet, burberry handbags, michael kors outlet, kate spade outlet, ray ban sunglasses, longchamp outlet, louis vuitton outlet, oakley sunglasses, nike air max, oakley sunglasses, replica watches, ugg boots, polo ralph lauren outlet online, ugg boots, gucci handbags, jordan shoes, cheap oakley sunglasses, michael kors outlet online, christian louboutin uk, burberry outlet, tory burch outlet, tiffany and co, christian louboutin shoes

 
At 8:28 PM, Blogger oakleyses said...

michael kors, nike tn, ralph lauren uk, abercrombie and fitch uk, north face uk, ray ban pas cher, nike free uk, lululemon canada, michael kors, true religion jeans, coach outlet, coach outlet store online, hollister uk, sac longchamp pas cher, vans pas cher, nike blazer pas cher, louboutin pas cher, nike air max uk, michael kors pas cher, nike free run, nike air max uk, new balance, sac hermes, jordan pas cher, true religion outlet, replica handbags, nike roshe, longchamp pas cher, guess pas cher, true religion outlet, north face, polo ralph lauren, coach purses, hollister pas cher, oakley pas cher, timberland pas cher, air max, polo lacoste, nike air force, nike roshe run uk, burberry pas cher, converse pas cher, nike air max, sac vanessa bruno, mulberry uk, hogan outlet, michael kors outlet, true religion outlet, ray ban uk, kate spade

 
At 8:32 PM, Blogger oakleyses said...

beats by dre, nfl jerseys, nike trainers uk, mcm handbags, lululemon, reebok outlet, valentino shoes, wedding dresses, nike roshe run, celine handbags, ghd hair, ferragamo shoes, mont blanc pens, louboutin, giuseppe zanotti outlet, new balance shoes, timberland boots, oakley, soccer shoes, nike air max, iphone 5s cases, nike huaraches, iphone 6 plus cases, herve leger, iphone 6s plus cases, p90x workout, babyliss, vans outlet, north face outlet, iphone cases, jimmy choo outlet, iphone 6 cases, s6 case, abercrombie and fitch, bottega veneta, north face outlet, hermes belt, longchamp uk, ralph lauren, chi flat iron, insanity workout, iphone 6s cases, ipad cases, baseball bats, mac cosmetics, instyler, hollister, soccer jerseys, asics running shoes, hollister clothing

 
At 8:33 PM, Blogger oakleyses said...

doudoune moncler, pandora uk, moncler outlet, vans, converse outlet, montre pas cher, louis vuitton, moncler, moncler, canada goose, canada goose outlet, ugg uk, links of london, barbour uk, supra shoes, replica watches, lancel, nike air max, moncler, moncler, moncler outlet, coach outlet, wedding dresses, canada goose outlet, pandora jewelry, karen millen uk, ugg, marc jacobs, juicy couture outlet, converse, moncler uk, louis vuitton, ugg pas cher, swarovski, pandora jewelry, gucci, canada goose, canada goose uk, ugg,uggs,uggs canada, pandora charms, juicy couture outlet, louis vuitton, louis vuitton, ray ban, ugg,ugg australia,ugg italia, canada goose jackets, swarovski crystal, canada goose, hollister, thomas sabo, canada goose outlet, toms shoes

 
At 2:25 AM, Blogger dong dong23 said...

air max 90
ray ban sunglasses
michael kors handbags
fitflops sale clearance
jordans
ray bans
nike outlet store
louis vuitton outlet
louis vuitton outlet
michael kors handbags
basketball shoes
ralph lauren sale
oakley sunglasses
michael kors outlet
hollister clothing
replica watches for sale
michael kors bags
nike roshe flyknit
true religion outlet
kate spade
replica watches
adidas shoes
air max 90
cheap nfl jerseys
michael kors outlet online
adidas stan smith
jordans for sale
louis vuitton handbags
nike air max
jordans
adidas superstar
nike roshe runs
louis vuitton handbags
nfl jerseys wholesale
nike uk
louis vuitton outlet
coach outlet
air jordan 13
fitflops sale clearance
michael kors uk
20166.3wengdongdong

 

Post a Comment

<< Home