linked to me from https://twitter.com/cattheory/status/1220803662802489344 (by Joomy Korkut, PhD student in programming languages at Princeton https://cs.princeton.edu/~ckorkut/) — « not a language but a way to reason about C programs in Coq: VST lets you define separation logic predicates that describe how a Coq type would be represented in C: https://cs.princeton.edu/~appel/vc/Verif_reverse.html#lab32 \n\n might be interesting to you, or not, I don't know. » at 9:20 PM CET on Jan 24, 2020
The goal of the Ynot project is to make programming with dependent types practical for a modern programming language. In particular, we are extending the Coq proof assistant to make it possible to write higher-order, imperative and concurrent programs (in the style of Haskell) through a shallow embedding of Hoare Type Theory (HTT). HTT provides a clean separation between pure and effectful computations, makes it possible to formally specify and reason about effects, and is fully compositional. more...