How much time would it take? Human months?
How are formal specifications of programming language done? What to read to educate myself if I have such aim?
Is it possible for patient beginner to contribute/ to do that?
One thing is to go all the CompCert way and write formally verified compiler... but formalizing only the language seems easier.
if you want a verified LISP in Coq, one approach could be to port Milawa runtime ("Jitawa") from HOL4 to Coq: https://www.kookamara.com/jared/2011-itp-jitawa.pdf
C is a complicated language, so if you're interested in formal specs of practical programming languages, I recommend taking a look at CakeML:
For specifications of smaller languages, I recommend taking a look at Ott, which has export to Coq: github.com/ott-lang/ott
Last updated: Jan 29 2023 at 08:28 UTC