5 ms·
Nothing guarantees that code is bug free. We will always have to interact with hardware, and although we can have high confidence in the hardware the physical w
by voxl 9y ago
Nothing guarantees that code is bug free. We will always have to interact with hardware, and although we can have high confidence in the hardware the physical world has a habit of changing out from under us.
Your argument is very strange. We use type systems not because we think we'll write perfect code, but because we know it will reduce the likelihood of making mistakes in our code (at least, when that type system is sound).
It seems like you're against writing proofs that your code is correct because you think you'll do better. I have a very hard time believing that, seeing as you probably aren't writing your own assembly (that beats a compiler) most if any of the time.
- auggierose 9y agoFormally proving something is just very expensive. The difference between the cost of an informal understanding of the correctness of your code, and the cost of formally proving it in a theorem prover is usually at least one order of magnitude (if you are lucky). A compiler though with a type system actually REDUCES your cost. So these are very different beasts.
- somenewacc 9y agoType checking your code is, in a sense, a formal proof. That is, your types encode theorems, and the compiler check them. The article actually alludes to this, linking to this: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
- auggierose 9y agoYeah, I should have been more specific in my comment: I don't mean type systems like in Agda or Idris or Coq ..., but where writing down the types is not a big deal, because otherwise you are doing theorem proving with all the associated costs. In short: I like both my type systems and my theorem proving without any involvement of Curry-Howard :D
- qznc 9y agoRelated: Hoare looks back at formally proving programs correct https://m.cacm.acm.org/magazines/2009/10/42360-retrospective-an-axiomatic-basis-for-computer-programming/fulltext https://m.cacm.acm.org/magazines/2009/10/42360-retrospective...
- david-gpu 9y agoThe problem is that these formal proof systems are often marketed as tools to write "bug free code". You will see statements along the lines of "this code is proven to be bug-free", etc. They over-sell and under-deliver. When you also consider that performing these proofs takes a very significant amount of time, you end up with something with very limited applicability for the vast majority of software development scenarios. That's all I'm saying. Please don't argue against a strawman.
- icebraining 9y agoCan you provide an example of a system being marketed as a tool to write "bug free code"? I saw nothing of the sort in the sites of Coq, TLA+ or Isabelle. Are you sure you're not the one arguing against a strawman?
- deleted 9y ago[deleted]
- david-gpu 9y agoIn these comments there are several examples of folks selling an algorithm as "proven" and later turning out to be buggy.
- icebraining 9y agoRight, because they are proven. It's your assumption that proven == bug-free that is incorrect.
- dtornabene 9y agoYou mean like, say, seL4? Pretty sure that kernel is seeing some very real "applicability".
- seanc 9y ago"Beware of bugs in the above code; I have only proved it correct, not tried it. " - Don Knuth
- dllthomas 9y agoOf course, Knuth's proof was not mechanically checked...