3 ms·

Not all programs have a compile time (and for those that do, there's a one-to-many relationship between it and runtimes), but there's always a distinction betwe

Not all programs have a compile time (and for those that do, there's a one-to-many relationship between it and runtimes), but there's always a distinction between runtime and write-time. I do not see how one could write a program without having in mind specific semantics for each identifier you introduce, and if they have specific semantics, are they not at least implicitly typed, whether or not they are statically typed? The author seems to want to use dynamic typing in a restricted manner, to help in testing and debugging and understanding a program, particularly within a REPL. Further down, he seems to be saying that the lack of empirical evidence on how this works in practice (on account of it rarely, if ever, being used in available tooling) seems to suggest it is difficult.

zozbot234 4y ago
Why do you assume that one can't assign a semantics to code that happens to be included within the program as a runtime construct? Such semantics might even be "compile-time" checked in a conventional way, if one can come up with a machine-checked proof that the runtime treatment of such "constructs" does preserve whatever semantics one cares about. Of course this runs into concerns with Turing-completeness in the fully general case, but for many practical scenarios such a check might well be feasible.
- mannykannot 4y ago
  I'm not saying you cannot do that (and, specifically, I am not saying you cannot do the sort of things the author seems to want to do.) I am saying that I don't see how you can write the program in the first place, unless you have some semantics in mind for every identifier you introduce. To add to that, I doubt to can perform a runtime substitution unless the substitution conforms to the semantics of the original design. This seems to be the case with the author's examples, which extend the original types with a sidechannel for getting information about the execution of the program.

zozbot234 4y ago

Why do you assume that one can't assign a semantics to code that happens to be included within the program as a runtime construct? Such semantics might even be "compile-time" checked in a conventional way, if one can come up with a machine-checked proof that the runtime treatment of such "constructs" does preserve whatever semantics one cares about. Of course this runs into concerns with Turing-completeness in the fully general case, but for many practical scenarios such a check might well be feasible.

mannykannot 4y ago
I'm not saying you cannot do that (and, specifically, I am not saying you cannot do the sort of things the author seems to want to do.) I am saying that I don't see how you can write the program in the first place, unless you have some semantics in mind for every identifier you introduce. To add to that, I doubt to can perform a runtime substitution unless the substitution conforms to the semantics of the original design. This seems to be the case with the author's examples, which extend the original types with a sidechannel for getting information about the execution of the program.