[nextos]

Automation of Hoare logic is quite good these days. Dafny, from MS Research (https://dafny.org), is probably the most friendly formal language of any kind. It's built around Hoare logic and its extension, separation logic. The barrier of entry is low. A seasoned imperative or functional programmer can get going with Dafny in just a few days. Dafny has been used to verify large systems, including many components of AWS.

I am hoping that LLMs make more advanced languages, such as Liquid Haskell or Agda, less tedious to use. Ideally, lots of code should be autocompleted once a human provides a type signature. The advantage of formal verification is that we can be sure the generated code is correct.

[petschge]

How do you encode the difference between a method that adds and a method that multiplies two numbers in the type signature?

[ted_dunning]

It is hard to understand what you mean by type signature, but I think what you mean is something like the type signature in Java, Go or C.

That isn't what people are talking about when they talk about formal verification with a type system. They are talking about much more complex type systems that have equivalent power and expressivity to formal logic.

This intro is good at introducing the topic. Unfortunately, the correspondence between advanced type systems and logic is itself fairly abstract and uses lots of concepts in non-intuitive ways. This means that you can easily wind up in a situation where you can do lots of proofs about number theory using a tool like Lean4, but you don't really see the corresponding types (this is what happened to me).

https://leanprover-community.github.io/learn.html

[lmm]

With dependent types, if you really want to. (Or just with conventional generics or typeclasses, the difference between a ring and a monoid will show, and that's enough for many cases).

[puzzledobserver]

If you ignore syntax and pretend that the following is a snippet of Java code, you can declare that a variable x always holds an int, like so:

var x: int = y + 5

Here x is the variable being defined, it is declared to hold values of type int, and its initial value is given by the term y + 5.

In many mainstream languages, types and terms live in distinct universes. One starts by asking whether types and terms are all that different. The first step in this direction of inquiry is what are called refinement types. With our imaginary syntax, you can write something like:

val x: { int | _ >= 0 } = y + 5

Once again, x is the variable being defined, it is declared to always hold a value of type int at all relevant instants in all executions, and that its initial value is given by the term y + 5. But we additionally promise that x will always hold a non-negative value, _ >= 0. For this to typecheck, the typechecker must somehow also confirm that y + 5 >= 0.

But anyway, we have added terms to the previously boring world of types. This allows you to do many things, like so:

val x: int = ... val y: int = ... val z: { int | _ >= x && _ >= y } = if x >= y then x else y

We not only declare that z is an integer, but also that it always holds a value that exceeds both x and y.

You asked for the type of a function that multiplies two numbers. The type would look weird, so let me show you an imaginary example of the type of a function that computes the maximum:

val f : (x : int) -> (y : int) -> { int | _ >= x && _ >= y } = ...

This doesn't really get you to the maximum, because f might be computing max(x, y) + 5, but it does show the idea.

The final step in this direction is what are called full-blown dependent types, where the line between types and terms is completely erased.

[schoen]

> This doesn't really get you to the maximum, because f might be computing max(x, y) + 5, but it does show the idea.

Perhaps { int | _ >= x && _ >= y && (_ == x || _ == y) } ?

I just proved in Coq that if all of these always hold for a function, the function coincides exactly with the max function.

[fooker]

Basically weird type systems that encode pre/post conditions.

These ideas have not caught on for a reason. You end up writing the logic twice, and pretty high chances you mess up once.