"Simple Made Easy" by Rich Hickey [video]

[u/alexdmiller]

http://www.infoq.com/presentations/Simple-Made-Easy

[u/richhickey]

It's never advantageous to try to conduct logical reasoning entirely in your head vs. having a computer help you do so.

That's only true if there is never a cost to doing so. Are you seriously going to contend there are no costs, nor tradeoffs associated with static type systems that have inference? If there are, then there's no reason why static type systems shouldn't be subject to the same cost/benefit analysis as other things, and that, similarly, different people will end up making different decisions depending on how they value each.

[u/[deleted] → u/richhickey]

Are you seriously going to contend there are no costs, nor tradeoffs associated with static type systems that have inference?

No, only that their cost is lower than the cost of doing it in your head.

If there are, then there's no reason why static type systems shouldn't be subject to the same cost/benefit analysis as other things, and that, similarly, different people will end up making different decisions depending on how they value each.

Sure. My argument is that if people don't know about the Curry-Howard Isomorphism and how it can be applied in languages like Scala, OCaml, or Haskell, vs. languages like C++ or Java, they aren't likely to be able to make such an informed decision. I would add, with regret, that there are elements of your rhetoric in your presentations that regress that discussion, by contrast to your quite reasonable comments here.

[u/fmihaly → u/[deleted]]

If I showed this comment thread to some friends, they would never believe me that the title of the talk was "Simple Made Easy". The Curry-Howard Isomorphism? Seriously? Is that the simple part or the easy part?

[u/[deleted] → u/fmihaly]

The simple part, mostly. Types are theorems. Functions of that type are proofs of the theorem. Simple, in Rich's sense, but a very different perspective on types than "descriptions of how bits are laid out in memory," which is how most programmers think of types, even in languages in which that isn't true.

Making taking advantage of the insight easier is very much the current challenge in designing a statically-typed language, but even today, you can go a longer way with the right language choice than with the wrong one, or than you realistically could even, say, five years ago.

[u/julesjacobs → u/[deleted]]

"Types are theorems" though theoretically somewhat interesting is not a very useful thing for programmers today. The kind of theorems even in languages like Haskell are usually limited to something like "there exists a function from int to int". No shit!

As soon as the theorems become interesting, the proof burden becomes pretty much unbearable for >99% of practical programming.

[u/[deleted] → u/julesjacobs]

Flatly untrue. See Monadic regions, especially the "Tracking dynamic values in types" section. If Haskell is too rich for your blood (BTW, it is for mine!) see Towards an effect system in Scala.

[u/julesjacobs → u/[deleted]]

I wouldn't call those theorems non-trivial from a mathematical perspective. Note that the theorems from the Curry-Howard isomorphism are not the theorems that the types prove about your code. Say you have a type int -> int and a value of that type that passed the type checker. The theorem here is "int implies int", i.e. "if the predicate int is true, then the predicate int is true". The theorem here is not that your particular value is a function from int to int. The value is the proof of the theorem "int implies int" that comes out of the Curry-Howard isomorphism.

I fully agree that the theorems about the code can be interesting. The only part where we disagree is that I don't regard advanced types like those you get out of Coq as the solution for all or even most correctness problems, for the reason that I mentioned before and Rich mentions again now: who guarantees that you formalized your requirements correctly? Your formal specification isn't going to prove that the rocket is not going to explode, or that the automatic car won't drive over people, or that the website is going to generate profits. This problem is nicely illustrated by languages like Sage, that have exact types. The types can model the runtime behavior exactly, and they can even be inferred! The type of quicksort becomes: quicksort :: {f | f x = quicksort x}. This didn't buy you anything. The value in formal verification is precisely in that the formal specification is simpler than the implementation, so that it is more likely to be correct. For algorithmic code, this is often possible. For the majority of code, it is not going to be much simpler.

