Hacker News Reader

> Dependent types rely on deductive proofs for verification, and deductive proofs (the "proof theory" part of a logic) are the least scalable verification method as they are least amenable to automation.

What? You can generate proofs for the trivial cases using various algorithms like constraint solving.

Things like sledgehummer tactic, omega tactic, the whole F* language simply prove you wrong (by construction ;)

You need to prove manually only complex cases, where your constrain solver would not manage to generate the proof.

> But now I claim that their composition `foo bar` never crashes (on `head`)

If you proved that foo does not crashes on head for any predicate P and any integer X, and bar terminates, than foo bar terminates. What's the problem?

> The idea that properties compose and that you can cheaply reuse knowledge about components to prove stuff about their composition is just mathematically false. There are a couple of results I mention in my blog posts that show that.

Could you refer to the proof of that, as well as give the definition of ``cheaply'' and especially the evidence that a composition of lemmas and theorems would be more expensive than a constraint solvers-based methods?

I didn't state that proving is easy or cheap, just that manual proving with a usage of constraint solvers for trivial cases is more scalable and makes more sense for sufficiently big programs.

Aside: Sledgehammering doesn't currently work in Curry-Howard-based provers. (This may change in the future, it's an active research topic.)

I was talking about deductive proving, not constructive in particular.

> What? You can generate proofs for the trivial cases using various algorithms like constraint solving. Things like sledgehummer tactic, omega tactic, the whole F* language simply prove you wrong

I don't understand this simple proof. How does allowing some automation prove that it's not the method least amenable to automation?

> If you proved that foo does not crashes on head for any predicate P and any integer X, and bar terminates, than foo bar terminates. What's the problem?

Because that would make the verification problem even harder (possibly to the point of undecidability). And this approach simply doesn't make sense. Clearly, the important correctness properties of your program arise from the composition of all components of your program (or you wouldn't need them). If the same correctness property arises from each component in isolation, then you wouldn't need all others. Most correctness properties are just not compositional (inductive), and the belief that a non-compositional property can be proven by combining results about the components at a cost that scales with their number (polynomially, exponentially -- take your pick) is mathematically false.

> Could you refer to the proof of that, as well as give the definition of ``cheaply'' and especially the evidence that a composition of lemmas and theorems would be more expensive than a constraint solvers-based methods?

I never mentioned "constraint solvers-based methods" (and I'm not even sure what you're referring to [1]). Once you need to prove something, the method is irrelevant, and the theoretical limitations kick in. Showing that one method is easier or harder for instances encountered in practice requires empirical research, so I can't say whether their harder or easier, just that so far deductive proofs are the least scalable in practice. Finally, I can say that we cannot in general decompose correctness to make it easier. Some relevant results are in the papers mentioned in my post in the sections "Correctness does not decompose" and "Language abstractions cannot generally be exploited".

[1]: Perhaps you're referring to SMT solvers and the like, but they are rarely used in isolation. They are used as components in deductive proofs, model checkers and concolic tests. As usual, they are more effective when used in the latter two than in the first.

> Because that would make the verification problem even harder (possibly to the point of undecidability). And this approach simply doesn't make sense.

What? If foo terminates and bar terminates, than foo bar clearly terminates. How does this make no sense?

> Most correctness properties are just not compositional (inductive), and the belief that a non-compositional property can be proven by combining results about the components at a cost that scales with their number (polynomially, exponentially -- take your pick) is mathematically false.

Ok, let's check your blog and what paper you mention

> A Parametric Analysis of the State-Explosion Problem in Model Checking⋆

What? You state that proving doesn't scale referring to constraint based solutions? Sure, they don't scale.

What this foobar example has to do with this tho? Foo does not terminate due to exception, and so does Foo Bar. How doesn't this compose?

> I don't understand this simple proof. How does allowing some automation prove that it's not the method least amenable to automation?

Because you can automate anything you can prove with a SMT or model checker?

