...`is awesome <https://nim-lang.org/blog/2020/06/08/static-analysis.html>`_.
I'm not sure I agree that a version of Nim with complete static analysis would be easier than Ada, though. My understanding is that one of the things that makes Ada hard is precisely its very tight static analysis.
(Sorry if someone already mentioned it; I didn't see a post.)
To develop Weave I took a poor man's Ada/Spark approach:
preCondition, postCondition, ascertain templates (names cleverly chosen to not conflict with requires and ensure). Those also report the thread that triggered the logic bug and gives lineinfo, wrong value and expected value details. This has been invaluable for debugging stuff like parent task being missing. In particular Nim templates and macro tend to eat stacktraces and Weave code transformations being a heavy user of macros, lots of traces disappear.
The second thing is to embrace the rise of the State Machines. I hope that one day I can formally verify the state machines produced by Synthesis but even then, having a self contained piece of code with the corresponding visual control flow / event triggers has been very useful to investigate livelocks, a situation where codepaths are mutually depending on each others (an hypothetical example would 2 threads sending the same task to each other repeatedly never actually working on it).
The third has been to actually use formal verification via TLA+ proving that my algorithm (a 2-phase commit algorithm to be able to put a thread to sleep) was deadlock-free and so that the deadlocks I had on Linux (and not Windows or Mac) were due to an implementation bug in Glibc and Musl and that they went away when I used Futexes instead of locks+condition variables: see investigation at https://github.com/mratsim/weave/issues/56
Disclaimer: this is a teaser for my talk at NimConf on debugging multithreading and proving that your concurrency is correct.
I didn't see a post
The post was in the making, but you were faster than me ;)
Thanks for posting it here, and thanks to @moerm for writing it!
You are all welcome
@cantanima
I disagree. Reasons, mainly:
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.
In the "Let's Prove Leftpad" repo, as a common programmer, I personally found the Dafny version to be the only one that looked reasonably familiar and approachable to me. I'm supper happy to see that what you show in the article seems to look similarly approachable too!
As to your reply above, I'm curious if Dafny is also mostly at the same place/compromise as Ada Spark?