The Golo Galaxy has recently be extended by a new project: Hardened Golo.
This sub-project aims at giving some trust into a Golo program by formally proving their correctness. This project has been initiated with the help of two interns: Bertrand CAYEUX and Raphaël LAURENT.
Bertrand starded the work and made a first proposition based on a translation of Golo into Java in order to use Krakatoa in front Why to verify a Golo program. He introduced the specification language name “JGolo”. Afterwhat, Raphael continued the work and developped Hardened Golo Version 0.1. He tried to make a direct translation of Golo program into WhyML.
Welcome on board Hardened Golo! :D