4 ms·

Formally verifying the complexity of OCaml programs with CFML

31 points by lelf 11y ago

bdcravens 11y ago
The choice of language name is peculiar, since "CFML" has referenced the ColdFusion Markup Language since 1995? (looking at git log for this project, I see first commit in Nov 2014)
- mafribe 11y ago
  CFML stands for "Characteristic Formulae for ML". Characteristic formulae are a powerful concept of program logic. Simplifying a great deal, given a program M, a characteristic formula for M is a pair (A, B) of logical formula such that 1. {A} M {B}, i.e. if precondition A is satisfied, then the result of running program M satisfies postcondition B. 2. Whenever another program N satisfies {A} N {B} then M and N are contextually indistinguishable. In other words, the pair (A, B) specifies everything that can be said about M in the ambient program logic. Note that a program logic does not necessarily admit characteristic formulae for all programs. Program logics that do are 'in harmony' with the operational semantics in that the logic makes exactly the same distinctions about programs that the operational semantics makes. Characteristic formulae come the theory of communicating processes, see [1] for an overview. [1] L. Aceto, A. Ingolfsdottir, Characteristic Formulae: From Automata to Logic.
  - vog 11y ago
    While I appreciate your insightful comment very much, I don't see how it addresses the concern of the parent comment. (i.e. that the name "CFML" is already taken and thus may have the potential of confusion)
    - mafribe 11y ago
      Most (all?) three- and four-letter abbreviations are already used. Context disambiguates.
      - vog 11y ago
        Thanks for trying, but this still seems to utterly miss the point of the parent posting. The parent posting did not merely say that "CFML" is already used in some totally unrelated context. That complaint would be indeed pointless. Rather, they noted that there is another computer language with that abbreviation. So the context of both "CFML" is very close. Or, are you saying that it is never worth worrying about naming/abbreviation clashes, because you can always trust on the disambiguation by context?
        mafribe 11y ago
        CFML is not a computer language. It's two things: (1) a program that takes as input an ML program (more precisely a Caml program, i.e. Ocaml without objects) and computes the characteristic formula (expressed in the logic of Coq) of the program; (2) a Coq library, more precisely a library of Coq tactics, that enables users interactively to manipulate characteristic formulae of Caml programs in Coq. So Charguéraud's CFML is far away from cold fusion that context can always disambiguate. And if not ... is the sky going to fall down?
- nickpsecurity 11y ago
  I agree: CFML instantly will make people think ColdFusion Markup Language. Only reason I clicked it was that it said formal verification and Ocaml. Only a sadist would use ColdFusion for such a job lol... So, it should be fine in context but they do need to know using CFML associates them with something developers hate. Even in Google to a degree. Case in point: https://www.google.com/?gws_rd=ssl#q=CFML https://www.google.com/?gws_rd=ssl#q=CFML Although, putting Coq after it gets the right solution and meaning of acronym instantly: https://www.google.com/?gws_rd=ssl#q=CFML+Coq https://www.google.com/?gws_rd=ssl#q=CFML+Coq Then again, concerns about naming aren't new to the Coq community. ;) They might not care as people who would use it know the difference and can find it. (shrugs)

31 points by lelf 11y ago

The choice of language name is peculiar, since "CFML" has referenced the ColdFusion Markup Language since 1995? (looking at git log for this project, I see first commit in Nov 2014)

mafribe 11y ago
CFML stands for "Characteristic Formulae for ML". Characteristic formulae are a powerful concept of program logic. Simplifying a great deal, given a program M, a characteristic formula for M is a pair (A, B) of logical formula such that 1. {A} M {B}, i.e. if precondition A is satisfied, then the result of running program M satisfies postcondition B. 2. Whenever another program N satisfies {A} N {B} then M and N are contextually indistinguishable. In other words, the pair (A, B) specifies everything that can be said about M in the ambient program logic. Note that a program logic does not necessarily admit characteristic formulae for all programs. Program logics that do are 'in harmony' with the operational semantics in that the logic makes exactly the same distinctions about programs that the operational semantics makes. Characteristic formulae come the theory of communicating processes, see [1] for an overview. [1] L. Aceto, A. Ingolfsdottir, Characteristic Formulae: From Automata to Logic.
- vog 11y ago
  While I appreciate your insightful comment very much, I don't see how it addresses the concern of the parent comment. (i.e. that the name "CFML" is already taken and thus may have the potential of confusion)
  - mafribe 11y ago
    Most (all?) three- and four-letter abbreviations are already used. Context disambiguates.
    - vog 11y ago
      Thanks for trying, but this still seems to utterly miss the point of the parent posting. The parent posting did not merely say that "CFML" is already used in some totally unrelated context. That complaint would be indeed pointless. Rather, they noted that there is another computer language with that abbreviation. So the context of both "CFML" is very close. Or, are you saying that it is never worth worrying about naming/abbreviation clashes, because you can always trust on the disambiguation by context?
      - mafribe 11y ago
        CFML is not a computer language. It's two things: (1) a program that takes as input an ML program (more precisely a Caml program, i.e. Ocaml without objects) and computes the characteristic formula (expressed in the logic of Coq) of the program; (2) a Coq library, more precisely a library of Coq tactics, that enables users interactively to manipulate characteristic formulae of Caml programs in Coq. So Charguéraud's CFML is far away from cold fusion that context can always disambiguate. And if not ... is the sky going to fall down?
nickpsecurity 11y ago
I agree: CFML instantly will make people think ColdFusion Markup Language. Only reason I clicked it was that it said formal verification and Ocaml. Only a sadist would use ColdFusion for such a job lol... So, it should be fine in context but they do need to know using CFML associates them with something developers hate. Even in Google to a degree. Case in point: https://www.google.com/?gws_rd=ssl#q=CFML https://www.google.com/?gws_rd=ssl#q=CFML Although, putting Coq after it gets the right solution and meaning of acronym instantly: https://www.google.com/?gws_rd=ssl#q=CFML+Coq https://www.google.com/?gws_rd=ssl#q=CFML+Coq Then again, concerns about naming aren't new to the Coq community. ;) They might not care as people who would use it know the difference and can find it. (shrugs)