Re:Coq 8.6 is out
by pron on Thursday December 15, 2016 @08:11AM
(#13184323)
> You think that's useless voodoo?
No, but I also think it's just not worth the effort for 99.99% of software. It's neat that it can be done when absolutely necessary, but that's not where most of the benefit of formal methods can be had. Also, you don't need many certified compilers, so the techniques used to construct them need not be scalable.
> SCADE is great, and it's "formal methods" in the sense that you write your program as a formal model with clear semantics that can be reasoned about. But it's not the kind of proof the OP asked about, I think.
Well, they wrote "I would image that certain languages are easier to prove (haskell vs C)", and SCADE is easier to formally reason about -- be it with a model checker, static analysis or deductive proofs -- than Haskell. Usually, languages with very simple semantics are easier to reason about either automatically, manually or semi-automatically, and the languages that are used in the industry in formal methods (except static analysis) -- even if the formal methods used aren't deductive because that's just too costly -- are those that really are "easiest to prove".
No, but I also think it's just not worth the effort for 99.99% of software. It's neat that it can be done when absolutely necessary, but that's not where most of the benefit of formal methods can be had. Also, you don't need many certified compilers, so the techniques used to construct them need not be scalable.
> SCADE is great, and it's "formal methods" in the sense that you write your program as a formal model with clear semantics that can be reasoned about. But it's not the kind of proof the OP asked about, I think.
Well, they wrote "I would image that certain languages are easier to prove (haskell vs C)", and SCADE is easier to formally reason about -- be it with a model checker, static analysis or deductive proofs -- than Haskell. Usually, languages with very simple semantics are easier to reason about either automatically, manually or semi-automatically, and the languages that are used in the industry in formal methods (except static analysis) -- even if the formal methods used aren't deductive because that's just too costly -- are those that really are "easiest to prove".