Sorry to hear you had issues with my comment system. Comments are invisible until I manually approve them, but I'm not seeing anything new in the database right now. Did you get any sort of error code? The system should let you know if e.g., the answer to the captcha was wrong.
I do mention SPARK at the end of the article. I'm not familiar with Frama-C so I'll check that and your blog posts out. Thanks for sharing!
Sorry I missed the mention of SPARK. TLA+, although I haven't fiddled with it as much, is more similar to Alloy than anything else. SPARK actually works on Ada code.
Author, here. The n ≈ 163 pages figure I give for R6RS includes the standard library and description of formal semantics.
I'd like to clarify that I didn't mean to imply that larger standards are worse. Quite the opposite, actually. That's why I enjoy R6RS. As shakow pointed out, it's a means of giving a rough estimate of size. Common Lisp has much more than Scheme in terms of what's included.
I agree. Using GTK+ for a small personal project made me realize just how unwieldy GObject is. Vala was a nice alternative, in my opinion, but it seems that everyone is trying to kill it off nowadays.
I do mention SPARK at the end of the article. I'm not familiar with Frama-C so I'll check that and your blog posts out. Thanks for sharing!