The most interesting features of DiSTiL, at a glance, are presented in this slide.

DiSTiL is a highly factored library and the data structures to be constructed are described as compositions of primitive components. These compositions are checked statically to ensure their validity. We assign attributes to components and test logical conditions on these attributes. This is a design check -- not a semantic check. It only verifies that our components will work together (to the extent that our conditions capture this). If the components themselves are correct and our conditions are accurate then the code is correct.

Also, in DiSTiL, data-structure operations are presented intentionally, using retrieval predicates. In other words, the programmer does not have to specify which elementary structure to use for a certain operation and in which way (e.g. “get the first element of the doubly linked list defined on this field and follow the next pointers of the elements till you find ...”). Instead, the programmer assigns a predicate to each retrieval (e.g. “all elements that have this age”) and the system determines how to satisfy this predicate in an “optimal” manner.