Are you passionate about good design and specification? Excited by recent advances in programming languages and verification tools?
The science of deep specification (http://deepspec.org/) is the subject of a National Science Foundation initiative for cutting edge work on software and hardware specification that is both truly exact and implementation-independent.
"Deep" specification is semi-officially defined as • rich (describing complex component behaviors in detail); • two-sided (connected to both implementations and clients); • formal (written in a mathematical notation with clear semantics to support tools such as type checkers, analysis and testing tools, automated or machine-assisted provers, and advanced IDEs); and • live (connected via machine-checkable proofs to the implementation and client code).
Perhaps equally important, deep specification raises the level of abstraction of specifications, by applying concepts from software architecture. It is modular or layered, and aims at constructively defining not just an implementation but context-equivalent classes of implementations. According to the research overview (http://deepspec.org/research/), "the greatest pay-off will come in elucidating the conceptual basis of deep specifications as a technique for abstraction and modularity, with the potential for equal or greater practical benefit as from ideas like data abstraction."