While I prefer declarative languages, it is also interesting to note very simple imperative languages are often the easiest to verify formally (as transition systems).