Re: VWG and K, was Formatting of Language LRMs

Ivan Godard <>
Sun, 22 Jun 2014 21:47:28 -0700

          From comp.compilers

Related articles
Formatting of Language LRMs (Seima Rao) (2014-06-17)
Re: Formatting of Language LRMs (Ivan Godard) (2014-06-20)
Re: Formatting of Language LRMs (=?UTF-8?B?Sm9zaHVhIENyYW5tZXIg8J+Qpw==?=) (2014-06-22)
Re: VWG and K, was Formatting of Language LRMs (Ivan Godard) (2014-06-22)
| List of all articles for this month |

From: Ivan Godard <>
Newsgroups: comp.compilers
Date: Sun, 22 Jun 2014 21:47:28 -0700
Organization: A noiseless patient Spider
References: 14-06-010 14-06-016 14-06-021
Keywords: semantics
Posted-Date: 24 Jun 2014 11:46:19 EDT

> I did a bit of playing with K during a course a few years ago, and I
> ended up getting the feeling that the start of the art in executable
> semantics is such that we could start seeing languages written as
> executable semantics in maybe 10-20 years or so. While I did have a
> very large share of swearing and screaming at the tool for its
> deficiencies, I did leave the course actually feeling like I would
> want to use K if I had the chance, which is more than I can say for
> the few other attempts I've had at using formal methods tooling
> (disclaimer: the professor of said course led the development of K).
> Link: <>.

I have never played with K, but after a run through the doc it appears
to have much the same goal as VWG, but to be more imperative/pattern
oriented and less applicative than VWG. Either will be a steep ramp.

Anyone can do syntax; sugar is easy, but also immoral and fattening.
Semantics is much harder, but worthwhile. Stretch those synapses!

Post a followup to this message

Return to the comp.compilers page.
Search the comp.compilers archives again.