4 ms·

A web site with no bug (I mean, no error) is a web site with no vulnerabilities. Wouldn't that be interesting when your customers trust you with their credit c

A web site with no bug (I mean, no error) is a web site with no vulnerabilities. Wouldn't that be interesting when your customers trust you with their credit card number?

wkornewald 16y ago
Of course I want to have secure code. However, do I have to write 100% of my code in such a verbose language in order to guarantee security? I don't think that any security expert would claim that. It's sufficient if the relevant parts of the system and the communication protocols between your components provide a secure foundation. Writing all of your code in a verbose language would be total overkill and a huge waste of effort. So, in the end a combination of both systems might be the solution. The issue here is that this news post is about "the language of the future". It's definitely far from the language of the future. If at all, it might be a small component of the language(s) of the future (and even for that it should better improve on readability). There's just too much research going into verifiable systems and language theory and by far not enough research into making the majority of our code more expressive and reusable from a very practical point of view.
- loup-vaillant 16y ago
  I didn't see significant examples of Omega, but… I'd be surprised if a language with a Haskell-like syntax is verbose. The verbosity most likely didn't come from the language itself, but from the proofs. Once you've built the foundations, and proven a host of invariants about them, then you don't need to prove much more when you write the rest of the program. I bet Omega supports the very programming model you advocate: invulnerable foundations, and quickly written "rest of the program". If the code you saw was verbose, that's probably because it was foundation code. (After all, standard data structures are par of the foundations.)
Groxx 16y ago
You're implying all vulnerabilities are bugs due to coding error. To take a high-profile recent case: this would do nothing to prevent padding oracle attacks. Or future crypto attacks using techniques unknown to us now. Why? Because the encryption is working as it should. As advertised. As proven. Or imagine you used Rot13 for encryption. Your DB could hold people's credit cards in clear-text; how will this language prevent that from happening? Your website has no authorization tools, so you can access others' data by simply going to their URL; this is still a provably-correct logic structure.
- andolanra 16y ago
  How is any language going to fix the problem of bad programmers programming badly? And, more relevantly—how does the fact that a language can't fix those errors make preventing other errors a useless endeavor? It's true that there's no such thing as a programming language that can only write good/safe/acceptable programs, and a lot of people (myself included) who advertise programming languages as a solution to problems tend to overstate the relevance of type systems, correctness proofs, pure functions, &c, but that doesn't mean you can't eliminate a certain variety of error through good language design or by enforcing programmer rigor.
  - Groxx 16y ago
    It's not, which is the point. loup-vaillant's comment implied that it was possible to write a "perfect" program in a proof-oriented language, as it would have no vulnerabilities, and people could trust your code. I wasn't intending to imply that, because language X does not solve likely-intractable problem Y, language X is worthless. Just that likely-intractable problem Y is likely intractable in language Z as well as X, as it's an inherent quality of the problem. edit: I will however explicitly imply that more syntactically complicated languages are probably more likely to hide many kinds of logic errors. More brainpower spent decoding your code is more brainpower not spent analyzing your logic. Each to their own, clearly; I most definitely side with highly-readable code, and know several people who would likely feel right at home with Omega (e.g.: my brother is a math + philosophy double-major).
    - wkornewald 16y ago
      Regarding "to each their own": Programmers aren't necessarily the best source for an objective view on productivity. This here is a nice example of CS students claiming subjectively which programming style they found easier, contrasted by a more objective comparison of the actual number of bugs in the code in each programming style: http://lambda-the-ultimate.org/node/4070 http://lambda-the-ultimate.org/node/4070 Studies like this tell me to never trust the opinion of a developer about programming languages and programming styles. In some cases not even my own. ;) Of course in this case we had not very experienced developers, but if we look at what expert developers often claim and how widely opinions differ I often have the impression that expert developers' fundamental opinions about programming languages aren't much better than that of a student.
makmanalp 16y ago
First of all, you're assuming that the person who writes the theorems is always correct and is able to describe their code accurately. This is not the case. Second, it's way more easy to take a bunch of common sense measures than to deal with this.
- voxcogitatio 16y ago
  Of course human error applies here too; But it's much simpler to get one type right than to use the type in the right way everywhere. Per example: The Red-Black-Tree implementation mentioned in the examples. If we define a tree that cannot be unbalanced, we can skip all explicit checks for whether the tree is balanced, thus eliminating a source for errors (forgetting/bungling the balance checks) and also increasing productivity (since we don't need to write the balance checks in the first place).
- loup-vaillant 16y ago
  > First of all, you're assuming No I'm not. When I say "no error", that include the specs. For instance, correctly following a specs when the green button set of the emergency shut down makes the interface too astonishing. That's a bug. > Second, it's way more easy to take a bunch of common sense measures than to deal with this. Of course. we never tried it seriously. What we didn't try yet is always more difficult. But if we do, it may very well become easier. I don't know. Anyway, these weren't the point. My point was that the domains where we need bug-free code is broader than we might think at a first glance. Not being able to trust that the code you run is error-free has costs that could very well be more important than taking the time to prove the absence of errors.

