The Alloy Analyzer is a tool developed by MIT for analyzing models written in Alloy, a simple structural modeling language based on first-order logic. Alloy can be used to detect conceptual mistakes in the model before the coding starts. Scientific American has published an article about it.
MIT Alloy and Software Dependability
Submitted by ganges master 2007-01-21 General Development 2 Comments
Seems like you need to write code twice. Translating alloy code to real program code can introduce errors, too.
Better compilers and debuggers maybe will do more to make software more reliable.