Passive syntax for static analysis

[leonardo]

I know this exists: https://www.pm.inf.ethz.ch/research/prusti.html

But I've never used it (it's not friendly to use). But lately I've used some times the WhyML language: http://why3.lri.fr/

I convert a (simple, not parallel, not concurrent) Rust function to that ML variant (and this is easy enough to do), then I (very slowly) add annotations (and sometimes I modify the code a little to make it more fit for the static analysis) to prove some of its functional proprieties. LLVM is able to remove few array bound tests, but not all of them. So I use Why3 to prove those array/slice accesses are always in-bound. This doesn't prove that the array accesses in the original Rust code is correct (because translation by hand introduces some bugs) but it's still good enough. In some cases if my brain works well enough I try to prove some other functional propriety of the code (often the limit is my skills and my patience, it's not Why3)

In Python3 they added "type hints", they do nothing: https://docs.python.org/3/library/typing.html

They give a nice syntax that extenal programs (like MyPy, Pyre, Pytype, and the PyCharm editor) use to perform static type checking. The type hints syntax helps to avoid the decorated comments usually used where there isn't a specific syntax, like {-@ ... @-} in LiquidHaskell ( https://ucsd-progsys.github.io/liquidhaskell-blog/ ) and so on, and to avoid the need to use the "compiled" (type annotations stripped) version generated like by TypeScript.

After a while it's possible to fold the external program inside the interepreter (and to run it optionally) if there's enough consensus and desire.

A disadvantage of having a built-in syntax for the external static analyzer is that it freezes the kind of static analysis you usually want to perform in your programs. If you introduce syntax for type predicates like LiquidHaskell and WhyML ones then later you probably can't use that syntax for very different things like dependent typing. 10-15 years from now if the preferred way to prove some correctness of the code will be like LiquidHaskell.

Still, refinement typing isn't controversial stuff, I think it will last some time. So what do you think about introducing in Rust some nice built-in syntax (that gets ignored as Python3 type hints) to be used to verify the code with external programs?

I am thinking about:

lemma {}
requires {}
invariant {}
ensures {}
variant {}
measure fn
predicate fn

Plus just inside the logic formulas it's also allowed:

->
<->
forall
exists
Old()

I think this amount of syntax could cover 99% of future usages of refinement typing (and all contract-based programming, see in C++: http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2017/p0542r0.html it also introduces "audit" and "axiom", that I have omitted in Rust because the purpose is different).

[steffahn]

I don’t quite understand how this all is relevant for rustc. If you want to do something different to compiling ordinary Rust code, wouldn’t you use a different tool that could very well generate ordinary rust code (i.e. the same code with the extra annotations stripped down)? As far as I can tell, this is the same with LiquidHaskell which is independent from Haskell compilers.

Regarding syntax, looking at Prusti they seem to use Rust’s attribute syntax. In this context, could you please elaborate on your point:

@leonardo

it's not friendly to use

Is it something syntactical or just the tool (or the fact that you never used it) that’s the reason you see it as “not friendly to use”?

I think if you want to have something added to the rust language you should be more clear about the benefits of making the addition “officially” part of the language and you should be more specific as to what form of support from the rust compiler you expect in handling the added syntax you propose.

[leonardo]

@steffahn

I don’t quite understand how this all is relevant for rustc .

Right, I missed a small note in my post: I think that one of the major selling points of Rust is that it allows to write correct code. Reducing usage friction of static analysis could help this. TypeScript shows you don't need built-in syntax, Python3 shows it's handy to have.

@steffahn

I think if you want to have something added to the rust language you should be more clear about the benefits of making the addition “officially” part of the language

Right, a true proposal should have a more robust section of justifications.

@steffahn

and you should be more specific as to what form of support from the rust compiler you expect in handling the added syntax you propose.

The Rust compilers should just ignore those annotations, if their syntax is correct. Years later if there's desire the external verifiers could become part of Rust compilers.

[Ixrec]

@leonardo

The Rust compilers should just ignore those annotations, if their syntax is correct.

This sounds like RFC 2103 Tool Attributes.

Looks like it's been accepted for two years but still not ready for stabilization. So I think this is just yet another thing to add to the pile of "we all need to stop designing new features and finish implementing the several hundred features we already designed."

[leonardo]

I am talking about syntax like requires {} without any other extraneous stuff like # etc.

[Ixrec]

So... is the suggestion a purely syntactic one to replace e.g. #[prusti::requires(...)] with requires { ... } someday?

All the stock negative responses I'm sure you've seen before to syntax sugar proposals seem to apply here, so I assumed there was more than that.

[kornel]

TypeScript is a compile-to-JS language. There could be a similar compile-to-Rust language which wouldn't require Rust to know about its syntax. It's doable today.

If Rust stabilizes a way to create Spans in proc macros, it'll be possible to make almost seamless integration that makes rustc show errors in correct places even when the input syntax is quite different.

[CAD97]

On top of the other notes: this isn't required, because we have macros!

Just create some package, say, proof-annotations, that provides simple strip-everything macros:

macro_rules! lemma {
    {$($tt:tt)*} => {};
}
// and so on

And then your external analyzer tool can look for calls to proof::lemma! {} and treat that however it would've treated lemma {} if rustc had first-class "dead syntax space" for this.

By using macros for statement position and attributes for annotating, you already have a fully generic space to put whatever extra information in already that rustc doesn't even need to care about.

[jjpe]

@leonardo

that gets ignored as Python3 type hints

Sounds like it'll have all the downsides but none of the upsides, from Rust's point of view: if this idea is implemented, Rust would have to maintain syntax that describe semantics, that are not enforced (so no safety provided by rustc w.r.t. that), but it would have the burden of supporting the syntax just the same.

Python can get away with that because there's no compile time checking whatsoever anyway, leaving all relevant errors to be detected at runtime. Therefore no expectations are violated.

But Rust is an entirely different beast. The big issue is the externality. If Rust describes syntax, and attaches semantics to that syntax, then I expect that based on those syntax and semantics, rustc can tell me when I'm writing illegal constructs. This necessarily means Rust needs to have an actual implementation for the semantics behind the syntax.