Visible to the public SPARK Language and Toolset: an intensive overview