A modern programming language that makes developers happier.

kotlinlang

I'm curious why this syntax was adopted: `return z.post({ it &gt; 0 }) { "greater than 0" }` where the string is in a block, rather than a parameter. It seems less visually noisy to write as `z.post("greater than zero") { it &gt; 0 }` - yeah it's different to require, but it seems to make more sense

this is mostly to follow the syntax for Kotlin’s own `require` blocks

<https://kotlinlang.org/api/latest/jvm/stdlib/kotlin/require.html>

the main benefit is that the lambda is lazily evaluated, so no allocation happens unless the condition is broken

That's true _for require_ but isn't true here, right? I thought pre/post are just hints to the SMT solver, they don't actually get compiled into the production code?

currently it does if you want it to be considered by Arrow Analysis

indeed having the string inside `{ }` is not needed for Analysis, but we still decided to do so for consistency