3 ms·

Programming languages from Adga to Monte are coming now with the ability to encode meaningful real-world proofs, and the compilers are checking those proofs. W

Programming languages from Adga to Monte are coming now with the ability to encode meaningful real-world proofs, and the compilers are checking those proofs. We could be writing a lot of verified code, if we wanted.

adrianN 9y ago
You radically overestimate the skills of the average programmer.
- DonbunEf7 9y ago
  In Monte, this object is proven by the compiler/interpreter to be transitively immutable: object popsicle as DeepFrozen: to getFlavor() :Str: # Obviously immutable. return "lime" to getObservedColor(eye): # The eye might not be immutable, but that's still okay. # All that's required is that this object not secretly stash the eye. return eye.observeCMYK(38, 0, 78, 1) You radically underestimate the intelligence of your fellow humans.
  - adrianN 9y ago
    In C++ the same can be achieved by using "const". I don't think that such properties are very useful in preventing security problems.
- atqtion 9y ago
  You are correct when you say that writing verifiable/verified code is a separate skill that not many programmers possess. But crucially, it's a skills gap -- not an intelligence gap -- that stands in their way. For most properties, writing verified code doesn't require that much more intelligence than writing normal code. Different skills, but in most cases not much more intelligence. But I don't think a skills gap is the most pressing barrier. There is an intrinsic difference in difficulty between stating conjectures and proving theorems. There's no silver bullet here, including either education or raw intelligence. The latter is, intrinsically, more difficult and more time consuming.
  - adrianN 9y ago
    I'm reasonably sure that for all things where a proof would be helpful, that is properties that the programmer has a nontrivial chance of getting the implementation wrong and not catching the mistake with a test, a correctness proof is a lot harder than writing a correct implementation. I've dabbled a bit with Coq and Isabelle and certainly found this to be the case. Stronger type systems help a lot with common security problems. Memory safety and a system to express taint of inputs eliminate a huge class of potential problems. They are still very, very far from correctness proofs that could catch actual logic bugs.

adrianN 9y ago

You radically overestimate the skills of the average programmer.

DonbunEf7 9y ago
In Monte, this object is proven by the compiler/interpreter to be transitively immutable: object popsicle as DeepFrozen: to getFlavor() :Str: # Obviously immutable. return "lime" to getObservedColor(eye): # The eye might not be immutable, but that's still okay. # All that's required is that this object not secretly stash the eye. return eye.observeCMYK(38, 0, 78, 1) You radically underestimate the intelligence of your fellow humans.
- adrianN 9y ago
  In C++ the same can be achieved by using "const". I don't think that such properties are very useful in preventing security problems.
atqtion 9y ago
You are correct when you say that writing verifiable/verified code is a separate skill that not many programmers possess. But crucially, it's a skills gap -- not an intelligence gap -- that stands in their way. For most properties, writing verified code doesn't require that much more intelligence than writing normal code. Different skills, but in most cases not much more intelligence. But I don't think a skills gap is the most pressing barrier. There is an intrinsic difference in difficulty between stating conjectures and proving theorems. There's no silver bullet here, including either education or raw intelligence. The latter is, intrinsically, more difficult and more time consuming.
- adrianN 9y ago
  I'm reasonably sure that for all things where a proof would be helpful, that is properties that the programmer has a nontrivial chance of getting the implementation wrong and not catching the mistake with a test, a correctness proof is a lot harder than writing a correct implementation. I've dabbled a bit with Coq and Isabelle and certainly found this to be the case. Stronger type systems help a lot with common security problems. Memory safety and a system to express taint of inputs eliminate a huge class of potential problems. They are still very, very far from correctness proofs that could catch actual logic bugs.