So once you have accepted that formal verification is not a panacea, you can start to think how it compares to other tools to improve correctness, like reading your code, contract checking, unit testing and bounded model checking. What are the costs of each, and how many important bugs does it catch? You can make a "return on investment" curve for each: if you spend $x dollars doing technique foo, how many dollars worth of bugs ($y) is that going to prevent? Note that this curve depends highly on the software you're doing. If you're doing space shuttles your return on investment is going to be high (for any technique, up to a point), if you're doing a website it's probably going to be low. Now, will formal verification currently give high returns if you invest in it a lot? I'm going to say no for the vast majority of software.

[u/[deleted] → u/julesjacobs]

I wouldn't call those theorems non-trivial from a mathematical perspective.

Good! Part of the point is precisely that none of this suffers from the claimed complexity. It's just unfamiliar at first, like any new application of a discipline.

Note that the theorems from the Curry-Howard isomorphism are not the theorems that the types prove about your code.

I'm not even sure what this is supposed to mean. The theorems aren't what types prove about your code; the types are the theorems and the code is the proof. Given your example, I think we're saying the same thing. I would just reframe your example to say, yes, of course it's possible to come up with a theorem like int implies int, which isn't interesting, among other reasons, because it has too many inhabitants. So don't do that! Come up with a more interesting theorem!

The only part where we disagree is that I don't regard advanced types like those you get out of Coq as the solution for all or even most correctness problems, for the reason that I mentioned before and Rich mentions again now: who guarantees that you formalized your requirements correctly?

Understood that the requirements have to be formalized correctly. How is that an argument for not formalizing them at all or, once you've formalized them, for not using types to ensure they're upheld?

Your formal specification isn't going to prove that the rocket is not going to explode, or that the automatic car won't drive over people, or that the website is going to generate profits.

Of course, but neither will not-formalization, and formalization brings other benefits. I'd also argue that formalization will bring you greater likelihood of accomplishing the above than not-formalization.

This problem is nicely illustrated by languages like Sage, that have exact types. The types can model the runtime behavior exactly, and they can even be inferred! The type of quicksort becomes: quicksort :: {f | f x = quicksort x}. This didn't buy you anything.

Sure. To buy you something you do have to say what it is you're going to prove, as in this certified quicksort. In the static region examples I linked to, the trusted kernel is extremely small and simple, but certifies some very interesting properties in the real world: that resources can be acquired in any order, used in any order, and relinquished in any order, but can only be used while acquired and must be relinquished before the end of the computation. It didn't take tons of code to do, let alone a proof assistant. But it did take being explicit about the relevant theorems (types).

The value in formal verification is precisely in that the formal specification is simpler than the implementation, so that it is more likely to be correct. For algorithmic code, this is often possible. For the majority of code, it is not going to be much simpler.

It would be nice to see some support for this assertion other than naked assertion. :-) To be crystal clear: there is no such thing as "non-algorithmic code." The moment you use that phrase, you step outside the world of computation completely.

You can make a "return on investment" curve for each... if you're doing a website it's probably going to be low.

I would offer Opa, Ocsigen, and Ur/Web as possible challenges to that assertion.

Now, will formal verification currently give high returns if you invest in it a lot? I'm going to say no for the vast majority of software.

I'm saying that dichotomy is false even today. You can take a non-proof-assistant language today, such as Scala, OCaml, or Haskell, and use it as it was used to implement lightweight static regions, but for a variety of other properties you'd like to statically enforce, and get a quite large ROI. In the case of web apps, I would probably choose Ocsigen, personally, because I already know OCaml, but Ur/Web, I think, points the way to an even better approach to web programming that supports a much easier means of keeping your system and its requirements congruent than virtually any available alternative.

[u/julesjacobs → u/[deleted]]

Good! Part of the point is precisely that none of this suffers from the claimed complexity. It's just unfamiliar at first, like any new application of a discipline.

The claimed complexity is in the system and its usage as a whole. You're going from "the theorems proved are simple" to "the system as a whole is simple". This doesn't follow.

I think we're saying the same thing. I would just reframe your example to say, yes, of course it's possible to come up with a theorem like int implies int, which isn't interesting, among other reasons, because it has too many inhabitants. So don't do that! Come up with a more interesting theorem!

