An assessment of system configuration by type cheking

We want to verify the adequacy of Higher Order Typed Functional Languages (HOTFULs), like Pebble, SOL and the like, with respect to a specific facet of software specification, namely modelling the configuration facilities of modern languages for system programming like Ada, Chill and Modula-2: no thorough study has been done in this direction, even if the literature is full of small scale sketches, which are used to claim that they are indeed adequate. We are using as a case study the advanced configuration concepts for distributed systems introduced on top of Ada in the Cnet project. The main result is that the configuration of a Cnet system can be expressed in a suitable HOTFUL, and that the problem of the correctness of the configuration can be reduced to type checking: It turns out, however, that the process is not straightforward enough, so that the question of how much these languages are suitable for system configuration is still open, and needs further experimental investigation. As a side result, requirements have been assessed for a suitable HOTFUL: definability of (generally) recursive types, availabilty of the type of all types and of an inheritance mechanism.