|
|
|
|
|
|
by trealira
1052 days ago
|
|
|
> To me the "formal" aspect of their spec starts after the output of the hs-to-coq compiler, which isn't a verified compiler. I already have to trust coq, in which about a paradox a year have been discovered(maybe less now), and which isn't small (about 20k lines minimal core iirc). Trusting an additional compiler and a language subset(some total Haskell subset) is stretching it formality wise. I'm a bit confused from my lack of knowledge here. If it's fed into Coq, why does the origin of the code matter? As it's a proof assistant, wouldn't it reject invalid proofs of validity (assuming you fully trust Coq)? Shouldn't it be fine even if the code is randomly generated by monkeys on typewriters? |
|
|
The subject of discussion was whether an executable specification in F# or Haskell are also formal specifications. While Haskell is based on System FC, a type of lambda calculus, there are many additions and quirks, and as far as I know no mechanised metatheory, or even complete language semantics stated in one document. There are also some language features known to make Haskell inconsistent in the logical sense, not to mention that turing completeness makes any language inconsistent as a logic. In the paper linked above authors call their multipurpose specification in Haskell formal, while I don't like it, they have their reasons and justifications (total, non-turing complete subset of the language, haskell's metatheory scattered across papers, System F, which is well established). But to me when one sees some formal statement, the shorter is the path to the trustable foundation the better, and in statements in Haskell I see all of the issues above, plus possibly bugs in the language. If there were proofs of correctness/soundness of hs-to-coq compiler and of Haskell metatheory I couldn't have found reasons to complain. (But then it would have been better to invest this effort into verifying a hardware specification DSL to coq translation or embedding) As the result, what one would have to trust in this situation is the translation of this Haskell spec to coq, not the spec itself, considering that in this setup you have to prove theorems in coq anyway, and guarantees of the proven theorems only work for coq definitions. So Haskell's spec is seen by me as a superfluous entity, that only complicates things and lowers trust. You are correct that a proven statement is coq doesn't depend on the source from which boilerplate was generated, but you would have to trust the statement in coq, and not the "spec", and that's a fail for a formalization in my eyes. I suspect (did't check) that the translation and language subset they chose are trivially translatable to coq and they don't use anything particularly questionable, but the superfluousness doesn't go away.