Re:Certigrad: bug-free machine learning on stochastic comput...
by xgk on Tuesday July 11, 2017 @07:50AM
(#14743335)
Can this be done with Coq?
This can be done with any prover.
Simplifying a bit, an algorithm is a function of type A -> B. If you have two implementations, f1 :: A -> B and f2 :: A -> B, say one slow and simple (f1), one fast and complicated (f2), then you can verify that f2 does what it is supposed to do in two steps:
1. Show that for all a in A we have f1 a == f2 a.
2. Show that f1 meets the specification.
If you trust that f1 does what it is supposed to do, then you can skip (2).
Simplifying a bit, an algorithm is a function of type A -> B. If you have two implementations, f1 :: A -> B and f2 :: A -> B, say one slow and simple (f1), one fast and complicated (f2), then you can verify that f2 does what it is supposed to do in two steps:
1. Show that for all a in A we have f1 a == f2 a.
2. Show that f1 meets the specification.
If you trust that f1 does what it is supposed to do, then you can skip (2).