As you probably can tell Maude sets out to solve a different set of problems than ordinary imperative languages. It is a formal reasoning tool, which can help us verify that things are "as they should", and show us why they are not if this is the case. Maude lets us define formally what we mean by some concept in a very abstract manner, but we can describe what is thought to be the equal concerning our theory (equations) and what state changes it can go through (rewrite rules). This is useful to validate security protocols and critical code. The Maude system has proved flaws in cryptography protocols by just specifying what the system can do , and by looking for unwanted situations the protocol can be showed to contain bugs, not programming bugs but situations happen that are hard to predict just by walking down the "happy path" as most developers do. We can use Maude's built-in search to look for unwanted states, or it can be used to show that no such states can be reached.