> How does this make no sense?

Because most correctness properties aren't compositional.

> What? You state that proving doesn't scale referring to constraint based solutions? Sure, they don't scale.

No, you've misunderstood the paper, and missed the part of the post where I provide necessary context. Like a lot of work in computational complexity theory, they're referring to the model checking problem, i.e. the problem of determining whether a program satisfies some property, not to any particular verification algorithm. Their results apply to all methods (their proofs don't not rely on any particular verification method but show hardness results).

Also, it's funny that you say "they don't scale." You're right, none of the formal methods we have scales nearly as well as we'd like, to the point we can say "they don't scale" [1]. Of them, the one that scales the least is deductive proofs. That's the main reason it's the formal methods that is used the least.

> constraint based solutions

I don't know what you mean by that (SMT?), and I don't recall mentioning those.

> Because you can automate anything you can prove with a SMT or model checker?

Yes, model checkers are completely automatic.

SMT is a class of algorithms and techniques used in various verification methods -- deductive proofs, model checking, static analysis, concolic testing -- not a verification method in itself, so I'm not sure what you mean exactly. Sometimes they're used to prove some logical proposition directly, but they're not used as a complete software verification tool, because they're rather limited on their own.

[1]: When applied to the code directly. We have ways of scaling formal methods by verifying high level specifications.

People are missing the point of your post, which is a bit of a shame. The point is that `foo p n` returns an integer when `n` is the sum of two positive integers that both satisfy `p`. `bar n` holds when `n` is prime. Thus `foo bar` always returns an integer iff Goldbach's conjecture is true. You point is that no one knows how to prove Goldbach's conjecture therefore no formal methods can prove that `foo bar` never crashes.

If the dependent typing proponents in this thread responded to your point rather than picking holes in your usage of the words "composition" and "terminate" then they might make some interesting counterpoints. For example, they might say

1. "We don't expect dependent types to be able to prove everything (of course), we only expect them to be approximately as good as any other proof method for almost any property of interest", or

2. "What do you mean "you can easily prove almost any property of interest about each of them in isolation"? Does "property of interest" have a specific definition? How about `bar (factorial (10101010))`? Is that `True`? Is it not a "property of interest"? Is it not "in isolation"? How about "there exists n such that `bar m == False` for all m > n"? How would you "easily" prove that?

Personally I'm not a dependent typing proponent so 1 is just my wild speculation. I am interested in your response to 2 though.

1. I mentioned why dependent types are not as good, in my opinion, as other verification methods. They are not flexible in the choice of verification method, and the method they're tied to is the worst default a programmer could want.

2. It's not a very precise statement, I mean that you can fully describe and understand what it is they do. After all, when you verify a program, you want to check certain properties that are of interest to you (because they're requirements). So you can ask and answer questions like what it is that they do, are there values of p for which foo always returns false? Values for which it always returns true? Values for which it sometimes returns true and sometimes false? And yes, your question, too, "there exists n such that `bar m == False` for all m > n?" The answer is no, and it was proven by Euclid: https://en.wikipedia.org/wiki/Euclid%27s_theorem

In other words, if two different programmers were writing foo and bar (as is often the case in software), each would have thought -- without knowing of the other component -- that pretty much any property they want to state about their component could be rather easily proven.

Regarding 2 I think you're missing my point. Firstly, the first "property of interest" was rendered incorrectly (and also stated incorrectly). It was supposed to be

> How about `bar (factorial (10^10^10^10 + 1))`? Is that `True`?

Can we easily prove or disprove that property of interest?

Secondly, I know the second result is true. I'm asking how you would easily prove it. How do you easily show that "forall m. bar m == True" is equivalent to Euclid's theorem?

> Can we easily prove or disprove that property of interest?

