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).
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).
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.
ted_dunning|1 year ago
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|1 year ago
puzzledobserver|1 year ago
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|1 year ago
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|1 year ago
These ideas have not caught on for a reason. You end up writing the logic twice, and pretty high chances you mess up once.