Wikified aptitude TODO list.

I've been able to crib more time lately for Debian, so I'm hoping that I can stop just keeping my head above water (barely) and start on the pile of new work that I'd like to do. For a while I've been accumulating a mental list of stuff that sucks in aptitude, but mental lists have the drawbacks that no-one else knows about them and that they never seem to be available when I want them.

I've now got a nice page in the Debian wiki holding aptitude's current TODO list. The entries range from changes that are trivial but will improve the user experience, to deep and difficult changes that no-one will notice. Since I don't expect a team of magic pixies to do the coding for me, I figure I might have the majority of the design and coding done in a year or so.

How *not* to impress your customers.

So, today I tried to sign up for a service online (unidentified for reasons that will become obvious briefly). This is a service that, had I successfully signed up, would be withdrawing monthly subscription fees from my bank account and handling some data that's fairly important to me. But when I hit the button to start the registration process, I got back...

[TCX][MyODBC]You have an error in your SQL syntax. Check the manual that corresponds to your MySQL server version for the right syntax to use near ''7GDiSp=E8-Mgvgo\', Now() )' at line 9

SQL = "INSERT INTO [REDACTED] ([REDACTED], FieldName, FieldValue, update_dt ) VALUES ( 10724, 'PASSWORD', '7GDiSp=E8-Mgvgo\', Now() )"

The password I tried to enter, for the record, was 7GDiSp=E8-Mgvgo\#dEwb8m7Ec_e~z0myAAj. This is at best inexcusable sloppiness and at worst a security hole, and I don't want a company that does either anywhere near my money and data. (sadly, there probably are already many such companies near my money and data, but I try to avoid the ones I know about)

coq's -ness-nesses

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

toy-ness

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

programming-language-ness

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.
   

OCaml-ness

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!

Wikipedia is case-sensitive, who'da thunk?

This is part of my ongoing series of posts wherein I am the last person on the planet to discover various things. (this is not a planned series, it's just how life is. :) )

If I ask Wikipedia about Virtual Server, I get an article about a Microsoft Hproduct. If I ask it about Virtual server, I get a page on server virtualization. Presumably if you know enough Wiki-lore, this makes sense.

Unsurprisingly, neither article gives me a clue about how I might go about renting a virtual server to avoid the hassle of maintaining hardware or which providers (if any) are reasonably trustworthy.

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.