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...
R. Dapoigny, and P. Barlatier. Proceedings of the 21th International Conference on Conceptual Structures (ICCS 2013), volume 7735 of Lecture Notes in Computer Science, page 135-152. Springer, (2013)