Maybe we could answer that affordably, albeit with some probability, using fast probabilistic primality tests (I don't know how high they can practically go). But can we easily prove what the result of sorting a particular list with a 10^10^10 elements is? Maybe not, but I don't think it's as much a property of interest as "does this program ever crash." In other words, for every algorithm with some non-trivial complexity, the question of what the result would be for some very large input is hard to answer, but I don't think that is a common property of interest.

But if I get your meaning, you are correct that sometimes, if our focus is on an algorithm rather than on a working system, we forget that all systems can, at best, be shown correct only with some probability (because the hardware only does what it's told with probability), and at some point, there are algorithmic bugs that can occur in practice with a probability that's lower than that of a hardware glitch.

> How do you easily show that "forall m. bar m == True" is equivalent to Euclid's theorem?

By proving that bar is, indeed, a primality test, which is not hard. I.e. you prove that bar n = TRUE iff ∀ m ∈ ℕ . 1 < m < n ⇒ n % m ≠ 0. This is usually proven by induction.

This is a very confusing thread for me.

I think Idris -- while not exactly mainstream -- has shown that it's fine to treat type checking and types as a continuum. There's nothing about dependent types that forces anybody to prove Goldbach's conjecture or anything of the sort.

You, the programmer, get to choose just how rigorously you want your values to be specified, and if you really want you can ask for proof of the Riemann hypothesis, or you can ask for a... String.

For me, that's the great thing about dependent types -- you, the programmer, get to choose how rigorous you want to be.

> has shown that it's fine to treat type checking and types as a continuum

It has not shown that at all. That you can encode arbitrary propositions with dependent types has been known for many decades. That doing so is a feasible, affordable way to verify software correctness has yet to be shown by anyone, despite decades of attempts.

> You, the programmer, get to choose just how rigorously you want your values to be specified

But that's the problem. Specifying your software and verifying it are two different things. The last thing you want is to limit the rigor of your specification to the rigor of your verfication, especially if your verification is done with deductive proofs, as that's the most costly, least effective verification method. You want developers to choose the rigor of their specification and separately choose the rigor of verification. The main problem with dependent types is that they don't let you do that, and so force you to specify only stuff you can affordably prove, which is usually the simple stuff.

> It has not shown that at all. That you can encode arbitrary propositions with dependent types has been known for many decades. That doing so is a feasible, affordable way to verify software correctness has yet to be shown by anyone, despite decades of attempts.

Well feasible is definitely a way I would characterize dependently typed deductive proofs. Compcert was a large achievement and produced a formally verified compiler back-end. Therefore it is definitely feasible to design software that is correct by construction using these methods.

I think it's pretty reasonable to say that it's not yet affordable to verify all compiler back-ends this way. However I don't think the future where it is affordable is far off. Folks in the Lean community are making head way and learning from Compcert about how to model the semantics of C-like programs using new advances in type theory that will make it easier to verify such systems.

Therefore I wouldn't discount Dependently Typed Haskell so completely. Verification methods work in a continuum and I use a few depending on the needs of the project. I often use TLA+ and sometimes I use Lean. One day I'd like to see synthesis get better for large-scale projects. That would be super cool.

> Compcert was a large achievement and produced a formally verified compiler back-end. Therefore it is definitely feasible to design software that is correct by construction using these methods.

CompCert is a very small program (1/5 of jQuery) and it's taken world-experts years of work. Its verification also wasn't really done using dependent types, but in Coq, a traditional proof assistant whose theory happens to be based on dependent types, but is much more similar in practice to, say, Isabelle/HOL than to Idris/dependent Haskell.

> However I don't think the future where it is affordable is far off. Folks in the Lean community are making head way and learning from Compcert about how to model the semantics of C-like programs using new advances in type theory that will make it easier to verify such systems.

It's been said to not be far off for 40 years now. Yet what can be verified with deductive proofs has remained, for decades, 2-3 order of magnitudes behind "ordinary" software, and the gap isn't closing.

> Therefore I wouldn't discount Dependently Typed Haskell so completely.

I'm not. I'm just saying that it's currently less promising than the main thrust of formal methods research (which focuses on automated methods much more than on deductive proofs) and that it is certainly nowhere near a point where it can be said to be "the future." I'm also pointing out that there are currently approaches that subsume dependent types -- have nearly all of their advantages and virtually none of their disadvantages (contract systems).

How is `foo` "clearly terminating"? With `p = const False`' it's undefined for any even x >= 3.

It would terminate with an exception.

Hence diverge, aka not terminates.

You've even stated this yourself:

> But now I claim that their composition `foo bar` never crashes (on `head`)

It does, because foo does.

> Hence diverge, aka not terminates.

By focusing on FP nomenclature (whether an exception is regarded as "divergence" or not depends on your language -- note that I said "terminates"; the point is that the trace for each execution is finite) you're missing the issue, that exists regardless of language.

> It does, because foo does.

`foo bar` never crashes (unless I made some silly bug).

Now I'm genuinely confused: do you consider a program that diverge (as in reaches some exceptional state) not as a "crash" but as a form of termination? If so then I don't understand what your original point was; if you could prove that both functions always return some value then you can also say that composing them will always return some value.

> diverge (as in reaches some exceptional state)

The term "diverge," when applied to an exception, is not a computational term but a term from a specific formalism (e.g.: Haskell). A computation is a sequence of states; if it ever reaches a terminal state (i.e., a state from which it cannot exit), it is said to terminate. You can apply the terms converge/diverge to termination/non-termination, but once you speak of exceptions, you're using a language-specific terminology.

> if you could prove that both functions always return some value then you can also say that composing them will always return some value

Yes, but that would be too hard. `foo` doesn't always return a value, but `foo bar` does. What can you prove about `foo` and `bar` separately that would make proving that easier, not harder?

@pron: I'm not an expert in rewriting systems and type theory, but in the literature I have studied a partial function is said to diverge when it's applied to some particular value that won't return / produce a normal form (i.e. non-terminating), either because it will recur ad infinitum or because the applied value doesn't map to the function's codomain. One could argue that in a well typed program the latter shouldn't happen, but then one would require a type system with dependent types to type-check programs with functions like head : [a] -> a :) An exception is just a mechanism that some PLs provide to indicate that the program reached such exceptional state where, for whatever reason, some assumption failed and there is no meaningful reduction to compute.

The very notions of a "partial function" and a "normal form" are language-dependent. And yes, certainly in those languages, throwing an exception is called divergence. But partial functions are not an essential concept of computation. A computation can terminate or not, and the name divergence in that context applies to that. In any event, I was careful to speak of termination, the computational concept, rather than divergence, which can have a formalism-specific meaning.

Partial function is a standard mathematical term, not a programming language (PL) one: https://en.wikipedia.org/wiki/Partial_function so what you say seems wrong

A function that is non-partial is, in standard maths parlance, a total function https://en.wikipedia.org/wiki/Partial_function#Total_functio...

Such terms are certainly used in that sense by PLs eg in scala Function and PartialFunction types exist with those intended semantics, and it seems haskell recognises the terminology https://wiki.haskell.org/Partial_functions (though whether it supports them in the language definition or libraries I don't know).

Could people please respond to pron's actual point rather than nitpicking terminology? If it helps I've tried to elucidate here: https://news.ycombinator.com/item?id=20722887

The point is @pera said in https://news.ycombinator.com/item?id=20717160 "Now I'm genuinely confused". That seems to be down to confusion in terminology.

@pron then makes an apparently incorrect claim which I dispute to try to help clarify. That's clarification not nitpicking (I intended that way anyway). @pron's point may be valid but if we don't have common meanings to words, this will go nowhere.

The confusion is about a word that I didn't use. I said that both subroutines "terminate". That is a word with a precise meaning in computation -- every possible trace is finite. Someone started arguing about whether or not they "diverge", and I said that that's language-dependent (https://news.ycombinator.com/item?id=20723623). Both foo and bar always terminate, and that is both precise and a common meaning.

> The confusion is about a word that I didn't use.

which word?

> I said that both subroutines "terminate". That is a word with a precise meaning in computation

I'd say so. But here's a clip from previous:

> zopa 23 hours ago :- How is `foo` "clearly terminating"? With `p = const False`' it's undefined for any even x >= 3.

-and you say-

> pron 23 hours ago :- It would terminate with an exception.

So you're claiming that 'terminating with an exception' is termination "with a precise meaning in computation". But that's a bloody strange definition I have never come across.

In fact it's so weird I had trouble finding a definition because it seems so fundamentally bizarre that nobody I've ever met has ever considered throwing an exception (or similar) due to precondition violation to be termination. But here goes:

1943: In a paper, Stephen Kleene states that "In setting up a complete algorithmic theory, what we do is describe a procedure ... which procedure necessarily terminates and in such manner that from the outcome we can read a definite answer, 'Yes' or 'No,' to the question, 'Is the predicate value true?'."

That from https://en.wikipedia.org/wiki/Halting_problem

So yes termination is defined and no it's not what you claim it is. No wonder people are getting confused.

as for... (edit: deleted this as poster accidentally linked to wrong comment)

> But that's a bloody strange definition I have never come across.

I don't know what else I can say. Exceptions are not a computational concept, they're a language concept. The computation terminates in some well-defined state. That the language declares that that well-defined state is not considered a value is a language-specific thing.

> So yes termination is defined and no it's not what you claim it is.

It is exactly what I defined, as your quote shows. Termination and decision are not the same thing. Imagine that the decider could terminate with, Yes, No, or Error. It would still not be a decision procedure, but it is very much termination. And your very quote says exactly that when it says "terminates and in such manner that..."? If termination already means that it is in such manner, why is the qualification necessary?

Your definition of termination (to mean anything other than reaching a terminal state after a finite number of steps) is based on the fact that in a particular formalism, the lambda calculus, termination yields a normal form. Now, the lambda calculus doesn't have exceptions, and so every lambda term either reduces to a normal form or the reduction never terminates, but a language like Haskell adds a third possibility. Because Haskell draws inspiration from the lambda calculus, it's easier, in the discussion of Haskell, to map exceptions -- which don't yield a normal form but do terminate at a definite computational state -- to the same notion of divergence, that, in the lambda calculus, is synonymous with termination, but in Haskell it isn't. So I wouldn't be surprised if some people took it further, and used termination to be synonymous with "produces a normal form" in Haskell. But, again, this is not how the notion of termination is commonly defined in computation (many notions of computations don't even have the concept of a normal form or of a value). In Java, for example, where the denotation of a subroutine isn't similar to a partial function but is, rather, a predicate transformer, an exception and a return value are equally valid results.

But yeah, I agree that selling Haskell as maths, does tend to confuse, and so people can mistakenly think that Haskell terminology is canonical mathematical or computer-science terminology. And yeah, it is sometimes frustrating to speak with those who are only familiar with the mathematics of functional programming and not with the mathematics of imperative programming, or with the theory of computation in general, and so don't even know which terms are overloaded and which are canonical.

All of this, however, is so irrelevant to the point of my `foo bar` example (namely, that knowing things about components does not mean you can feasibly know things about their composition) that it's ridiculous.

> Yep, and that reply was posted 10 minutes before you referred to it.

OMG, I linked to that one because I had just written it and it was right in front of me. Here is the same answer in an older comment: https://news.ycombinator.com/item?id=20715970

So not only are you determined to focus on something that is entirely beside the point because you've completely missed the point, you are also wrong in the side-track you've chosen.

AFAICS you are fundamentally confused which is causing this mess. This is a good example:

> Imagine that the decider could terminate with, Yes, No, or Error.

That's just not how it works. Mathematically a function, if it terminated, terminates with an answer. There is no error - the precondition of the function states what is acceptable and the function must come back with an answer (or possibly not terminate, but that's another thing). That's why the quote from Stephen Kleene[0] didn't mention errors.

