5 ms·

> You express your specification as types (theorems), and your implementation proves those theorems. Then your code is correct by construction. This is a true s

> You express your specification as types (theorems), and your implementation proves those theorems. Then your code is correct by construction. This is a true statement; it isn’t open to debate, not being a matter of opinion. That's technically correct, but a little bit divorced from reality. Let's say I want to write a function that counts the primes below one million. Since that's a function with no arguments that returns a single integer, the corresponding theorem by Curry-Howard is that "at least one integer exists". The function "return 0" is a proof of that theorem. That doesn't seem too useful! You might argue that we should use a richer type system to express the specification. Sure! We just need to express the idea of "primes below one million" in the type system. But that's at least as difficult and bug-prone as writing the program in the first place, so I have a hard time seeing the benefit. Most real world functions are the same way. Say you're programming a game and you need a function to fire the gun. Play the sound, add some screenshake, create a bullet object, etc. Go ahead, express that as a theorem. Don't forget to come back and tell us what you gained by doing that.

codemac 12y ago
Um, maybe you missed the point about dependent types? You can express a function, that takes no arguments, that returns primes below 1,000,000 as it's type! That's kind of the point of the talk, and is supposed to be possible in languages like Agda and Idris (I don't know enough about them to give any syntax here). See jules' comment below about how curry-howard does not mean your implementation is a full proof as well. Considering code that flies planes and shoots guns generally is written using proofs on control systems (if not required by law), your examples are a bit weak.
- AnimalMuppet 12y ago
  But the "proofs" of those control systems isn't anything that looks like a type system, is it? (An argument of the form "due to Curry-Howard, all proofs are type systems" will be regarded as uninteresting at best.)
  - codemac 12y ago
    Absolutely not, at least not to me. I'm not a huge type theory guy or anything. But saying that "proofs are a burden especially for things with side effects like shooting a gun" when systems that shoot guns specifically do have proofs in spite of their type systems invalidates the example, if not the argument. The presenters certainly think these languages will help construct those proofs.. that I'm less certain of.
- cousin_it 12y ago
  It seems to me that using dependent types to express the type "the number of primes below one million" would take at least as much code, and be at least as error-prone, as writing that function in a dynamically typed language directly. In fact I'd be surprised if the dependently typed version were less than 2x the size of the direct version.
  - codemac 12y ago
    This is why they brought up the language that uses the same syntax for types as it does for your function definition. It really sounds like you haven't played with Coq or Agda.. because expressing these things are not that much code at all. Also the presentation literally covers that complaint, and how they think more programming languages are needed.
- kestert 12y ago
  The constructive nature of Idris makes it hard (at least for me) to express a prime under 1,000,000 as a type. For example, it's trivial to express a composite as a GADT: data Composite : Nat -> Type where factors : (x : Nat) -> (y : Nat) -> Composite ((S (S x)) * (S (S y))) but there is no analogous construction of a prime type. Luckily most day to day programming looks more like the composite case than the prime case.
  - gergoerdi 12y ago
    As an example, here's how primality is defined in the Agda standard library. It is simply the negation of the property 'has a divisor and is greater than 2'. http://agda.github.io/agda-stdlib/html/Data.Nat.Primality.html http://agda.github.io/agda-stdlib/html/Data.Nat.Primality.ht...
AnimalMuppet 12y ago
Let's go further. If I'm writing, say, numerical calculations, types can save me from getting kilometers when I expect miles (or, worse, kilograms). What it can't do is save me from numerical instability, round off errors, and a whole host of other problems known to the field of numerical analysis. If my code is calculating the angle of a control surface on a plane, the type system is not going to say anything about whether I get 40 results every second. Without those constant, timely updates, the plane is going to crash. A robust type system means that "your code is correct by construction"? That seems incredibly naive. There's more ways for programs to be wrong than are provable via a type system.
- Confusion 12y ago
  Concerning 'numerical instability': with a sufficiently advanced type system you should be able to save yourself from something like numerical instability. You could e.g. ensure all numbers have an 'order of magnitude type' and define operations between 'order of magnitude' types to raise errors for certain (ranges of) combinations. However, there is (AFAIK) no convenient way to express this in any language, let alone without performance suffering greatly.
eli_gottlieb 12y ago
>You might argue that we should use a richer type system to express the specification. Sure! We just need to express the idea of "primes below one million" in the type system. But that's at least as difficult and bug-prone as writing the program in the first place, so I have a hard time seeing the benefit. Theorem primes_below_million_spec: forall l m, (forall p, In p l -> p < 1000000 /\ ~exists n, n <> p /\ n <> 1 /\ Divisible p n) -> length l = m -> primes_below_million = m. Done.
- cousin_it 12y ago
  I think that's missing an implementation of the function that matches the type. Is that also easy?
  - vilhelm_s 12y ago
    That's not so easy. That's the point, right? It's easier to write a specification than an implementation, so it's valuable to check that the implementation satisfies the spec.
  - eli_gottlieb 12y ago
    Well if I wasn't so lazy, it would be easy to implement a Sieve of Eratosthenes algorithm yielding a list of primes up to some number, and then another function feeding 1000000 to that function and returning the length of the resulting list. The hard part would be actually proving the theorem I stated in terms of those two functions.

codemac 12y ago

Um, maybe you missed the point about dependent types? You can express a function, that takes no arguments, that returns primes below 1,000,000 as it's type! That's kind of the point of the talk, and is supposed to be possible in languages like Agda and Idris (I don't know enough about them to give any syntax here). See jules' comment below about how curry-howard does not mean your implementation is a full proof as well. Considering code that flies planes and shoots guns generally is written using proofs on control systems (if not required by law), your examples are a bit weak.

AnimalMuppet 12y ago
But the "proofs" of those control systems isn't anything that looks like a type system, is it? (An argument of the form "due to Curry-Howard, all proofs are type systems" will be regarded as uninteresting at best.)
- codemac 12y ago
  Absolutely not, at least not to me. I'm not a huge type theory guy or anything. But saying that "proofs are a burden especially for things with side effects like shooting a gun" when systems that shoot guns specifically do have proofs in spite of their type systems invalidates the example, if not the argument. The presenters certainly think these languages will help construct those proofs.. that I'm less certain of.
cousin_it 12y ago
It seems to me that using dependent types to express the type "the number of primes below one million" would take at least as much code, and be at least as error-prone, as writing that function in a dynamically typed language directly. In fact I'd be surprised if the dependently typed version were less than 2x the size of the direct version.
- codemac 12y ago
  This is why they brought up the language that uses the same syntax for types as it does for your function definition. It really sounds like you haven't played with Coq or Agda.. because expressing these things are not that much code at all. Also the presentation literally covers that complaint, and how they think more programming languages are needed.
kestert 12y ago
The constructive nature of Idris makes it hard (at least for me) to express a prime under 1,000,000 as a type. For example, it's trivial to express a composite as a GADT: data Composite : Nat -> Type where factors : (x : Nat) -> (y : Nat) -> Composite ((S (S x)) * (S (S y))) but there is no analogous construction of a prime type. Luckily most day to day programming looks more like the composite case than the prime case.
- gergoerdi 12y ago
  As an example, here's how primality is defined in the Agda standard library. It is simply the negation of the property 'has a divisor and is greater than 2'. http://agda.github.io/agda-stdlib/html/Data.Nat.Primality.html http://agda.github.io/agda-stdlib/html/Data.Nat.Primality.ht...

AnimalMuppet 12y ago

Let's go further. If I'm writing, say, numerical calculations, types can save me from getting kilometers when I expect miles (or, worse, kilograms). What it can't do is save me from numerical instability, round off errors, and a whole host of other problems known to the field of numerical analysis. If my code is calculating the angle of a control surface on a plane, the type system is not going to say anything about whether I get 40 results every second. Without those constant, timely updates, the plane is going to crash. A robust type system means that "your code is correct by construction"? That seems incredibly naive. There's more ways for programs to be wrong than are provable via a type system.

Confusion 12y ago
Concerning 'numerical instability': with a sufficiently advanced type system you should be able to save yourself from something like numerical instability. You could e.g. ensure all numbers have an 'order of magnitude type' and define operations between 'order of magnitude' types to raise errors for certain (ranges of) combinations. However, there is (AFAIK) no convenient way to express this in any language, let alone without performance suffering greatly.

eli_gottlieb 12y ago

>You might argue that we should use a richer type system to express the specification. Sure! We just need to express the idea of "primes below one million" in the type system. But that's at least as difficult and bug-prone as writing the program in the first place, so I have a hard time seeing the benefit. Theorem primes_below_million_spec: forall l m, (forall p, In p l -> p < 1000000 /\ ~exists n, n <> p /\ n <> 1 /\ Divisible p n) -> length l = m -> primes_below_million = m. Done.

cousin_it 12y ago
I think that's missing an implementation of the function that matches the type. Is that also easy?
- vilhelm_s 12y ago
  That's not so easy. That's the point, right? It's easier to write a specification than an implementation, so it's valuable to check that the implementation satisfies the spec.
- eli_gottlieb 12y ago
  Well if I wasn't so lazy, it would be easy to implement a Sieve of Eratosthenes algorithm yielding a list of primes up to some number, and then another function feeding 1000000 to that function and returning the length of the resulting list. The hard part would be actually proving the theorem I stated in terms of those two functions.