3 ms·

Thanks, I will respond to other people here as well. I know a bit of Haskell and want to look at Idris, someday. My point was, there should be a clean (best i

by js8 9y ago

Thanks, I will respond to other people here as well. I know a bit of Haskell and want to look at Idris, someday. My point was, there should be a clean (best if even syntactic) separation between code itself (i.e. what should actually be done) and its properties (like types). Also, because there are two points of view about the properties (human and computer), this separation needs to be there twice (so for example, each type could be specified by computer and by human). I haven't seen a system that would do it, on a systematic level in the programming language. I only gave examples to show where it could be used.

marcosdumay 9y ago
You mean that types should reside on different files, and be inputed by different means? Now I get the entire programming-compiler conversation. It is interesting. I can see some potential there. Yet, I shrug when I think about all the sparse metadata that I will have to check once I discover a low level bug (there is a reason I'm not programming in Smalltalk). Somehow the best place for all that stuff to live is right there at the source code. That means the compiler (IDE) should be editing your files, so it better have a great integration with your version control system.
- js8 9y ago
  > Somehow the best place for all that stuff to live is right there at the source code. That's what I am saying, and that's why it has to be syntactically distinct. Also it needs to be clear what was input by computer and what was input by human, that's the second distinction. Because of how the conversation works. You don't want computer to erase human input, but the result also has to be logically sound. So you need to know both inputs for the comparison and synthesis, which happens at each conversation turn, both human's and computer's. And that's what "type holes" and similar systems lack - they only record the result of the synthesis, not the two different opinions. Which is IMHO wrong.
  - marcosdumay 9y ago
    > You don't want computer to erase human input I will contest that one too :) As long as it is interactive enough, and the history is well marked, there is no reason not to rewrite human code.

by js8 9y ago

marcosdumay 9y ago

You mean that types should reside on different files, and be inputed by different means? Now I get the entire programming-compiler conversation. It is interesting. I can see some potential there. Yet, I shrug when I think about all the sparse metadata that I will have to check once I discover a low level bug (there is a reason I'm not programming in Smalltalk). Somehow the best place for all that stuff to live is right there at the source code. That means the compiler (IDE) should be editing your files, so it better have a great integration with your version control system.

js8 9y ago
> Somehow the best place for all that stuff to live is right there at the source code. That's what I am saying, and that's why it has to be syntactically distinct. Also it needs to be clear what was input by computer and what was input by human, that's the second distinction. Because of how the conversation works. You don't want computer to erase human input, but the result also has to be logically sound. So you need to know both inputs for the comparison and synthesis, which happens at each conversation turn, both human's and computer's. And that's what "type holes" and similar systems lack - they only record the result of the synthesis, not the two different opinions. Which is IMHO wrong.
- marcosdumay 9y ago
  > You don't want computer to erase human input I will contest that one too :) As long as it is interactive enough, and the history is well marked, there is no reason not to rewrite human code.