Path: csiph.com!v102.xanadu-bbs.net!xanadu-bbs.net!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!border4.nntp.dca.giganews.com!backlog4.nntp.dca3.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!news.iecc.com!.POSTED!nerds-end From: =?UTF-8?B?Sm9zaHVhIENyYW5tZXIg8J+Qpw==?= Newsgroups: comp.compilers Subject: Re: Formatting of Language LRMs Date: Sun, 22 Jun 2014 21:12:50 -0500 Organization: A noiseless patient Spider Lines: 23 Sender: news@iecc.com Approved: comp.compilers@iecc.com Message-ID: <14-06-021@comp.compilers> References: <14-06-010@comp.compilers> <14-06-016@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 1403489747 70676 2001:470:1f07:1126:0:676f:7373:6970 (23 Jun 2014 02:15:47 GMT) X-Complaints-To: abuse@iecc.com NNTP-Posting-Date: Mon, 23 Jun 2014 02:15:47 +0000 (UTC) Keywords: standards Posted-Date: 22 Jun 2014 22:15:47 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: 2229 Xref: csiph.com comp.compilers:1276 On 6/20/2014 2:09 PM, Ivan Godard wrote: > VWG is vastly superior to BNF because it provides a formal specification > of semantics, in particular the type system, which cannot be expressed > in BNF. Unfortunately formal reasoning about semantics is beyond many > users. Stll IMO no other formal semantic notation (Denotational > Semantics for example) is superior to VWG. 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: . -- Beware of bugs in the above code; I have only proved it correct, not tried it. -- Donald E. Knuth