3 ms·

Because the code will literally not compile if it isn't correct. As opposed to weaker languages where bugs (run-time problems) can exist. I'm still something

Because the code will literally not compile if it isn't correct. As opposed to weaker languages where bugs (run-time problems) can exist. I'm still something of a layman on this, and I know less about formal specification languages like TLA+, but languages like Coq work by using things like dependent types. Here's an example: if you have a method that takes (through specifying type parameters) an Int and returns an Array of Integers, and it compiles, then you have effectively proven that it is possible to take an Int and return an Array of Integers. This is not particularly useful to the method author that is only using that method signature to write some more specific business logic. Dependent types allow you to spruce up that method signature until it actually reflects your business logic. So then you know that if it compiles, the actual intent of your method/function is bug free. Yes, it is true that there is a "turtles all the way down" element to this kind of thing - "how do they prove that this real source code is correct?" The answer is that languages like Coq rely on a small kernel of code that cannot be proven. It's like their axiom from which everything flows. But the kernel is small enough that people verify it with eyeballs. Bugs can still happen there, and I think they even found one a few years ago, but it didn't have any impact on all the mathematical proofs that have been written using Coq. I'm sure some experts can jump all over what I just wrote but that's the gist as I understand it so far.

munin 11y ago
> proven that it is possible to take an Int and return an Array of Integers. proving that something is POSSIBLE is very easy: just write this function in an untyped language and call it with an int, and show that you get back an array. proven: it's possible. static type systems give you something much stronger: the guarantee that, always, Int -> [Int]. sometimes languages weaken this to exceptions, sometimes, certain kinds of exceptions. these systems are pretty straightforward, we've had them for a while, and they're even in environments like c++ and java. the "dependent types" area of the world that you talk about is more exciting: a desire to push more information about the program, as a specification, into the type system. so for example session types are a technology by which you can encode the state machine of a network protocol into the types of data values and functions. then, if your state machine is correct, and the process of translating the state machine into a session types implementation is correct, you can prove that your implementation is a correct implementation of a given protocol. the dynamic typing half of this, as I understand it, is contracts. you write executable guards around the beginnings of functions that check, at runtime (usually), that the environment the function is in is something the function expects. both of these technologies come from, I think, the same place: the desire to control the steps that a program makes during runtime. static type systems don't permit programs to be compiled that could take invalid steps, dynamic type systems don't permit programs that run to advance past an invalid step.
schoen 11y ago
Is the Coq bug you're thinking of this one, from earlier this year? https://github.com/clarus/falso https://github.com/clarus/falso
- tel 11y ago
  That wasn't really in the core verifier exactly. It was more like an optimization.

munin 11y ago

> proven that it is possible to take an Int and return an Array of Integers. proving that something is POSSIBLE is very easy: just write this function in an untyped language and call it with an int, and show that you get back an array. proven: it's possible. static type systems give you something much stronger: the guarantee that, always, Int -> [Int]. sometimes languages weaken this to exceptions, sometimes, certain kinds of exceptions. these systems are pretty straightforward, we've had them for a while, and they're even in environments like c++ and java. the "dependent types" area of the world that you talk about is more exciting: a desire to push more information about the program, as a specification, into the type system. so for example session types are a technology by which you can encode the state machine of a network protocol into the types of data values and functions. then, if your state machine is correct, and the process of translating the state machine into a session types implementation is correct, you can prove that your implementation is a correct implementation of a given protocol. the dynamic typing half of this, as I understand it, is contracts. you write executable guards around the beginnings of functions that check, at runtime (usually), that the environment the function is in is something the function expects. both of these technologies come from, I think, the same place: the desire to control the steps that a program makes during runtime. static type systems don't permit programs to be compiled that could take invalid steps, dynamic type systems don't permit programs that run to advance past an invalid step.

schoen 11y ago

Is the Coq bug you're thinking of this one, from earlier this year? https://github.com/clarus/falso https://github.com/clarus/falso

tel 11y ago
That wasn't really in the core verifier exactly. It was more like an optimization.