Re:What is Symbolic Computation?
by Retra on Thursday June 30, 2016 @01:48PM
(#12010345)
Now you're confusing the implementation with the abstraction. Types can be modeled by tags. They can be modeled by trees. Or any other data structure that you can analyze with a program.
>The actual function of types, on the other hand, is to prove simple propositions about a program without running it.
The value of a tag proves something about the program. You're just proving it at run-time rather than compile time.
Which is an artificial distinction anyway, since your static types theorems are being proved during the run-time of your static type checker. All theorems are proven during some run-time.
>The actual function of types, on the other hand, is to prove simple propositions about a program without running it.
The value of a tag proves something about the program. You're just proving it at run-time rather than compile time.
Which is an artificial distinction anyway, since your static types theorems are being proved during the run-time of your static type checker. All theorems are proven during some run-time.