Interactive theorem proving is the modern way of formalizing mathematics using a computer as a proof assistant, helping solve simple tasks and keeping an order on the proofs. Still, it is a tedious task, as such mechanical proofs contain detail that humans do not want to see. When it comes to the verification of real world applications in software engineering, as required for the assurance of safety and security properties of embedded systems, the level of detail becomes even more annoying. In fact, it is a gargantuan task to prove a program correct or prove that an implementation...
Interactive theorem proving is the modern way of formalizing mathematics using a computer as a proof assistant, helping solve simple tasks and keepi...