3 ms·

I agree with everything you've said except the line about formal correctness proofs. I'd in fact be willing to replace "unit tests" with correctness proofs at a

by tel 13y ago

I agree with everything you've said except the line about formal correctness proofs. I'd in fact be willing to replace "unit tests" with correctness proofs at almost every point in your comment and stand behind it myself... given that I get to define "correctness proof" carefully. In particular, I want to appeal for using "the most formal thing reasonable" whenever possible. If you're writing highly abstract code, you would likely be amazed at how simply you can write down and prove it's behavior. For less abstract code, some formal properties may still be available and provable, some available but difficult to prove and better verified using exhaustivity or probabilistic property checking [0], and finally some are simply unknown. My point is that unit tests are one of the very weakest forms of verification. They should be traded for more powerful techniques at every availability. Availability is, today, still an issue, but this is precisely why dependently typed language research is interesting. In Idris you can write your core code alongside a machine-checked proof of its correctness. You can verify your outside interface by nearly autogenerating an interface fuzzer and checking encode/decode roundtrips or system fixed points. Finally, you can compile the whole thing down to Javascript and deploy it atop Meteor if that's your endgame. Idris is just one interesting point on this spectrum. I think availability of formal correctness proving (in capability, expression, organization, and automatic execution) will be a major force in the future of CS. [0] http://en.wikipedia.org/wiki/QuickCheck http://en.wikipedia.org/wiki/QuickCheck

agentultra 13y ago
Maybe it's because lisp has warped my brain but I'm not entirely sold on dependent type systems and formal proofs yet. It will be interesting to see if there's anything worthwhile that falls out of it as a consequence of such research but I don't think it's very interesting in its current state. It could use more exploration and I look forward to seeing what comes of it.
- tel 13y ago
  Heh, I find it the next step in evolution after lisp. All the same flexibility, but with a new language that lets you delineate and work with the meaning of your data alongside the data itself. I don't think it's anything resembling practical in its current state, but I think it's absolutely the way of the (possibly deep) future. I want to spend more of my time programming with types than programming with values since that's where my brain honestly is (despite the type languages of today being a bit obtuse) and since the compiler is often able to program the value-level stuff for you.
- tunesmith 13y ago
  The way I see formal correctness proofs is that they'll be useful, but not a panacea. If I have a method that takes a List as a parameter, and returns an Integer, then congratulations - I have just written a formal proof that it is possible to derive an Integer from a List. However, the business need wasn't to derive an Integer from a List - it was something far more specific. So that's why people like the idea of dependent types, in that you can make the type system (mostly) Turing complete, and actually make the types reflect the specification of the problem. And then if you write an implementation of that specification, congratulations, you have proved that that implementation is correct. Which is pretty cool, except that it overlooks the fact that a very large percentage of our bugs are not in our implementation, but in our agreed-upon specification. Almost every bug I encounter (that sneaks its way to QA or production and is reported as a bug) is due to the fact that I validly implemented a specification one way, when the business need actually wanted a slightly different interpretation of the specification, but just wasn't specific enough when they described it. Anyway, formal correctness proofs won't handle that. Really all it means is that the hard part of programming - making sure we're actually developing the correct thing - will be offloaded from implementation to specification. That means that implementation will be more of a code monkey role, while the real art of programming - interpreting and anticipating needs, a role that programmers are vastly under appreciated for - will need to be accomplished by someone that is sort of like a product owner, but far more technical and exacting than is the norm now. I'd imagine many senior level programmers would move into that role - translating business needs into formal specification, and then leaving junior programmers to monkey with the proof itself.
  - tel 13y ago
    I don't see formal proofs replacing acceptance tests. I see them helping you build leak-proof abstractions upon which you assemble the domain where your functionality is implemented. The line between those two positions is blurry and, despite the sound of it, your need to be comprehensive with a formal proof also varies due to possibility and value. All of these things are just tools after all—you use them to produce value. I think you've described one potential future with this technology, but it, I feel, is very narrow. One thing that does seem to be playing out is that for many interesting programs the establishment of the theorem is sufficiently challenging that the proof need not be relegated to "junior programmers" but instead automated entirely. Of course, that said, typically a primary tool in the search for a well-specific theorem is a long series of failed attempts to prove its poorly-specified predecessors.

by tel 13y ago

agentultra 13y ago

Maybe it's because lisp has warped my brain but I'm not entirely sold on dependent type systems and formal proofs yet. It will be interesting to see if there's anything worthwhile that falls out of it as a consequence of such research but I don't think it's very interesting in its current state. It could use more exploration and I look forward to seeing what comes of it.

tel 13y ago
Heh, I find it the next step in evolution after lisp. All the same flexibility, but with a new language that lets you delineate and work with the meaning of your data alongside the data itself. I don't think it's anything resembling practical in its current state, but I think it's absolutely the way of the (possibly deep) future. I want to spend more of my time programming with types than programming with values since that's where my brain honestly is (despite the type languages of today being a bit obtuse) and since the compiler is often able to program the value-level stuff for you.
tunesmith 13y ago
The way I see formal correctness proofs is that they'll be useful, but not a panacea. If I have a method that takes a List as a parameter, and returns an Integer, then congratulations - I have just written a formal proof that it is possible to derive an Integer from a List. However, the business need wasn't to derive an Integer from a List - it was something far more specific. So that's why people like the idea of dependent types, in that you can make the type system (mostly) Turing complete, and actually make the types reflect the specification of the problem. And then if you write an implementation of that specification, congratulations, you have proved that that implementation is correct. Which is pretty cool, except that it overlooks the fact that a very large percentage of our bugs are not in our implementation, but in our agreed-upon specification. Almost every bug I encounter (that sneaks its way to QA or production and is reported as a bug) is due to the fact that I validly implemented a specification one way, when the business need actually wanted a slightly different interpretation of the specification, but just wasn't specific enough when they described it. Anyway, formal correctness proofs won't handle that. Really all it means is that the hard part of programming - making sure we're actually developing the correct thing - will be offloaded from implementation to specification. That means that implementation will be more of a code monkey role, while the real art of programming - interpreting and anticipating needs, a role that programmers are vastly under appreciated for - will need to be accomplished by someone that is sort of like a product owner, but far more technical and exacting than is the norm now. I'd imagine many senior level programmers would move into that role - translating business needs into formal specification, and then leaving junior programmers to monkey with the proof itself.
- tel 13y ago
  I don't see formal proofs replacing acceptance tests. I see them helping you build leak-proof abstractions upon which you assemble the domain where your functionality is implemented. The line between those two positions is blurry and, despite the sound of it, your need to be comprehensive with a formal proof also varies due to possibility and value. All of these things are just tools after all—you use them to produce value. I think you've described one potential future with this technology, but it, I feel, is very narrow. One thing that does seem to be playing out is that for many interesting programs the establishment of the theorem is sufficiently challenging that the proof need not be relegated to "junior programmers" but instead automated entirely. Of course, that said, typically a primary tool in the search for a well-specific theorem is a long series of failed attempts to prove its poorly-specified predecessors.