Hey all, I see a branch on `arrow-meta` called `as...

# arrow

[Gavin Ray]

Hey all, I see a branch on arrow-meta called as-var-invariants

It seems to add some commits around pre, post and invariant functions.

Is this going to enable a DSL for a sort of Design-by-Contract style programming similar to Ada and D, where you can state pre/post-conditions of a method and invariants of a method or class?

If so, very exciting!

• https://github.com/arrow-kt/arrow-meta/commit/38f6850bbeab3e2df7fffbd1409d0415c57a0006#diff-0cba0892a09ca12cf39e0816[…]8d75d7633e5d6fce55dd30fbfc15e
• https://github.com/arrow-kt/arrow-meta/commit/64efe5e7fed1c98dfd9460c79ec02f0eb6477708#diff-d8893c41325132d95cc89c5a[…]6dd9ea55a0c7fc4413d35bfb1d0eb

[raulraja]

Hi @Gavin Ray, yes, this is an experimental plugin to bring SMT analysis capabilities to Kotlin’s and it implements exactly what you mentioned 🙂. We plan on releasing after the 1.0 release once we have a chance to test it.
It will ship with optional laws libraries for the standard library which will include all refinement laws for its functions and types.
We hope to autodetect cases like division by zero. unsafe access to collections and many of the common issues the compiler currently ignore but result in unsafe programs.

[raulraja]

Once it’s finished beside the pre, post and invariant DSL that covers all use cases we plan on natively supporting the Kotlin contract DSL and require and other known functions already that already denote pre conditions when in existing code bases.

[Gavin Ray]

Oh wow, that is incredible. I think this will be revolutionary to the entire language!

[Gavin Ray]

You're using satisfiability solvers/proofs over constraints by processing and modeling these?

[Gavin Ray]

Oh my goodness, there are ANNOTATIONS! THIS IS WHAT I HAVE ALWAYS WANTED, CONTRACT ANNOTATIONS!

@Pre(formulae = ["(< (int x) 10)", "(> (int x) 0)"])
      fun bar(x: Int): Int =
        x + 2
     
      val result = bar(30)
      """(
      withPlugin = { failsWith { it.contains("fails to satisfy its pre-conditions") } },
      withoutPlugin = { compiles }

[Gavin Ray]

Bless you all, I am shedding tears of joy.
See the bottom half of my comment here, from July. My prayers have been answered:
• https://github.com/Kotlin/KEEP/issues/259#issuecomment-882650719

[raulraja]

hahhaa yes, but the annotations themselves are just ment for serialization. The compiler plugin infers the constraints from the DSL and persists them with those annotations. You can write the annotations manually but the smtlib lang is not ment to be exposed directly to the user. The user just uses terms from the standard lib apis that are recognized inside the DSL and that the compiler plugins translates into smt formulae.

[mattmoore]

OMG this is nice! I haven't kept up lately but starting to look into Arrow again - bravo! 👏