3 ms·

That's not possible. If I'm about to write some code that assumes the gyroscope is spinning, I might assert that the gyroscope is spinning. That cannot be check

That's not possible. If I'm about to write some code that assumes the gyroscope is spinning, I might assert that the gyroscope is spinning. That cannot be checked at compile time. Also, until almost all the world's software has been rewritten in Idris, compile time checks just cannot do very much. This is a reality of our century. Keep in mind that my original example isn't really about checking that x == 5. The focus is not on checking integer values, it's just an example. Although, again, even something as simple as checking integer values is beyond the compile time abilities of our compilers. Halting problem sends its regards!

kccqzy 3y ago
But how do you know that the gyroscope is or isn't spinning when that code is written? You don't. You might as well do a regular check for if the gyroscope is spinning, and if not return an error. You do not need to have the entire world's software rewritten in Idris (which I don't even like that much). This is purely local reasoning that can be accomplished by minor changes to existing languages if we want to. The compiler doesn't need access to the world. It is you who are unnecessarily raising the bar for what you expect compilers to do and then throwing in the towel just because the compiler can't actually do it. Any argument that invokes the halting problem has a standard response: you don't need to handle every case; perfect is the enemy of good. Furthermore it is often better to have the programmer rewrite the code to help the compiler deduce these facts, because helping the compiler also helps future readers of the code.
- diogenes4 3y ago
  > You might as well do a regular check for if the gyroscope is spinning, and if not return an error. I mean yea, it'd be great if programs propagated every possible error state or violated invariant possible up the stack. I don't see that happening any time soon, nor that being worth the effort. When was the last time you checked and propagated allocation failure? I'm guessing not in a long time, unless you're working with a runtime where allocation failure is explicitly handled as part of normal program progression (like the `alloc` libc family) and where you expect to run into memory limits. Granted, exceptions are a good deal easier to handle "invisibly", but those have notably been absent from this discussion except in the case where they are unhandled as an assert might trigger.

kccqzy 3y ago

But how do you know that the gyroscope is or isn't spinning when that code is written? You don't. You might as well do a regular check for if the gyroscope is spinning, and if not return an error. You do not need to have the entire world's software rewritten in Idris (which I don't even like that much). This is purely local reasoning that can be accomplished by minor changes to existing languages if we want to. The compiler doesn't need access to the world. It is you who are unnecessarily raising the bar for what you expect compilers to do and then throwing in the towel just because the compiler can't actually do it. Any argument that invokes the halting problem has a standard response: you don't need to handle every case; perfect is the enemy of good. Furthermore it is often better to have the programmer rewrite the code to help the compiler deduce these facts, because helping the compiler also helps future readers of the code.

diogenes4 3y ago
> You might as well do a regular check for if the gyroscope is spinning, and if not return an error. I mean yea, it'd be great if programs propagated every possible error state or violated invariant possible up the stack. I don't see that happening any time soon, nor that being worth the effort. When was the last time you checked and propagated allocation failure? I'm guessing not in a long time, unless you're working with a runtime where allocation failure is explicitly handled as part of normal program progression (like the `alloc` libc family) and where you expect to run into memory limits. Granted, exceptions are a good deal easier to handle "invisibly", but those have notably been absent from this discussion except in the case where they are unhandled as an assert might trigger.