Thanks, that makes good sense from what I remember. When integrating proofs in one's program, should one remember to use a compiler switch to disable a proof's evaluation in production code for performance?
On Thursday, March 8, 2018 at 9:54:13 PM UTC-5, gmhwxi wrote: > > > >> Aren't proofs a static construct ... > > No. This is a common misconception. Proofs are dynamic > but the evaluation of proofs cause no effect on the evaluation > of a program (containing proofs) and can thus be omitted. Often > this is referred to as proof irrelevance. > > You can think about it like this: > > Static terms are used to clarify dynamic terms. Proofs are clarified > by static terms (props) but they themselves cannot be used to clarify > dynamic terms. > > On Thu, Mar 8, 2018 at 9:47 PM, Brandon Barker <[email protected] > <javascript:>> wrote: > >> I saw the following at the beginning of "A Tutorial on Programming >> Features in ATS": >> >> *The code in the dynamics of ATS is colored red unless it represents >> proofs, for which the color dark green is used* >> >> This is slightly confusing to me. (And I get the sense, maybe I asked >> this question before, years ago - if so, apologies): aren't proofs a static >> construct, in the sense that they aren't executed during a program's >> runtime? >> >> -- >> You received this message because you are subscribed to the Google Groups >> "ats-lang-users" group. >> To unsubscribe from this group and stop receiving emails from it, send an >> email to [email protected] <javascript:>. >> To post to this group, send email to [email protected] >> <javascript:>. >> Visit this group at https://groups.google.com/group/ats-lang-users. >> To view this discussion on the web visit >> https://groups.google.com/d/msgid/ats-lang-users/29e80558-538d-4111-a4d8-aed95c83cb32%40googlegroups.com >> >> <https://groups.google.com/d/msgid/ats-lang-users/29e80558-538d-4111-a4d8-aed95c83cb32%40googlegroups.com?utm_medium=email&utm_source=footer> >> . >> > > -- You received this message because you are subscribed to the Google Groups "ats-lang-users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/ats-lang-users. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/033e5485-f0d2-4c2e-8cc3-f4d62134e102%40googlegroups.com.
