K-user mailing list

[Dwight Guth <dwight.guth AT runtimeverification.com>]

It's really up to you. K has a fairly complex parser in terms of the functionality it supports, but it is also not the most performant. In many cases using concrete syntax rather than purely labeled forms can vastly improve the readability of the semantics, but often formalizing the grammar of a language in K is a nontrivial task, and if you already have a parser for the language that can be adapted to spit out KAST (K's abstract syntax), you may view it as an unnecessary effort, especially because such a parser will likely be much faster than a parser generated from K. I have seen languages successfully written in a variety of styles, from fully concrete syntax to nearly fully abstract syntax. That being said, K's refactoring tools are poor and you may find it more effort than you want to spend to change your decision at a later date.

On Wed, Apr 10, 2019 at 12:21 PM Dustin Wehr <dustin.wehr AT gmail.com> wrote:

For the purpose of evaluating the suitability of K for my company's
use case, I am wondering if I should expect to have an easier time
formalizing a fully-bracketed concrete syntax for our language (well,
for a minimal version of our language, but that's not what I'm asking
about). I understand that the general recommendation is to use one's
desired concrete syntax, but I don't think we need to use a nice
syntax at this stage in order to imagine what it will be like to later
have a K formalization that uses a nice syntax.

Thanks,
Dustin Wehr

--

Dwight Guth

Director of Engineering

Email: dwight.guth AT runtimeverification.com