The Maude system is an implementation of rewriting logic. It is similar in its general approach to Joseph Goguen's OBJ3 implementation of equational logic, but based on rewriting logic rather than order-sorted equational logic, and with a heavy emphasis on powerful metaprogramming based on reflection. Maude is free software, and tutorials are available online. It was originally developed at SRI International, but is now developed by a diverse collaboration of researchers. Introduction Maude sets out to solve a different set of problems than ordinary imperative languages like C, Java or Perl. 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. In other words, Maude lets us define formally what we mean by some concept in a very abstract manner (not concerning ourselves with how the structure is internally represented and so on), 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). Maude modules (rewrite theories) consist of a term-language plus sets of equations and rewrite-rules. Terms in a rewrite theory are constructed using operators (functions taking 0 or more arguments of some sort, which return a term of a specific sort). Operators taking 0 arguments are considered constants, and one constructs their term-language by these simple constructs. Maude lets the user specify whether or not operators are infix, postfix or prefix (default), this is done using underscores as place fillers for the input terms. Reduction equations are assumed to be confluent and terminating. Rewrite rules do not have this restriction. When Maude "executes", it rewrites terms according to the equations and rewrite rules. Maude rewrites terms according to the equations whenever there is a match between the closed terms that one tries to rewrite (or reduce) and the left hand side of an equation in our equation-set. A match in this context is a substitution of the variables in the left hand side of an equation which leaves it identical to the term that one tries to rewrite/reduce. Equations and rewrite rules can also be conditional rules, which means they have to fulfill some criteria to be applied to the term (other than just matching the left hand side of the rewrite rule). The rules are applied at "random" by the Maude system, meaning