[bitc-dev] Bitc/Hume

Tue Aug 8 04:21:34 CDT 2006

Hume was devised by Kevin Hammond and myself starting roughly in early
2000 as a way of making functional programming accessible outside the FP
ghetto by trying to actually deliver the many claims made over the years
for its closeness to formal methods. Since then, the Hume project has
blossomed beyond our widest hopes: we estimate that at least 25 people
in Europe (UK, France, Germany, Hungary, Portugal) are now working on
Hume with maybe $3.5M in national and EU funding.

Hume is oriented to the development of systems where precise resource
analysis is required, especially embedded systems. It is based on
concurrent finite state automata, termed "boxes" and connected by
"wires", controlled by pattern matching on inputs and recursive
expressions to generate outputs. The coordinatioin language is used to
define boxes, wiring, streams etc. The expression language is used to
define box actions and is reminiscent of SML or Haskell. The definition
language is used to define auxiliiary types, constants and functions
used in the coordination and expression languages. Hume has rich
polymorphic types and all the other features found in a contemporary
functional language.

Full Hume is Turing complete. Turing complete languages have interesting
properties which are undecidable. Languages with decidable interesting
properties have lousy expressibility and unpleasant syntax. So, we
distinguish different language levels in Hume with different
decidability properties depending on types on wires and constructs
generating outputs:
+ Full Hume - undecidable equivalence/termination/corerectness; poor
time/space bounds
+ PR-Hume (Primitive Recursive) - functions restricted to primitive
recursive - decidable termination; weak time/space bounds
+ Template Hume - no user defined recursion but higher-order functions -
decidable termination; good time/space bounds
+ FSM-Hume (Finite State) - no functions and only fixed precision/size
types - decidable equivalence/correctness; strong time/space bounds
+ HW-Hume (Hardware) - bits & tuples - exact time/space bounds 
Now, rather than imposing syntactic restrictions, and of course syntax
can't capture PR-ness, our philosophy is to provide analyses and
transformations between levels. If the analyses break or are not
accurate enough then we identify problematic constructs and invite the
user to transform them to something more analysable.

So far, there are excellent space cost models and analyses for HW- and
FSM-Hume, experimental space models & analyses for Pr-Hume. A time cost
model for HW/FSM is nearing completion and about to be incorporated into
an analyser. Hume is implemented via the Hume Abstract Machine (HAM)
which forms the locus for analyses but there is also ongoing work on
direct analysis of Hume source.

There is also a HW to Promela translator enabling model checking and
currently TLA for HW is being embedded in Isabelle.

Hume implementations are based on a common front end written in Haskell.
They include a reference interpreter based on the semantics, Hume to HAM
and a HAM interpreter, and HAM to C for compilation to Intel/PowerPC via
gcc and M32C via IAR. Oh there's also HW to Java and HW semantics in
Isabelle nearing completion.

The main application areas so far are vision/image processing and
autonomous control. We think it very important to have convincing,
realistic, hard application domains right from the start.

You can find a variety of Hume information via
http://www-fp.dcs.st-and.ac.uk/hume/index.html and
http://www.macs.hw.ac.uk/~greg/hume/

I'm sure Kevin will want to correct/augment this hurried account!

Best wishes

Greg

-----Original Message-----
From: bitc-dev-bounces at coyotos.org [mailto:bitc-dev-bounces at coyotos.org]
On Behalf Of Jonathan S. Shapiro
Sent: 08 August 2006 00:44
To: Discussions about the BitC language
Subject: Re: [bitc-dev] Bitc/Hume

[Greg writes]

> Having had a quick look at BitC I note some fundamental differences to
> Hume:
> a) it is Scheme derived so doesn't have rich syntax, especially
pattern
>    matching, but does have loads of reserved words

The surface syntax is actually not something that I like. It was
motivated by the desire for a simply quasiliteral pattern syntax.
Mainly, I already knew how to deal with that in an S-expression
language, and I didn't see any reason to redesign the surface syntax
while many other issues needed attention.

