Is Type Checking Practical for System Configuration?

The paper describes ongoing work on a facet of software specification, namely system configuration, i.e. the specification of the structure of the system and of the operations needed to build it. We want to verify the adequacy of Higher Order Typed Functional Languages (HOTFULs), like Pebble [Lampson&Burstall 88], SOL [Mitchell&Plotkin 85] and other [Cardelli 85, Cardelli&Wegner 85], to model 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 such languages are indeed adequate. We are using the new configuration concepts for distributed systems introduced on top of Ada in the Cnet project [Inverardi&Mazzanti&Montangero 85, Cnet 85] as a case study, since they provide a good test bed being an enhancement of Ada advanced configuration facilities. The main result is that checking correctness of a Cnet configuration can be reduced to type checking in a suitable HOTFUL. However, the process is not straightforward enough, so that the question in the title is still open. As a side result, requirements have been assessed for a suitable HOTFUL: definability of (generally) recursive types, availability of the type of all types and of a peculiar inheritance mechanism.