Path: csiph.com!newsfeed.hal-mli.net!feeder3.hal-mli.net!border3.nntp.dca.giganews.com!backlog3.nntp.dca3.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!news.iecc.com!.POSTED!nerds-end From: Ivan Godard Newsgroups: comp.compilers Subject: Re: VWG and K, was Formatting of Language LRMs Date: Sun, 22 Jun 2014 21:47:28 -0700 Organization: A noiseless patient Spider Lines: 18 Sender: news@iecc.com Approved: comp.compilers@iecc.com Message-ID: <14-06-022@comp.compilers> References: <14-06-010@comp.compilers> <14-06-016@comp.compilers> <14-06-021@comp.compilers> NNTP-Posting-Host: news.iecc.com Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 7bit X-Trace: miucha.iecc.com 1403624780 96990 2001:470:1f07:1126:0:676f:7373:6970 (24 Jun 2014 15:46:20 GMT) X-Complaints-To: abuse@iecc.com NNTP-Posting-Date: Tue, 24 Jun 2014 15:46:20 +0000 (UTC) Keywords: semantics Posted-Date: 24 Jun 2014 11:46:19 EDT X-submission-address: compilers@iecc.com X-moderator-address: compilers-request@iecc.com X-FAQ-and-archives: http://compilers.iecc.com X-Original-Bytes: 2116 Xref: csiph.com comp.compilers:1277 > 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!