So, your thread is about other programming languages applied to the cryptography field or the general modeling of cryptographic protocols?
If the first is true, then I would say that: formalization is not profitable. To apply a formal proof to a piece of code much effort is required, and not many people are willing to spend so much workload on this task. We have had some great advancements on this area, specially concerning topics like dependent types and automated formal proffers (such as Isabelle/HOL) but, still, too complex for normal people.
Also, about language, most of the languages used in cryptography, at least on the primitives, is checked by hand. If you go to some mailing list like the "moden crypto" you'll find threads about this. People there usually write the code in assembly.
I do agree with you, though, that some abstraction layer could help. For example, there's two main problems that could have a better focus from the community: language checking and compilers.
The language checking, such as the ones implemented in dependent-type languages (as in Idris and ATS), or external checkers, like the simplified C subsets that can be more easily parsed for checking and optimization (see OpenPAT).
If the second is true, then I would say that some efforts is already been done, like the SeLF Project:http://www.cs.cmu.edu/~self/
But, from my (not-so-trustworthy) opinion, there would be a need to go meta on this. Not just analyze the interaction between sets, but also watch is "from above" and see what is the main model actually doing, and see if it's really optimized or is a mess. That's the point with projects evolving Modeling Languages, such as UML (unified modeling languages).
These fields are not so explored because of two main reasons: is from the basis/complicated and it's not profitable. The first refer to the point that the study of this subject is actually the basis of all other knowledge. It comes from questioning the basics of logic itself, and going on the philosophy of logics, the metalogics, and analysing not just how is it's usage on practical mathematics, but also questioning: what is mathematics? Isn't it just an abstraction? Kurt Godel is one very interesting read if you want to think about it, and also Agrippa's trilemma and constructivism (realizability).
ps. too much text. people will not even read all this soykaf... but, look, you still here!