Increased complexity of configuration tasks in computing systems has brought out automatic configuration management tools and high level languages for specifying configurations, such as Puppet, a popular configuration management tool, providing its own language. However, both configuration languages and the validations lack formalization that provides high confidence in their security. The correctness of configurations built in these tools is not guaranteed and especially there is little aid for correcting configuration errors. At most, their correctness relies on existing techniques or tools invented for other purposes besides the system, but these techniques are not integrated with configuration systems. As configuration languages are domain-specific languages with distinctive features, it is worthwhile to equip them with suitable formalisms. We propose to use formal semantics in programming language theory and “provenance” techniques rooted in database research to provide formalisms for understanding and correcting configuration errors.