4 ms·
One of my Uni professors was working on Proof-carrying code *(https://en.wikipedia.org/wiki/Proof-carrying_code https://en.wikipedia.org/wiki/Proof-carrying_cod
by kn1ght 5y ago
One of my Uni professors was working on Proof-carrying code *(https://en.wikipedia.org/wiki/Proof-carrying_code https://en.wikipedia.org/wiki/Proof-carrying_code). I got a cursory involvement. Although I agree with you, the fact that there is a way forward and is entirely based in mathematics (on the formal side) makes me also agreeable with OP. I don't see a contradiction. If you talk about the more informal side- the way something is used does not necessarily define its nature.
- jhanschoo 5y agoIndeed, I don't disagree with OP. I just felt compelled to point major problems with Dijkstra's argument, because it's somewhat generally known yet its very real shortcomings aren't as widely known. The general response seems to be that "yeah, ideally we should be more mathematically rigorous with programs if we have time and mathematical expertise", but few have sufficient exposure to formal methods to understand that it's far from the panacea the memo makes it out to be and there are more reasons not to do it than just time and expertise.
- UncleMeat 5y agoThere is a way forward, but it is tedious as all hell. I love formal methods. I spent years in grad school working in it. But the truth is that formal reasoning struggles to scale to interesting programs, especially if you have to consider open programs, and is utterly incoherent for most software engineers. You can compare something like symbolic execution, which seems amazingly elegant and powerful, with coverage guided fuzzing, which is hacky and random. Coverage guided fuzzing eats symbolic execution for lunch.