Proving code correct is orders of magnitude harder than the rest IMHO. It is amazing that enough progress has been made that large scale projects like CompCert and seL4 can now be done successfully by small teams of people.
I'd say it is not hard but impossible. I have a hard enough time to get requirements specifications that are unambiguous. Proving I coded what I was asked for is not a rigorous science practice. It's a social contract.
Hard Things in Computer Science
31–40 of 46 posts
Re: Hard Things in Computer Science
#32Computing with limited numerical precision (aka floating point) is 1.000000000000003534 additional hard thing to deal with.
Modern computers can calculate with a very large finite precision using decimal types. We have so much machine to waste today that if calculations of that sort are relevant, just throw more iron at it.
Now sometimes you don’t need this level of effort but don’t underestimate just how much CPU you might be leaving on the floor. Sometimes it can mean what seems like an impractically slow algorithm actually runs fine. Even if you ran an infinite precision version of the ML code on a modern desktop CPU you might struggle to get perf to get the system to run in real-time (we needed to run the simulation within 5-10 ms and then do a bunch of even more complicated math to compute the blue dot location every 250ms)
Re: Hard Things in Computer Science
#33Earlier quoted context omitted.
Yeah I stopped reading at that point, cache invalidation is not 'also known as TTL'.
It's a simplification but it isn't wrong. Mostly.
Re: Hard Things in Computer Science
#34Re: Hard Things in Computer Science
#35Proving code correct is orders of magnitude harder than the rest IMHO. It is amazing that enough progress has been made that large scale projects like CompCert and seL4 can now be done successfully by small teams of people.
I'd say it is not hard but impossible. I have a hard enough time to get requirements specifications that are unambiguous. Proving I coded what I was asked for is not a rigorous science practice. It's a social contract.
And then, you can formally prove that code does not have certain kinds of bugs. You cannot formally prove that code has no bugs, because 1) you don't even know all possible kinds of bugs, and 2) even for the kinds you do know, you don't have formal proofs for all of them.
Re: Hard Things in Computer Science
#36Earlier quoted context omitted.
I'd say it is not hard but impossible. I have a hard enough time to get requirements specifications that are unambiguous. Proving I coded what I was asked for is not a rigorous science practice. It's a social contract.
I agree with "impossible". In fact, it's worse than you say. Specs can be unambiguous and still be wrong. How do you prove that the specification doesn't have a bug? And then, you can formally prove that code does not have certain kinds of bugs. You cannot formally prove that code has no bugs, because 1) you don't even know all possible kinds of bugs, and 2) even for the kinds you do know, you don't have formal proof…
Re: Hard Things in Computer Science
#37Re: Hard Things in Computer Science
#38Re: Hard Things in Computer Science
#39Re: Hard Things in Computer Science
#40As another problem of applied CS I also suggest to add "Character Encoding" to the list of strongly underestimated complex problems :)
Agreed, and also just text in general, internationalization, line-breaks, horizontal vs vertical text, left-right vs right-left, etc, etc. OTOH that starts getting quite "application oriented" and where do you draw the line? compsci is perhaps more about computation and how to achieve it, analyze it, etc, and in that case even dates and times should not be in the list, being an "application" domain concern.
Text Rendering Hates You - https://news.ycombinator.com/item?id=21105625 - Sept 2019 (170 comments)