A web site with no bug (I mean, no error) is a web site with no vulnerabilities. Wouldn't that be interesting when your customers trust you with their credit card number?

wkornewald 16y ago

Of course I want to have secure code. However, do I have to write 100% of my code in such a verbose language in order to guarantee security? I don't think that any security expert would claim that. It's sufficient if the relevant parts of the system and the communication protocols between your components provide a secure foundation. Writing all of your code in a verbose language would be total overkill and a huge waste of effort. So, in the end a combination of both systems might be the solution. The issue here is that this news post is about "the language of the future". It's definitely far from the language of the future. If at all, it might be a small component of the language(s) of the future (and even for that it should better improve on readability). There's just too much research going into verifiable systems and language theory and by far not enough research into making the majority of our code more expressive and reusable from a very practical point of view.

loup-vaillant 16y ago
I didn't see significant examples of Omega, but… I'd be surprised if a language with a Haskell-like syntax is verbose. The verbosity most likely didn't come from the language itself, but from the proofs. Once you've built the foundations, and proven a host of invariants about them, then you don't need to prove much more when you write the rest of the program. I bet Omega supports the very programming model you advocate: invulnerable foundations, and quickly written "rest of the program". If the code you saw was verbose, that's probably because it was foundation code. (After all, standard data structures are par of the foundations.)

Groxx 16y ago

You're implying all vulnerabilities are bugs due to coding error. To take a high-profile recent case: this would do nothing to prevent padding oracle attacks. Or future crypto attacks using techniques unknown to us now. Why? Because the encryption is working as it should. As advertised. As proven. Or imagine you used Rot13 for encryption. Your DB could hold people's credit cards in clear-text; how will this language prevent that from happening? Your website has no authorization tools, so you can access others' data by simply going to their URL; this is still a provably-correct logic structure.

andolanra 16y ago
How is any language going to fix the problem of bad programmers programming badly? And, more relevantly—how does the fact that a language can't fix those errors make preventing other errors a useless endeavor? It's true that there's no such thing as a programming language that can only write good/safe/acceptable programs, and a lot of people (myself included) who advertise programming languages as a solution to problems tend to overstate the relevance of type systems, correctness proofs, pure functions, &c, but that doesn't mean you can't eliminate a certain variety of error through good language design or by enforcing programmer rigor.
- Groxx 16y ago
  It's not, which is the point. loup-vaillant's comment implied that it was possible to write a "perfect" program in a proof-oriented language, as it would have no vulnerabilities, and people could trust your code. I wasn't intending to imply that, because language X does not solve likely-intractable problem Y, language X is worthless. Just that likely-intractable problem Y is likely intractable in language Z as well as X, as it's an inherent quality of the problem. edit: I will however explicitly imply that more syntactically complicated languages are probably more likely to hide many kinds of logic errors. More brainpower spent decoding your code is more brainpower not spent analyzing your logic. Each to their own, clearly; I most definitely side with highly-readable code, and know several people who would likely feel right at home with Omega (e.g.: my brother is a math + philosophy double-major).
  - wkornewald 16y ago
    Regarding "to each their own": Programmers aren't necessarily the best source for an objective view on productivity. This here is a nice example of CS students claiming subjectively which programming style they found easier, contrasted by a more objective comparison of the actual number of bugs in the code in each programming style: http://lambda-the-ultimate.org/node/4070 http://lambda-the-ultimate.org/node/4070 Studies like this tell me to never trust the opinion of a developer about programming languages and programming styles. In some cases not even my own. ;) Of course in this case we had not very experienced developers, but if we look at what expert developers often claim and how widely opinions differ I often have the impression that expert developers' fundamental opinions about programming languages aren't much better than that of a student.

makmanalp 16y ago

First of all, you're assuming that the person who writes the theorems is always correct and is able to describe their code accurately. This is not the case. Second, it's way more easy to take a bunch of common sense measures than to deal with this.

voxcogitatio 16y ago
Of course human error applies here too; But it's much simpler to get one type right than to use the type in the right way everywhere. Per example: The Red-Black-Tree implementation mentioned in the examples. If we define a tree that cannot be unbalanced, we can skip all explicit checks for whether the tree is balanced, thus eliminating a source for errors (forgetting/bungling the balance checks) and also increasing productivity (since we don't need to write the balance checks in the first place).
loup-vaillant 16y ago
> First of all, you're assuming No I'm not. When I say "no error", that include the specs. For instance, correctly following a specs when the green button set of the emergency shut down makes the interface too astonishing. That's a bug. > Second, it's way more easy to take a bunch of common sense measures than to deal with this. Of course. we never tried it seriously. What we didn't try yet is always more difficult. But if we do, it may very well become easier. I don't know. Anyway, these weren't the point. My point was that the domains where we need bug-free code is broader than we might think at a first glance. Not being able to trust that the code you run is error-free has costs that could very well be more important than taking the time to prove the absence of errors.