  Imprecise and incomplete specification of system \textit{configurations}
threatens safety, security, functionality, and other critical system properties
and uselessly enlarges the configuration spaces to be searched by configuration
engineers and auto-tuners. To address these problems, this paper introduces
\textit{interpreted formalisms based on real-world types for configurations}.
Configuration values are lifted to values of real-world types, which we
formalize as \textit{subset types} in Coq. Values of these types are dependent
pairs whose components are values of underlying Coq types and proofs of
additional properties about them. Real-world types both extend and further
constrain \textit{machine-level} configurations, enabling richer, proof-based
checking of their consistency with real-world constraints. Tactic-based proof
scripts are written once to automate the construction of proofs, if proofs
exist, for configuration fields and whole configurations. \textit{Failures to
prove} reveal real-world type errors. Evaluation is based on a case study of
combinatorial optimization of Hadoop performance by meta-heuristic search over
Hadoop configurations spaces.
