[wyager]

>but you have to realize that this kind of perfection in software costs huge amounts of money

Maybe not as much as people think. There are machine-assisted mechanisms for building mathematically perfect software. See Curry-Howard oriented languages like Coq and Agda. It's certainly harder to write perfectly, provably correct programs, but maybe not as hard as most people think.

There is also a lot of middle ground in the form of relatively powerful (but not quite Agda-powerful) type systems.

[vezzy-fnord]

Mathematically perfect provided the proposition you're verifying is actually relevant and consistent with the one you're applying in the real world. Given the finicky nature and constraints of the environments that most software runs on, this could prove difficult. Moreover, the proofs must be maintained along with the software.

As for type systems, mission-critical software has generally made good practice with them (Ada, proof checkers, etc.) More so than consumer and enterprise circles. Yet a ton of catastrophic bugs have been the result of errors outside the scope of type checking, and as a counterpoint, our telephony is pretty robust with dynamically typed Erlang switches. It seems that mechanisms for building self-healing and concurrent systems are often put aside and equivocated solely with strong type systems. From what I recall, Erlang's signature feature of hot code loading actually conflicts with static typing.

[Kenji]

I am familiar with some code-proving tools and functional programming. Verifying such code is tedious and will increase time, cost and skill required for the project substantially. People just aren't ready to pay the price for that. Yet.

[tormeh]

The thing about typechecking, though, is that you're essentially specifying your program's behavior twice: Once very detailed in the actual code and once at usually some lesser detail in the types. All the compiler does is checking that these two specifications are consistent with each other. Your types can have bugs too, in which case nothing will help you. What frustrates me about detailed type systems is that as detail increases, difficulty of writing the types will increase and type bugs will become more common. Now, assuming the bugs in your code and types are statistically independent that would still save you a lot of bugs, but I suspect they are not.

[Dewie]

> The thing about typechecking, though, is that you're essentially specifying your program's behavior twice: Once very detailed in the actual code and once at usually some lesser detail in the types.

How so? The implementation is not the specification; but the type is the specification. Like people like to say, the type is a Theorem, and the implementation is is the Proof of the Theorem. (In a very real sense.) And don't you need both?

Hopefully there can be some type inference at a certain scope, to avoid cluttering the code with a lot of 'obvious' type declarations. I forget exactly how dependently typed languages work in that regard right now (there certainly can't be full type inference).

> All the compiler does is checking that these two specifications are consistent with each other.

"All". That's already better than informal mathematical proofs.

> Your types can have bugs too, in which case nothing will help you.

Yes, just like any other kind of alternative specification there is. Short of mind reading, there is no getting around actually describing what we want. But where there is a distinction to be made is in what kind of specification is easy and declarative enough to use as to give the least likelihood of introducing bugs in the spec itself.

> What frustrates me about detailed type systems is that as detail increases, difficulty of writing the types will increase and type bugs will become more common.

I guess if we assume that we have collapsed/unified the type and term(/value) level, we can use any old Good Software Engineering Practice when it comes to keeping the types tidy. Like using type functions to encapsulate some of the detail: maybe have a `sorted(list)` function instead of having to write it out each time we need it.

This is just a guess though; I don't know how the dependent programmers do it. Well most of what I'm writing here is guessing, on some level.

(And judging by the pride that some people show when they proclaim that "half of our code base consists of just tests", well... I certainly think that types can be more succinct than that!)

> Now, assuming the bugs in your code and types are statistically independent that would still save you a lot of bugs, but I suspect they are not.

I guess if we go with the previous assumptions of a unified value/term level, then the statistical chances are the same in that types are just ordinary values, instead of the types belonging to its own language. ;) Then we just have to make sure that the amount of types is substantially smaller than the amount of "regular ol' code".

Typer er fremtiden. Håper jeg (kanskje).

[Dewie]

The problem with advanced type systems is that, while the theory and implementations and the research might be mature, it will take god-knows how many years of research oriented on usability in order to get something approachable and understandable. If people are even researching usability like that in a systematic manner (I have my doubts whether there are PL researchers that are working on that kind of thing, or if the community has just thrown their hands up and said that it isn't doable).