Understanding ELF using readelf and objdump talks about how dynamic linking works in ELF. It also introduces a nice tool, biew, which has a nicer interface to view binaries.

I also noticed other tools such as elfsh and elfutils.

Don't forget the links of the article and the link I gave is the third page.

As a side note, I kind of understand the surface of the so-called Curry-Howard Isomorphism now. Of course gotta read http://lambda-the-ultimate.org/node/1115.

In my way of thinking, a type system is a programming language at the type level; Omega gives you the ability to write programs at all levels: type, kind, ... The essential idea is that types provide a second version of your program; one that operates on value abstractions (the abstraction is a Galois connection among domans, see Cousot 1997). So, with two programs, the checker's job is to ensure that the two versions (the value-level and the type-level) correspond. Omega checks all the levels.

Usually, people only provide type annotations, because the checker can build most of the program (i.e. the proof of type evaluation). Inferable type systems mean that the checker can build the entire proof/type-level program from the value-level program (NB. not all type-systems are inferable). Dependent types work in this description by explicitly breaking the (often overlooked) belief that programs are two-phase (cf. Cardelli 1988). REPLs give another great example of how strict two-phase distinction forces extra closure properties (witness the heavy use of `rec' definitions in SML/OcaML--but I believe that System E might reduce this).

But, since types provide property-level descriptions (programs), they're *tremendously useful* for checking that the value-level program meets these properties. These properties might include proving that qsort provides a permutation of the original values into a monotonic order; most type systems only let you prove that you take a list/array of elements and return a list/array of elements of that same type. In Omega, you can write a type program that expresses that valuable qsort property, or a type program as part of your interpreter that says your interpreter enforces a sound type system.

Alternatively, you could say that a programming language is a specification language at the machine level. After all, a program is simply a specification of the behavior that we want a computer to exhibit.

Now, I'm not trying to claim that a programming language is necessarily a "good" (for some value of "good") specification language. I'm simply trying to point out that specification languages and programming languages are (in some senses) essentially the same thing. For some reason people seem to feel the need to separate them somehow - perhaps because "specification" isn't all that popular. But really programming is just a form of specification. The imaginary line between programming and specification becomes particularly blurry once we start talking about functional and logic programming languages, and high-powered type systems.

Ultimately what we are doing, no matter what "level" we are operating at, is formally expressing notions about some pieces of data (our universe of discourse), the fundamental relationships between those pieces (our axioms), and some procedures for manipulating that data in accordance with our axioms. The goal of verification (whether by proof, static checking, or testing) is to demonstrate that there is some preservation of structure between different levels of abstraction.