peteg's blog - hacking - isabelle - 2008 02 02 WorkerWrapper

1 +# 1 = 2⊥, or more mucking about with Isabelle's HOLCF.

Sat, Feb 02, 2008./hacking/isabelle | Link

It's been a while between drinks with HOLCF, and it didn't take me long to realise why; it's a massive time-sink and all one gets at the end is a proof unreadable by the mainstream and an awareness of vacuity. Here are some random observations that I will try to expand on later:

  • Brian Huffman gave me some help with treating unpointed domains, so I've begun cranking out a theory of a few ways to think about Nat. We'll see if that ever gets polished.
  • I was mucking about with those while trying to mechanise Andy Gill and Graham Hutton's worker/wrapper pre-paper. That went OK, modulo HOLCF's general unfriendliness towards numbers. I'll post the development when it's a bit more polished.
  • John Launchbury and Simon Peyton-Jones's Unboxed values as first class citizens is the most awesome concrete application of domain theory I've seen yet. Perhaps I should dig deeper into the abstract interpretation literature.
  • I was curious about Larry Paulson's mechanised verification of the unification algorithm in LCF, from the early 80s. Partial predicates? WTF is this? Larry's inimitable way of politely grinding his teeth made me realise just how much HOL brought to the table.
  • I managed to crank out a proof in HOLCF that "parallel or" and its friend "tell me if this function ever says yes" are continuous. So, err, just what is this domain theory modelling anyway? Those proofs were much harder yakka than I expected. Next step: Gordon Plotkin's notes on domains lists some cute sequentiality definitions that I'd like to understand.
  • In HOLCF we have (λx. ⊥) = ⊥, and one has to wonder just what that entails, coming from Haskell where it does not obtain.
  • Apparently some people are translating Haskell to HOLCF, and I have to wonder what the point is. There's a bit of a semantic gap, so many arbitrary modelling decisions to take, not much of a standard library, ... so there's lots of tedious stuff to do before you can prove your program is incorrect.

I guess I'll have to get back to real (economic) work one of these days.