You are all welcome @cantanima
I disagree. Reasons, mainly: a) Ada is intrinsically harder to work with. Likely reasons are its age (decades older than Nim) and some almost anal typeing problems, probably also due to its age; in a way J. Ichbiah had to try to emulate SA in the language itself back then. b) one can make SA syntax (and working) hard and ugly or one can make it reasonably human friendly. I have reason to assume that Nim's SA will be quite "friendly" (well, as friendly as is feasible considering that "mathematically rigorous" and "easy to grasp and use" aren't easy to mate). Moreover I'm pleased to see that @Araq goes at it in his usual way, i.e. profoundly reflecting, thinking through it as well as interested in mortal human usability. From what I know I'm very confident that our (Nim's) SA will be both rigorous (which is highly desirable in SA) and "easy" to use. One must keep the context in mind, i.e. compare our SA to what others offer. Real world: (almost all) SAs are either unsatisfactory (superficial, picking out only the easy stuff) -or- hard to very hard to use. Just look at Frama-C which is a PITA to install and use and which needs _very_ elaborate annotations to work at all. As far as I'm concerned (Ada's) Spark is by far the best compromise and about the only SA that's actually used even without pressing need. From what I know Nim's SA will feel similar to Spark. Summary: Sorry, SA just isn't easy as in "hacking some javascript or PHP junk" but I have reason to believe that Nim + Nim's SA will be actually useable for mere mortal developers after some (not to steep) learning and getting used to it. Btw, if there are questions re. my article feel free to shoot them at me.
