Hacker News Reader

I'm on the fence about function contracts like this. I've seen them for a decade in other languages, but never really used them, so I can't say how I feel about them.

But having them be inside comments is just weird.

View on HN

It's a directive that happens to be placed at the tail end of a comment. Reading the documentation the doc comment stops being a comment-proper with the first @-directive, after that it's a list of directives. SPARK started in comments, ACSL is placed in specially marked comments. SPARK 2014 moved into Ada proper using Ada 2012 features (aspects). The difference between SPARK 2014's annotation and this is basically, are the annotations above the function or after the function declaration?

It is different yes, having read a good amount of it by now I find it work's pretty well in practice. It means you can incrementally adopt them if you like and code with or without them looks quite similar assuming you documented your code, the function signatures look the same as well which I appreciate.

Reply on news.ycombinator.com