Semantics of C in K Framework | Hacker News Reader

Semantics of C in K Framework

github.com

48 pointspabs310 comments

https://kframework.org/ has high level details. It says "K is a rewrite-based executable semantic framework in which programming languages, type systems and formal analysis tools can be defined using configurations, computations and rules. "

I was confused by the git repo because I thought the "K" was referring to https://en.wikipedia.org/wiki/K_(programming_language) which is a terse APL-style language.

yeah me too, probably should change its name.

Pawing through this github account, it appears that they've been using the name for about 10 years. I wouldn't suggest renaming the project, but the link title could be clearer if it read "C in the K Framework"

Yeah same

The K framework is a tool to help verify semantics of languages- there are definitions for WASM, Ethereum VM, lisp, java etc.

Tbh I thought a lot of of the development had moved to K-Maude, guess I was wrong :)

http://fsl.cs.illinois.edu/pubs/serbanuta-rosu-2010-wrla-sli...

What is the form of the program produced by this, is it native x86 or does K provide some sort of runtime/vm style elements?

Does it fully encode all semantics? Since typically formal verifications have issues with floating point stuff (hence why we STILL don't have complete formal models of C even in 2019).

What is the performance like compared to traditional compilers?

And to me the most important, what things can we suddenly do with K that we can't easily do with a combination of other tools, since it seems that it can do a lot more but this isn't really explained all that well to an outsider IMO.

Usually it isn't about execution of programs, but analysis of their properties.

To do so you can use eg model checking, and you require a semantic definition for doing so.

I don't recall floating point stuff being hard to encode. See eg the flocq project.

What's wrong with CompCert's floating point model?

The highest profile project that has been using the K framework for formal specification and formal verification is likely Ethereum:

- The K EVM, the execution environment of Ethereum Smart Contract: https://github.com/kframework/evm-semantics

- Formal verification of the Beacon Chain, the Proof-Of-Stake consensus and finality protocol for Etheruem 2.0 phase 0: https://github.com/runtimeverification/beacon-chain-verifica...

The title should certainly be changed to better reflect the project, though the paper is certainly enjoyable to read

Reply on news.ycombinator.com