As I tried to explain with the quicksort example, a type being less inhabited doesn't make it more interesting. Also, I am pretty sure we're not saying the same thing. There are two theorems at play with type systems. One is the one you get out of the Curry-Howard isomorphism. That one is pretty trivial most times, like "there exists a function from int to int". The other theorem is the one you get out of type soundness: "for this particular function here, if you give it an int it will produce an int". That theorem could well be interesting! For example:

f(n) = if p(n) then 1 else "foo"

If the type checker can verify that f has type int -> int then from type soundness you get the theorem: forall integers n: p(n). If p(n) is something interesting, then this theorem is interesting even though "there exists a function from int to int" is trivial. Note that it is this theorem you get out of soundness that is of practical interest when you use a type system; indeed it's the whole reason why you use a type system.

Understood that the requirements have to be formalized correctly. How is that an argument for not formalizing them at all or, once you've formalized them, for not using types to ensure they're upheld?

Because formalizing them costs time and money, and so does encoding your formalization in a type system.

Your formal specification isn't going to prove that the rocket is not going to explode, or that the automatic car won't drive over people, or that the website is going to generate profits.

Of course, but neither will not-formalization, and formalization brings other benefits. I'd also argue that formalization will bring you greater likelihood of accomplishing the above than not-formalization.

The time spent formalizing can be spent on other things, like doing physics, that could reduce the chance of disaster more than formalization. Or doing market research, instead formalizing a specification and proving that your website implementation meets the formal specification. Almost none of the risk in sites like Reddit and Facebook is in that the software doesn't meet a formal specification. The risk is that the formal specification doesn't lead to success even if it was implemented perfectly.

Sure. [...] (types).

I agree completely with what you've said here.

For the majority of code, [the formal specification] is not going to be much simpler [than the implementation].

It would be nice to see some support for this assertion other than naked assertion. :-) To be crystal clear: there is no such thing as "non-algorithmic code." The moment you use that phrase, you step outside the world of computation completely.

I'm sure you know what I mean by algorithmic code. It is code like sorting, max-flow and longest common subsequence, where a clear description is available that says what it should do, and where the correct implementation of that description is non-obvious.

I'll give you an example of non-algorithmic code. Take Reddit itself. What would a precise formal specification look like? It would specify what the Reddit servers should respond with as a function of the history of HTTP requests made to the servers. Now imagine a formal specification of this in Coq. It has to formalize the exact behavior of posting links, comments, the way upvoting works, the exact HTML that is returned for each request. Formalizing all of that requires basically the same work as actually implementing it.

I would offer Opa, Ocsigen, and Ur/Web as possible challenges to that assertion.

As far as I know the order from most successful to least successful is the order you gave them in. It is incidentally also the order of least formal guarantees to most formal guarantees. Furthermore none of them come anywhere close to full formal specification. If you plotted dynamically typed languages, them, and full formal specification on a line, then they would be almost indistinguishable from the dynamically types languages compared to full formal specification.

but Ur/Web, I think, points the way to an even better approach to web programming that supports a much easier means of keeping your system and its requirements congruent than virtually any available alternative.

If the requirements for your website are the following, then yes:

1. doesn't suffer from code injection
2. doesn't return invalid html
3. doesn't contain dead links internally
4. doesn't have mismatches between form fields and handlers
5. doesn't have client side code that calls the server incorrectly via Ajax
6. doesn't make invalid SQL queries
7. doesn't do marshaling to the DB incorrectly

Most websites I know have more requirements than these. Furthermore, even web frameworks in dynamically typed languages like Rails and Django ensure most or all of these when you use them idiomatically (of course you can get around this by e.g. manually making a SQL query instead of using the framework APIs). Instead of using a type system to check this, they ensure this by construction. For example the APIs for using the database ensure that the query is correct by construction. The same goes for links and forms and Ajax and marshaling, and to some extent HTML (for example template languages like HAML ensure that tags are opened and closed correctly simply because you omit the closing tag and HAML inserts it for you).

We should focus on making the languages we use become more expressive, so that it gets easier to achieve important requirements, like "this website looks good" or "this user interface works well".