Recently, I have concluded that there is no need for an S-expression
syntax. I'm about to send a note to the list about this.

> b) it corresponds to the Hume expression layer but has no equivalence
>    to the Hume coordination layer i.e. boxes & wires

It is unfortunate that I know very little (or perhaps nothing) about
Hume. Where is a good place to start?

The BitC language specification today does not yet include any
specification for the logic language. I am not sure if this is relevant
to your comment.

> c) it is concerned with much more low-level fine detail than Hume

Yes. We are very concerned with low-level expressiveness. There are
several very talented language designers who are working on
verifiability of high-level, functional languages. Most are working on
pure term languages (where I consider Haskell's "monads" to fall within
the "pure term" idea).

The problem is (Mark Jones' work notwithstanding) that these languages
are not well suited to construction of systems code. The need for
operating systems, runtimes, and other high-performance low-level code
is not going away. There are both technical and social reasons for this.
The current state of the art in software verification has not paid a lot
of attention to this space (mainly because verification is already hard
enough by itself). The problem is that this leaves us standing in
mid-air building castles because our operating systems and runtime
systems are not verified or verifiable -- or even constructed in any
formally structured or principled way.

The BitC/Coyotos project is trying to make a small impact on this.

> d) it is closely tied to the Coyotos operating system project where
>    Hume is platform independent

BitC is not dependent on Coyotos in any way. Coyotos is simply the first
target application of interest. BitC is platform independent (the
bootstrap compiler generates portable C) and fully general.

[Kevin Writes]

On Mon, 2006-08-07 at 19:13 -0400, Jonathan S. Shapiro wrote:
> Yes, interesting.  As Greg says, it's a single-level language without
> coordination, though with a focus on explicit verification support.
> Unlike Hume, it has a built-in library for expressing program
properties
> (though concentrating on functional behaviour, I believe, rather than
on
> the time/space properties that we've mainly focused on in Hume), and
> seems to link the verification language with the program source.

I assume that "it" is referring to BitC.

We are moving to a two-level language. There is a level at which
programming occurs, and a meta-level at which theorems and properties
about the program will be stated. We have not yet started trying to
define the meta-level. Our goal is to get something that is structured
similarly to ACL2, but with static types and state in the programming
language.

> Unlike Hume, it includes imperative operations (I'd be interested in
> seeing what effect this has on verification -- this may weaken the
> proofs that can be constructed?)

The main impact is that our basis for discharge will need to be theorems
about the evolution of the state space rather than approaching the
problem through term substitution. This is, of course, a larger search
problem and we expect to hit many challenges.

We have been careful to preserve a pure subset language so that we can
switch back and forth between term-based and state-based reasoning as a
way to slice the search. I'm actually about to strengthen this aspect of
the language explicitly.

But I think that there is another thing to say here: it is better to
have weak proofs than no proofs. Right now, the number of systems that
can prove useful properties about things like operating system kernels
is zero. Jones' work on House is terrific, but everybody involved admits
that House is a toy (and that this was the right thing to do first). We
are approaching from the perspective of OS builders. Our objectives are
more aggressive and may not be realistic.

Perhaps our approach will not work, but if it does not we will learn
something about why not.

> and throw/catch exception handling.

Yes. However, throw/catch is not in the core language. There is a
straightforward whole-program rewrite that can entirely remove them. We
don't want to actually *do* that rewrite, but there is no new
foundational semantics introduced.

In fact, exceptions do not even require us to trigger value restrictions
(compare ML).

> It also includes type classes for overloading (something we've
avoided,
> because it can make costing harder -- again it would be interesting to
> see what this does for verification -- presumably the properties have
to
> be more general?).

I am not sure what you mean by "costing".

Certainly, any proof about an overloaded function must be suitably
quantified. However, as with Haskell, type classes are not part of the
core language. For whole-program analysis, at least, they can be
eliminated.

shap

_______________________________________________
bitc-dev mailing list
bitc-dev at coyotos.org
http://www.coyotos.org/mailman/listinfo/bitc-dev