APPLYING AN INTERACTIVE PROGRAM-PROVER LIKE COQ CAN BECOME A NEW STANDARD FOR APPROBING OF PRACTICALLY IMPORTANT THEORETICAL WORKS

There are some theories in the world, which have great scientific and practical importance but have no approbation. In the article the theory of “widened long flip-flop” (that represents scientific and practical interests in the field of building mission-critical computing system) is used as an example to analyze reasons of such situation and ways of solving this issue. These ways appear with powerful interactive program-prover like Coq. Such prover may either prove or do not prove the theory since it depends on human prompts. But if the proof is successful, the correctness of the theory will be guaranteed.