4 ms·
One of these days I'll get around to Rust. I don't think it's fundamentally difficult, just different from most people's cowboy programming. I'm much more excit
by krapht 9y ago
One of these days I'll get around to Rust. I don't think it's fundamentally difficult, just different from most people's cowboy programming. I'm much more excited these days about program extraction from verified programs written in Idris or Coq, which is on a whole other level of pain and suffering.
- timClicks 9y agoDoes anyone have any experience regarding TLA+. Does it make formal verification at least slightly less painful?
- bitL 9y agoMind you even correctness checkers aren't panacea - they won't go all the way down to check if you are using IEEE 754 correctly and handle all possible edge cases and rather assume "well-defined math properties". And as Donald Knuth used to say: "Beware of bugs in the above code; I have only proved it correct, not tried it."
- jacobush 9y agoMade me think, maybe they should check if you are using IEEE 754 correctly...
- TheDong 9y agoNumeric 'correctness' is a business-problem property. For a game engine, correctness is speed and "right enough". For a research physics simulation, it may be "as right as possible". You can't check whether floating point inaccuracy is correct generically because the definition is entirely dependent on the business needs of the program in question.
- jononor 9y agoOne could enforce the strictest correctness by default, and then allow/require to opt-out in cases where programmer decides it is OK, like a game.
- bitL 9y agoAn "ancient" conversation demonstrating this issue with early Coq: http://grouper.ieee.org/groups/754/email/msg00574.html http://grouper.ieee.org/groups/754/email/msg00574.html