# [Solidity Language Design Discussion] NatSpec for Formal Specifications #10825

_27.01.2021, 4:30PM - 5:30PM CET (Berlin time)_

Discussion on next steps for [issue #10825](https://github.com/ethereum/solidity/issues/10825).

### Attendees
Akos H
Alex B
Chris R
Dimitar B
Joran H
Leo A
Martin L
Valentin W
Goncalo S
Franziska H

### Notes

- Joran: Initial motivation of the issue was to discuss using NatSpec to standardise specification language annotations, could be useful for several tools
- Leo: Several aspects need to go together, otherwise they might diverge too much; let's create a general common minimum
- Akos: Pre- and post conditions, invariants and basic Sol expressions as starting point
- Valentin: Agrees that a minimal language would be nice, but e.g. Scribble does not have preconditions; there are different desing choices possible; not sure where the convergence is, maybe it would be worth trying different approaches first before trying to define the common denominator
- Leo: Could become chicken & egg thing if remains undefined for too long
- Valentin: There is no common specification lang yet and there is imo no easy way to integrate it into the compiler; usually standardization just takes a really long time; it will be a compromise, not everybody will be happy with it; let's try to collect empirical evidence what's essential before defining it
- Akos: Likes Dejan's proposal of common format + more custom spec
- Alex: 2 opposing positions: 1st doesn't want to do any type checking; spec tag + dialect
- References issue [#8146 on custom NatSpec tags](https://github.com/ethereum/solidity/issues/8146)
- Joran would like to have NatSpec tags for the mentioned reasons
- Valentin: Custom NatSpec tags could also be a first step and then work out the next iteration, still in explorative stage
- Dimitar: Several stages of general @spec (tool undefined) and @spec (with tool defined) to check whether parsing and typechecking is possible
- Chris: How exactly could the tools (e.g. Scribble) benefit from a simpler implemenation in the compiler? How would you work with an export (eg. AST node has XY tag)
- Akos: Returning an AST would help so that the tools would not need to reinvent parsing
- Chris: But you would still have to take the sol code and modify it?
- Dimitar: That would be the task of the tool, - Chris: you're working with a mix of parsed and unparsed content?
- Dimitar: Yes
- Alex: Wouldn't it be better if the JSON AST would keep all the comments from the source code and keep it included?
- Dimitar: Good idea, if you exclude NatSpec tags that would be useful, if you follow NatSpec tags you get more, if you also follow syntax you get even more etc.
- Chris: Would it help to do some sort of identifier solution?
- Dimitar: Yes that would help, also it would help if the compiler would not fail if not finding the identifier
- Chris: Compiler has to ignore any syntax anyways
- Chris: Don't think it's a good idea to agree on a fixed grammar
- Alex: Check free text for anything that resembles a variable name
- Chris: Reminds me of an old feature we wanted to have in the past: parsing and evaluating a contract Without inserting it into the source code
- Akos: This is what we are doing but in a hacky way
- Dimitar: Yes would be very useful
- Chris: This is most useful if you can keep the context of the compiler alive
- Alex: couldn't you pass in a list of snippets at the same time? hypothetically if we would expose all the comments in the AST; then you can do your own parsing on the comments
- Dimitar: How do you point the scope in a snippets format?
- Chris: By AST ID or filenum;
- Alex: Issue for that is ["Compile external code snippets #1272"](https://github.com/ethereum/solidity/issues/1272)
- Chris: Currently, the set of NatSpec tags is fixed but we were thinking of opening it up
- Alex: But is NatSpec even useful here? it's quite decoupled from the AST
- Joran: NatSpec would be useful because people are using it already to put "meta" information about the functions; it's not meant to make tool dev easier but rather encourage adoption of writing specifications
- Alex: Dejan made a good point about people being confused about the huge selection of tools and how to choose; that's why common language could make sense; if we go to the route of NatSpec there should be a common lang, which again would take time to get there
- Leo: Maybe the first common lang would just be natural lang; add a a new tag, maybe decide on some syntax / format (tag, tool, message), it would be nice to have something to start with, but there should also be some commmon ground, e.g. @spec
- Valentin: It would be great if there was a common format, we are not against that, it's just that we have this discussions for a long time already, it's hard to agree on this "common" stuff, going with something that is undisputed, semi-formal or natural lang, free form, would be good
- Matin: We can work into both directions, I also want to recognize there is a little interoperability in require/asserts; and then expanding towards more static asserts
- Valentin: there is some sort of duplication that we also observe; having clear seperation what is interface Specification and how you enforce it at run-time is not a bad idea
- Martin: Static assert could be useful there
- Goncalo: Pros / cons of doing it in NatSpec vs just getting the commenting to the AST
- Valentin: Pro NatSpec: make specs more visible, doc generators, tools would show it, verification exposure
- Goncalo: How I understood Dimitar having comments in the AST would already be a big benefit correct?
- nodding
- Valentin: Both would help, keeping comments in the AST could be the 1st step, adding it into NatSpec could be the 2nd step, formalizing it even further 3rd step
- Chris: All the three features are useful for other things too so it is justified to do them
- Leo: Doing it in NatSpec would really give more visibility to the subject
- Joran: From the user's perspective using NatSpec would be a first step to a more uniform experience
- Alex: Risk with NatSpec: if we don't have an agreed common subset... if we allow custom tags, the risk is that people can make mistakes; tools could warn them but not the compiler, currently the NatSpec is quite strict; once we have a common subset it would need to be bound to the compiler version
- Valentin: Is your concern backwards compatibility?
- Alex: Right now no link between NatSpec and the AST; this needs to be solved anyways
- Alex: IMO dialect (spec tag with dialect) required is better than custom (arbitary) tags
- Leo: @spec scribble invariant x > 1;
- Chris: Disadvantage here is it's a bit verbose
- Chris: Another way could be just having one tag at the beginning "add verification tool"
- Leo: I think I would use different tools in the same source code
- Valentin: main benefit of core language would be easy for users to try out different tools (at least for core constructs)
- Joran: Yes but you would still have different dialects, thinking of creating a "translator" for different backends
- Martin: Should we also come up with a minimal subset of the language for the dialects?
- Joran: That would be interesting, could be a working group
- **Leo: How about we start with ``@spec dialect message`` and in parallel we start running examples and see how things look and eventually agree on minimal lang**
- Chris: Only at locations where NatSpec is allowed?
- Dimitar: For now sufficient
- Martin: I would find it useful in different places, too
[...]

We've agreed on steps forward, let's continue the discussion on more next steps another time!