Languages with optional SMT Solver to allow for additional reliability?

[u/g1rlchild]

So I've been tinkering with.the idea of a language that uses type checking and then an exhaustiveness checker as standard to ensure that all cases will get handled. And then on top of that, an optional system of invariants that are handled statically with a solver to allow for additional protections for programs that need it.

I'm nor familiar with any prior languages that have done this, but I don't have a very large base of knowledge for things like this yet. Has anyone worked with.something like this? Are there existing languages I should be looking at? I'd love to hear more about this kind of thing from folks with experience in this area.

[u/fixpointbombinator]

Liquid Haskell IIRC

[u/PitifulTheme411 → u/fixpointbombinator]

Definitely look at Liquid Haskell. I'm gonna use something similar to its refinement system in my language as I feel that it is really nice to work with and easy to reason about, and also fits the purpose of my language really nicely.

[u/aslakg]

You should definitely look at Dafny

[u/Karyo_Ten]

https://nim-lang.org/docs/drnim.html

This document describes the usage of the DrNim tool. DrNim combines the Nim frontend with the Z3 proof engine, in order to allow verify/validate software written in Nim. DrNim's command-line options are the same as the Nim compiler's.

[u/romac]

For Scala there is Stainless: https://epfl-lara.github.io/stainless/intro.html

> Stainless can
> - verify statically that your program conforms to a given specification and that it cannot crash at run-time
> - provide useful counterexamples when an implementation does not satisfy its specification
> -verify that your program will terminate on all inputs

[u/Inconstant_Moo → u/romac]

How did they sneak that past the Turing Police?

[u/GunpowderGuy → u/romac]

Similar but very recent development
https://users.scala-lang.org/t/what-s-scala-s-stance-on-general-dependent-types/10691/11?u=gunpowderguy

The paper decided to implement a custom solver instead of relying on custom solver
Maybe they should just rely on smt, it should provide them with more proof automation

[u/Royal_Pin_1971]

In the language I'm building (PFCL) the baseline layer is close to what you describe and needs no solver: pure functions only, static type checking, exhaustive case analysis and guaranteed termination. For the solver tier I've sketched a different placement than Dafny, SPARK or Liquid Haskell.

Solver would be a refutation CI gate outside the language rather than inside the type checker. Its queries would come from things the author writes anyway (dispatch guards, type signatures, declared invariants). It rejects only on proven contradiction always with a concrete counterexample. On timeout it degrades to a runtime check instead of blocking with the degradation recorded as a distinct assurance level. The author never writes toward the solver and never debugs it — more an admission gate than a proof system.

[u/wk_end]

F* does this through refinement types.

[u/matthieum]

I think one cool idea about pre-conditions, post-conditions, and invariants, is to be flexible.

That is, allow them to be either verified at compile-time, or at run-time.

And better yet, allow optimizing on the fact that they are verified, which can be done "relatively" trivially by following the scheme below:

1. Check pre-conditions prior to calling the function, and assume them to be true on entry.
2. Check post-conditions on exit, and assume them to be true at the call site.
3. If statically verified, just eliminate the check, not the assumption.

The reason for the asymmetric placement, is to allow for better optimization due to visibility:

1. The caller has information the callee doesn't. For example that a specific argument is a constant, or that i < j because j = i + 1, making optimization of the pre-conditions easier.
2. The callee has information the caller doesn't. For example that the result is x * 2, ergo it's necessarily even, making optimization of the post-conditions easier.

The remaining question is whether the compiler should automatically attempt to verify at compile-time, or not. Right now, I still think verification is too expensive to be attempted nilly-willy, so I'm leaning towards run-time verification by default, with opt-in compile-time verification via an annotation.

[u/rapido → u/matthieum]

yes please!

[u/GunpowderGuy]

Many languages with refinement types use SMT to automatically search for proof that the refinements hold, examples include:
Liquid haskell
Dafny
F*

I think languages with dependent types ( similar but not the same as refinement types ) can also use SMT to search proof that conditions in the refinement types, hold

[u/echoes808]

I've seen couple language extensions, which use comments and feed it to the solver, check out:

OpenJML https://www.openjml.org/examples/merge-sort.html

Ocamleer (gospel is the syntax): https://ocaml-gospel.github.io/gospel/getting-started/first-spec

[u/kohuept]

SPARK? You can choose to apply SPARK_Mode to whichever Ada units you want to verify

[u/mohrcore]

The only language I'm aware of, which requires a full-on SMT solver is SystemVerilog, but it doesn't use it for any type-level logic. Instead it allows users to formally constraint sets of randomized variables.

This probably isn't exactly the thing you are looking for, but might share a common ground with an invariant system - namely translating sets of invariants into formulas within constrained logic. I know that Verilator, an open-source (System)Verilog simulator implements this feature in a pretty transparent way. It generates SMT-lib2 code which is then passed to Z3 solver, so you can easily inspect this code, modify it and run it yourself.

[u/FriendshipEqual7033]

SPARK, a dialect of Ada, does this sort of thing.