Originally, praxi is for axioms and prfun for proof functions that need to
be implemented.
However, this is not enforced in the current implementation of ATS.On Friday, March 27, 2015 at 5:56:21 AM UTC-4, Kiwamu Okabe wrote:
Hi all,
I am reading “Introduction to Programming in ATS” that is saying:
Enforcing this requires some form of global flow analysis.
I hope that someone will have the motivation to implement it someday.
My attitude towards the need for implementing a particular prfun is that it
should
be programmer-centric: The programmer is in the position to make that
decision
(rather than it is mandated by the typehecker).
This is also a kind of fairness issue for me. When writing code, one does
all sorts
reasoning implicitly. If someone wants to introduce proof functions to make
some reasoning
more explicit, why should the person be penalized with the requirement of
constructing explicit
proofs for the introduced proof functions?On Friday, March 27, 2015 at 5:12:16 PM UTC-4, Barry Schwartz wrote:
Originally, praxi is for axioms and prfun is for proof functions that
needs
to be implemented.
However, this is not enforced in the current implementation of ATS.
I am a bit curious if enforcement is in the plans.
I could see it as a ‘warning only’ stylistic check. My reasoning is
that proofs in ATS are more to ensure you did not make an error in
your statement than they are a formal requirement; thus there is no
fundamental difference between a praxi and a prfun.
I would definitely appreciate a flag to actually check if prfuns are implemented. I understand why the default is as it is but I’d prefer the extra assurance from the compiler rather than having to adopt coding standards enforcing actually proving proofs.
Originally, praxi is for axioms and prfun is for proof functions that needs
to be implemented.
However, this is not enforced in the current implementation of ATS.
I am a bit curious if enforcement is in the plans.
I could see it as a ‘warning only’ stylistic check. My reasoning is
that proofs in ATS are more to ensure you did not make an error in
your statement than they are a formal requirement; thus there is no
fundamental difference between a praxi and a prfun.
There is such a flag in ATS1, but it is not really useful as turning it on
almost always leads to
the output of a great number of warning/error messages. As I see it, one
needs to re-build the basic
library support for ATS in order to make such a flag useful.On Friday, March 27, 2015 at 6:24:54 PM UTC-4, Shea Levy wrote:
I would definitely appreciate a flag to actually check if prfuns are
implemented. I understand why the default is as it is but I’d prefer the
extra assurance from the compiler rather than having to adopt coding
standards enforcing actually proving proofs.
Originally, praxi is for axioms and prfun is for proof functions that
needs
to be implemented.
However, this is not enforced in the current implementation of ATS.
I am a bit curious if enforcement is in the plans.
I could see it as a ‘warning only’ stylistic check. My reasoning is
that proofs in ATS are more to ensure you did not make an error in
your statement than they are a formal requirement; thus there is no
fundamental difference between a praxi and a prfun.
I often use ‘praxi’ to indicate something that cannot be proven
within ATS. It refers to a form of truth that is external to ATS (e.g.,
the fact that the sun rises from the east)
I use prfun to indicate that a statement can be established based on
some existing ones (but I may not be willing to construct a proof for it).
In the future, if we really need to find a way to ensure that a declared
proof
function must be given a proof, then we could always try to introduce
another
keyword for doing so.On Saturday, March 28, 2015 at 10:38:25 PM UTC-4, Barry Schwartz wrote:
This is also a kind of fairness issue for me. When writing code, one
does
all sorts
reasoning implicitly. If someone wants to introduce proof functions to
make
some reasoning
more explicit, why should the person be penalized with the requirement
of
constructing explicit
proofs for the introduced proof functions?
I’d be perfectly happy with the choice of prfun vs praxi being
entirely stylistic, as long as one could count on that. My concern is
having code broken by a future version of ATS that enforces a
difference.