4 ms·

> using rewriting logic (Maude) instead of things like Coq or Isabelle/HOL. They seem to move faster on semantics as a result. This statement is close to nonse

> using rewriting logic (Maude) instead of things like Coq or Isabelle/HOL. They seem to move faster on semantics as a result. This statement is close to nonsensical. What are you comparing it to? Where is a comparable executable semantics project in Coq or Isabelle? This is great work, and they are definitely using the right tool for the job. But the field of "formal methods" is enormous, and you seem to be saying that apples are better than oranges.

nickpsecurity 9y ago
"What are you comparing it to? Where is a comparable executable semantics project in Coq or Isabelle?" In the others, they tend to do formal semantics of interpreters or compilers then extract them to ML or something. This group uses an executable, rewriting engine to do an executable semantics of a lot of languages which seems to require less people. Perhaps they're doing less on the verification side but what I've seen make me think more should try such methods. Most work I see posted in formal methods isn't done with rewriting tools like Maude. The ones I see use it get some interesting results for effort put in such as the SCOOP verification. So, I took the time to highlight that they use a different approach with quite a bit of tooling to use that people might want to look into trying. My 2nd reply, jcranmer, had exactly the kind of positive experience I was thinking readers might get out of a follow-up. "But the field of "formal methods" is enormous, and you seem to be saying that apples are better than oranges." You wouldn't notice it's enormous with the number of people that use a relatively-small set of tools. Convergence is usually good since ecosystems get built that can make new work easier. Coq and Isabelle/HOL are good examples where people keep plugging in prior work to new work. There's also quite a few more that don't get as much attention. Hence, me highlighting two (Maude and K) that had a series of practical results out of research using it.
solidangle 9y ago
Here is a Coq formalization of C11: http://robbertkrebbers.nl/research/ch2o/ http://robbertkrebbers.nl/research/ch2o/ It only covers a large fragment of C11, but they formalized the operational, axiomatic, and executable semantics and proved that these correspond to each other.
- tom_mellior 9y ago
  Yes, and there are other formalizations as well. But none of them (as far as I am aware) formalize the undefined parts in the way the featured article does. I think comparing projects with different goals and then saying "the differences must be due to the tools used" isn't solid reasoning.

nickpsecurity 9y ago

"What are you comparing it to? Where is a comparable executable semantics project in Coq or Isabelle?" In the others, they tend to do formal semantics of interpreters or compilers then extract them to ML or something. This group uses an executable, rewriting engine to do an executable semantics of a lot of languages which seems to require less people. Perhaps they're doing less on the verification side but what I've seen make me think more should try such methods. Most work I see posted in formal methods isn't done with rewriting tools like Maude. The ones I see use it get some interesting results for effort put in such as the SCOOP verification. So, I took the time to highlight that they use a different approach with quite a bit of tooling to use that people might want to look into trying. My 2nd reply, jcranmer, had exactly the kind of positive experience I was thinking readers might get out of a follow-up. "But the field of "formal methods" is enormous, and you seem to be saying that apples are better than oranges." You wouldn't notice it's enormous with the number of people that use a relatively-small set of tools. Convergence is usually good since ecosystems get built that can make new work easier. Coq and Isabelle/HOL are good examples where people keep plugging in prior work to new work. There's also quite a few more that don't get as much attention. Hence, me highlighting two (Maude and K) that had a series of practical results out of research using it.

solidangle 9y ago

Here is a Coq formalization of C11: http://robbertkrebbers.nl/research/ch2o/ http://robbertkrebbers.nl/research/ch2o/ It only covers a large fragment of C11, but they formalized the operational, axiomatic, and executable semantics and proved that these correspond to each other.

tom_mellior 9y ago
Yes, and there are other formalizations as well. But none of them (as far as I am aware) formalize the undefined parts in the way the featured article does. I think comparing projects with different goals and then saying "the differences must be due to the tools used" isn't solid reasoning.