That's exactly what Ada2012 and SPARK2014 did. You write your contracts (preconditions, postconditions, assertions, contract-cases, invariants, type predicates) in Ada syntax and you get both runtime assertions and proof depending on which tool you call (compiler or prover). You give more facts when proof fails. You can tag code as 'ghost' and it's only available for proof tools...

To be able to be a bit more 'terse' in assertions, they added quantifiers, expression functions, case- and if-expressions. Lots of small improvements to allow contracts, that are finally a boon to write simpler and clearer code.

Everything you're asking for here is available in Ada2012 and SPARK2014.

also what https://github.com/facebookexperimental/MIRAI does for rust: you add contracts (preconditions, postconditions, and invariants) using https://docs.rs/contracts/0.6.0/contracts/ and it checks whether they are true

here is an example using mirai and contracts:

https://github.com/facebookexperimental/MIRAI/blob/master/ex...

(note: the contracts crate can be used for verifying at runtime as well)

Ah yes, the power of rust's macros.

I think there is danger in proposing 'assume' without at least trying to prove it and say you're wrong. I think in spark 'assume' is a guide, but it is checked and it is great, because footguns.

C# has https://docs.microsoft.com/en-us/dotnet/framework/debug-trac...

But honestly it's not that great of a user experience, though it does seem to have been improved at least a little bit since the last time I used it in ~2016 or so.

Code Contracts are mostly abandoned AFAIK.

I think Perl 6 aka Raku allows this, you can say something like `Person but $age < 18`.

The `but` keyword takes an instance and something to mix into it.

So you can say something like this:

    0 but True

---

Since `True` is a `Bool` it automatically creates a role that has a method `Bool` that returns `True`.

    my $role = role { method Bool { True }}

You can do that manually if you want.

    0 but role { method Bool { True }}

---

It creates a new subclass of Int and mixes in the role.

So:

    0 but True

Is roughly equivalent to:

    do {
      my constant but-true = anon role { method Bool { True }}
      my $class = anon class :: is Int does but-true {}

      $class.new( 0 )
    }

I think the you mean: `subset Minor of Person where *.age < 18`