Comment by eggy

Yes, that's the Yggdrasil project; you can use any port of Shen to create code in Shen bringing type checking to Python or JavaScript for example.

Does Gerbil really have a lot of real-world projects vs. Shen?

I am trying to use Shen for safety related control systems. It is more formal and verifiable than Gerbil. I started in SPARK2014 and I am just playing with Shen to see if it goes better.

The videos I linked to in another post in this thread show how you can use Shen to program front end stuff with the JavaScript port of Shen.