I couldn't find any, even though formal semantics are included in R7RS-small. How come? Is there no value in it?
There is VLisp, which is a verified implementation of Scheme ( https://sci-hub.ru/10.1007/BF01128406 ). Rees' W7 kernel is also interesting ( http://mumble.net/~jar/pubs/secureos/secureos.html ). It's not formally proven, but definitely engineered for reliability. It lives on in Scheme48 ( https://www.s48.org/ ) which used to be my favourite Scheme impl, but seems moribund now.
But if you're interested in proving theorems, the simple ones of type theory seem relevant, so perhaps you should use a statically typed language?. I think CakeML is a better route to explore issues like this nowadays ( https://github.com/CakeML/cakeml ). On the other hand I'm slightly disillusioned with anything more complex than a SystemF-like type system with sums, products as in *ML or Haskell, etc. So if it looks like I have to prove general theorems in HOL, Coq or dependent types, I take a step back. This led me from CakeML to just SML.
>>2
I'm learning Coq right now, what's wrong with it? It is fascinating but I have to admit it does not seem very practical for software.
>>2,3
i can not read <qoc> without a giggle
therein lies my childlike heart
>>3
Coq (and HOL, and Z, and VDM) is great, I learned the basics myself. But that's more for personal interest, I think these techniques probably only make sense for 1-5% of software projects. That's what I meant by a "step back", I think a good static type system, e.g. *ML/Haskell, and contract-based development can get you 80% of the benefits but now your techniques are applicable to more than half of projects. And ML or Prolog is fairly widely taught around here, even though you could graduate with the impression that the toy subset you were taught is the whole language when actually they have everything needed to run industrial-strength projects.