search

gnolang / gno

Gno: An interpreted, stack-based Go virtual machine to build succinct and composable apps + gno.land: a blockchain for timeless code and fair open-source.
https://gno.land/
Other
900 stars 377 forks source link

proposal: code-tested specs #1125

Open thehowl opened 1 year ago

thehowl commented 1 year ago

From a discussion arising from #1111; relates in many ways also to gnolang/hackerspace#37 (which could be the test suite talked about)

The proposal is that in order to concile the need for a text-based, human-readable and understandable spec, as well as a more "exact" and definite approach, using an authoritative code as the reference for all other implementations ("the code is the spec"), we could try to strike a middleground wherein we have Markdown-based specs where each paragraph (or, more generally, "statement") has to have a number of matching tests which show the behaviour for that claim.

For an expression x of [interface type](https://go.dev/ref/spec#Interface_types),
but not a [type parameter](https://go.dev/ref/spec#Type_parameter_declarations),
and a type T, the primary expression

    x.(T)

asserts that x is not nil and that the value stored in x is of type T. The notation x.(T)
is called a type assertion.

[tested-by]: # (typeassert_nil typeassert_no_typeparams typeassert_structs)
[tested-by]: # (typeassert_interface typeassert_pointers ...)

The individual names in tested-by make reference to files present in a known directory, and are filetests like the ones we currently use, as well as Yaegi. (note this is just to try to adapt the more general idea from Marc of having a full test suite for Go, as well as for Gno gnolang/hackerspace#37 ).

This way, we can clearly state that any implementation that adds support for understanding the tested-by syntax, is not only able to automatically verify full conformance to the spec by executing the tests; additionally, if there are any failing tests, they can be traced down to specific points in the specification which are not respected.

This would have to come with adequate linters (for instance, all tests must refer to at least a statement in the spec). Tools could also allow to interactively show the content of tested-by "comments", ie. an accordion which can show the referred examples and their outputs.

In other words, we respect the principle of "the code as the source of truth", or spec, by stating: a compliant specification is anything that passes the tests (without using Volkswagen tricks). Passing the tests is a more reliable indicator of a good implementation than following the spec to the letter, which should be seen more of a "secondary source of truth", or a "glorified comment".

An alternative proposal by @moul was to flip this on its head, and instead generate the spec from the comments in test files.

package tests

// For an expression x of [interface type], but not a [type parameter], and a type T,
// the primary expression
// 
//  x.(T)
// 
// asserts that x is not nil and that the value stored in x is of type T. The notation x.(T) is called a type assertion.
// 
// [interface type]: https://go.dev/ref/spec#Interface_types
// [type parameter]: https://go.dev/ref/spec#Type_parameter_declarations 
func TestTypeAssertions(t *testing.T) {
    // ...
}

(note: since 1.19, pkg go/doc supports converting godoc comments to Markdown )

I personally think that any kind of specification should need to be worked directly in its markdown (or anyway, source) file rather than generated from code, in order to ensure proper structure and organic presentation (which is something that becomes more bureaucratic if it's reliant on test files being structured in a given manner). Also, this creates a 1-1 relationship between doc and test, while I think a single test could verify multiple statements.

moul commented 1 year ago

cc @gfanton who was thinking about this while working on #1117.

moul commented 1 year ago

Related with https://github.com/gnolang/gno/issues/1215.

ajnavarro commented 1 year ago

I personally think that any kind of specification should need to be worked directly in its markdown (or anyway, source) file rather than generated from code, in order to ensure proper structure and organic presentation

Fully agree.

I think specs cannot be the code because the code is alive. Specs have to be resilient to make them that, specs that anyone can implement for interactions between different implementations. Maybe we could create some tests from the spec to check that is implemented correctly or something like that.