The Design as its own proof

Dr. Daniel Selsam, of Microsoft Research, provides an example of interactive proof-assistants
being used to detect (semantic) implementation errors in Machine Learning systems

The ML system model persists as a Mathematical model encoded as rules or grammars in software
This method detects errors in the model once compiled because any errors in the program (and thus in the ML model) would cause the proof to fail

Adding another layer of logic to facilitate self-directed code-generation,
would allow an entire operating-system (or specification) to be maintained by a single engineer...

Developing Bug-Free Machine Learning Systems Using Formal Mathematics - Nov 5 2017