If I want to define a function computing real-number square root, I set as a precondition that negative numbers must never be passed to it. That's it. That's the precondition - "this and only this is acceptable to this bit of code" is what it means.

In any language an exception should happen if you violate that ie. pass in a negative number. That may show up as an exception. But you don't want exceptions! Which is why you try to formally guarantee the precondition is met! So You are guaranteed of an answer (leaving aside non-termination).

All this formal stuff (at least in my world) is about verifying the code conforms to the precondition such that an error will never occur (edit: wrong, it's more than verifying to the precondition but go with it for now) . Also verifying that if the precondition is verified that termination will happen.

Put another way, taking the head of an empty list is meaningless, so you set the precondition (edit: of the function hd())to be that always

  is_not_empty(lst)

yes, you may get an exception unless verified. But if you can prove that at the point of call lst is never empty then hd() will guarantee never to except.

If any program was entirely verified thus then no exceptions would be needed because the program would be correct (excluding resource exhaustion on our regrettably finite computers).

> Termination and decision are not the same thing.

Mathematically if it terminates, it decides. If it decided then it has terminated. Yes they are the same thing. That's what the quote says. Termination via exception is not in that world: "in such manner that from the outcome we can read a definite answer". Blowing up without deciding would mean termination (an exception in your terms) without providing yes/no. Useless.

I'm pretty weak in this area but I do know the basics, and it does not come across that you do.

> OMG, I linked to that one...

No probs, I edited out that.

[0] Heh, same kleene after whom was named the kleene star in regexes. Who know.

> Mathematically a function, if it terminated, terminates with an answer.

There is no such thing for a mathematical function to "terminate." In classical mathematics, a function is a one-valued relation, a set of pairs, if you like. There is no algorithm and no computation involved. Termination is a computation term. Divergence is a formalism-specific.

I believe these terms (including "exceptional state", but no "exception") are commonly used in formal languages, combinatorics, rewriting systems, mathematical logic and so. They are also used in Haskell because this was partially based on System F, which comes from the simply typed lambda calculus. I understand your frustration and please believe me that it was not my intention to turn this thread into a pedantic show.

But now coming back to your original point and example: I don't think anyone from the Haskell and ML-family languages camp is claiming one can automatically deduce every possible decidable property from any function with their type system, or at least not yet :)

Yes, they are commonly used in formal languages, and their precise meaning is language dependent, which is why I didn't use partial or divergence but termination, which has a unique computational meaning.

I don't think anyone claims that any property can be proven. I do think that some think that if a program can be decomposed into simple parts, whose "interesting" properties are provable in isolation, then you can feasibly prove interesting properties of their composition, which is not true. A proof of that was only given in the past 10-15 years, and is referenced in my post.

> Partial function is a standard mathematical term, not a programming language (PL) one

Like many things in mathematics, the term has been borrowed and changed. Look, for example at "function". Do you think "function" in programming (even in Haskell) means the exact same thing as in mathematics?

In general, partial functions mean that for some values, a function is undefined. But in a PL nothing is undefined. In some cases there would be an exception; in others the subroutine would loop forever. But a language like Haskell, because it wants its "functions" to resemble mathematical functions, declares that those perfectly normal computational behaviors correspond to "undefined". In imperative languages, where subroutines don't try to correspond to (partial) functions, throwing an exception does not correspond to undefined.

>But now I claim that their composition `foo bar` never crashes (on `head`); can you prove me right or wrong?

Mu. But I can prove that your argument is not well-formed.

1. That is not composition it is application. (This is not simply terminology, you using application is what allows you to reference bar inside foo)

2. The actual composition of those functions (foo . bar) is not valid Haskell and would not typecheck.

That seems a little uncharitable!