4 ms·

Thanks for this! Hoare (partially) answers a question I asked in the comments on "The Little Typer" (a good treatment of programming with dependent types). Th

Thanks for this! Hoare (partially) answers a question I asked in the comments on "The Little Typer" (a good treatment of programming with dependent types). That approach to dependent types brings our code closer to being verifiable. Unfortunately as a number of commenters testified it also makes software (currently) impossible to scale to complex algorithms, dependence on loosely coupled libraries, and so forth. Since Hoare wrote 22 years ago, I'm now wondering if there's a fundamentally intractable problem with improving formal validation of complex software. Dependent types seem like a natural way of embedding the programmer's assumptions and reasoning into software, but clearly current technology in that area is still very very far short of helping with software at current scale. Meanwhile our practical means of building complex software have improved considerably and we can develop systems that are reliable "enough", even at enormously greater scale than Hoare anticipated. The gap between viable software complexity and formal methods of describing software semantics has grown much wider since Hoare, rather than shrinking. I wonder if we could step back from this style of formal methods, and look for an alternative approach. We need ways to capture the actual reasoning and methods that work for programmers building complex systems -- rather than trying to pretend they are mathematical objects.

mikekchar 8y ago
For me, notation is everything. A computer program is a model of a problem. There is more than one representation of that problem: in the static code and in the running code. If you go to a kind of naive way of writing programs (that we all went through when we were first starting out), you write the code and then you step through it (either on paper, or with a debugger), viewing how the code is running. There are many techniques available for helping you reason about your code. However, it's important to understand that software code is a notation for modelling the problem. Often formal methods introduce another notation that proves that the encoding of the problem in the first notation is "correct" according to some definition of "correct". The more we move into modelling the correctness in the second notation, the more we move the burden of reasoning about the issue to the "code" in the second notation. It's often very useful to model the problem more than once. For example, I'm quite a big fan of unit tests. "Give the code in the system, I expect X to be true/false in this situation". I'm just as likely to make mistakes in my unit tests as I am with the production code. However, it's the comparison of the two that allows you to reason effectively about the code. They are two sides of the same coin (intentionally coupled -- which, as an aside, is why you should avoid trying to decouple your tests from your production code!!!). Even though it is useful to model twice, I'm not really sold on the idea of doing it in general (and I have a very specific idea of how to write unit tests that's heavily coloured by this point of view). Everything that you add to the code should make reasoning about something easier and more convenient than not doing it. Otherwise you are better off with just writing the production code. You will have less complexity to deal with overall. In my opinion, a good example of a tool that helps incredibly well are strongly typed languages with type inference systems. For a small penalty of type notation, the system can tell me, without a doubt, when I've made a mistake with the types of my variables. Not only that, but the notation itself allows me to reason about why I've gotten myself into a problem. It can even help me reason about what the function does, without having to even look at the implementation. This is incredibly helpful. I think as we go forward, we need to be looking for this kind of tool. Dependent types seem like a perfect example of this. However, there is always going to be a small price to pay. Writing code in a statically typed language is harder than writing code in a dynamically typed language -- precisely because the dynamically typed language allows you to write code without having to think up front about the consequences. Of course, you may leave bugs in your code because of it, but the initial cognitive load is smaller. Similarly, it's much better to write code where you can reason about the run time behaviour without it running, but that is much harder than writing some code and walking through it, playing "computer". We need to balance these kinds of factors because a tool that is not used is a useless tool. I'd be perfectly happy to work in a pure functional, statically typed language because it is much easier to reason about my code. Many of my colleagues simply are not willing (or possibly even able) to pay the upfront cost of working in that kind of ecosystem. Hence, I'm not able to work in it either.
- thrmsforbfast 8y ago
  This was a great comment. The fact that new notations/representations (be that tests, simulations, formal methods, etc.) must justify their additional cognitive overhead is a great point. Aside from unit and integration tests, I think that substantial new notation/infrastructure is most justifiable when the second notation/setting allows you to model parts of the problem that can't be modeled in the original notation. Embedded software is a good example. Although there are some tools that allow you to model the physical system alongside the control software, typically the code is written in C and so there's no way of expressing very important aspects of the problem in the implementation language. So a second notation can help. For example, simulators and HiL setups for testing or things like https://github.com/LS-Lab/KeYmaeraX-release https://github.com/LS-Lab/KeYmaeraX-release for formal methods. Security is another good example. Typically code does not include an explicit threat model or explicit security properties, and these aspects of the problem are often scattered across the code and difficult to reason about. So being able to capture those things directly in a second notation can add a lot. For example, automatic vulnerbaility scaners for testing or https://tamarin-prover.github.io/ https://tamarin-prover.github.io/ for formal methods. Distributed/fault-tolerant systems are yet another example where it's very hard to state the thing you want to state in the implementation language. Netflix's chaos monkey comes to mind.
- jedharris 8y ago
  Agree about type inference being a great tool along the lines we need. Notably it extracts information from the code and lifts it to the type level, needing only occasional guidance when it can't figure enough out by itself. We don't seem to have the same level of help yet with dependent types. A detailed comment in a Reddit thread: <https://www.reddit.com/r/haskell/comments/3zc81v/tradeoffs_of_dependent_types_xpost_from_ridris/cyl0bm1/> https://www.reddit.com/r/haskell/comments/3zc81v/tradeoffs_o... indicates that we still can't use them on large scale systems. This was some time ago but AFIK we still have all the problems listed. I wonder if there's good work on inference of minimal dependent types for APIs etc. I am not very familiar with current work so would be very interested in getting references. It seems that deriving canonical minimal types would resolve a lot of the listed problems.

mikekchar 8y ago

For me, notation is everything. A computer program is a model of a problem. There is more than one representation of that problem: in the static code and in the running code. If you go to a kind of naive way of writing programs (that we all went through when we were first starting out), you write the code and then you step through it (either on paper, or with a debugger), viewing how the code is running. There are many techniques available for helping you reason about your code. However, it's important to understand that software code is a notation for modelling the problem. Often formal methods introduce another notation that proves that the encoding of the problem in the first notation is "correct" according to some definition of "correct". The more we move into modelling the correctness in the second notation, the more we move the burden of reasoning about the issue to the "code" in the second notation. It's often very useful to model the problem more than once. For example, I'm quite a big fan of unit tests. "Give the code in the system, I expect X to be true/false in this situation". I'm just as likely to make mistakes in my unit tests as I am with the production code. However, it's the comparison of the two that allows you to reason effectively about the code. They are two sides of the same coin (intentionally coupled -- which, as an aside, is why you should avoid trying to decouple your tests from your production code!!!). Even though it is useful to model twice, I'm not really sold on the idea of doing it in general (and I have a very specific idea of how to write unit tests that's heavily coloured by this point of view). Everything that you add to the code should make reasoning about something easier and more convenient than not doing it. Otherwise you are better off with just writing the production code. You will have less complexity to deal with overall. In my opinion, a good example of a tool that helps incredibly well are strongly typed languages with type inference systems. For a small penalty of type notation, the system can tell me, without a doubt, when I've made a mistake with the types of my variables. Not only that, but the notation itself allows me to reason about why I've gotten myself into a problem. It can even help me reason about what the function does, without having to even look at the implementation. This is incredibly helpful. I think as we go forward, we need to be looking for this kind of tool. Dependent types seem like a perfect example of this. However, there is always going to be a small price to pay. Writing code in a statically typed language is harder than writing code in a dynamically typed language -- precisely because the dynamically typed language allows you to write code without having to think up front about the consequences. Of course, you may leave bugs in your code because of it, but the initial cognitive load is smaller. Similarly, it's much better to write code where you can reason about the run time behaviour without it running, but that is much harder than writing some code and walking through it, playing "computer". We need to balance these kinds of factors because a tool that is not used is a useless tool. I'd be perfectly happy to work in a pure functional, statically typed language because it is much easier to reason about my code. Many of my colleagues simply are not willing (or possibly even able) to pay the upfront cost of working in that kind of ecosystem. Hence, I'm not able to work in it either.

thrmsforbfast 8y ago
This was a great comment. The fact that new notations/representations (be that tests, simulations, formal methods, etc.) must justify their additional cognitive overhead is a great point. Aside from unit and integration tests, I think that substantial new notation/infrastructure is most justifiable when the second notation/setting allows you to model parts of the problem that can't be modeled in the original notation. Embedded software is a good example. Although there are some tools that allow you to model the physical system alongside the control software, typically the code is written in C and so there's no way of expressing very important aspects of the problem in the implementation language. So a second notation can help. For example, simulators and HiL setups for testing or things like https://github.com/LS-Lab/KeYmaeraX-release https://github.com/LS-Lab/KeYmaeraX-release for formal methods. Security is another good example. Typically code does not include an explicit threat model or explicit security properties, and these aspects of the problem are often scattered across the code and difficult to reason about. So being able to capture those things directly in a second notation can add a lot. For example, automatic vulnerbaility scaners for testing or https://tamarin-prover.github.io/ https://tamarin-prover.github.io/ for formal methods. Distributed/fault-tolerant systems are yet another example where it's very hard to state the thing you want to state in the implementation language. Netflix's chaos monkey comes to mind.
jedharris 8y ago
Agree about type inference being a great tool along the lines we need. Notably it extracts information from the code and lifts it to the type level, needing only occasional guidance when it can't figure enough out by itself. We don't seem to have the same level of help yet with dependent types. A detailed comment in a Reddit thread: <https://www.reddit.com/r/haskell/comments/3zc81v/tradeoffs_of_dependent_types_xpost_from_ridris/cyl0bm1/> https://www.reddit.com/r/haskell/comments/3zc81v/tradeoffs_o... indicates that we still can't use them on large scale systems. This was some time ago but AFIK we still have all the problems listed. I wonder if there's good work on inference of minimal dependent types for APIs etc. I am not very familiar with current work so would be very interested in getting references. It seems that deriving canonical minimal types would resolve a lot of the listed problems.