Yes or no, depending on how the code is written in ATS.
Say we have the following if-statement:
If
(mytest())
{
do_something();
} else {
do_something_else();
}
And a rule says that
do_something() can be called only if mytest() returns true.
In C, the programmer is responsible for enforcing the rule.
If mytest() changes into !mytest(), the rule is broken and the programmer
may not notice it.
The rule can be enforced in ATS through typechecking: do_something is
required to take a proof argument and such a proof can only be returned if
mytest() returns true. In this way, if mytest() changes into !mytest(), the
typechecker will complain. This is really the essence of programming with
theorem-proving.On Thursday, October 16, 2014 6:43:36 PM UTC-4, Barry Schwartz wrote:
I presume this could have been avoided more easily without testing,
were the kernel written in ATS:
https://bugs.gentoo.org/show_bug.cgi?id=525548
I was running that kernel until yesterday and suppose I should now do
filesystem checks.
i think this particular bug would easily be detected if people used
proper safe type aliases instead of raw primitive types, which seems
easier to advertise than saying anything with the word “proof” in it
I looked it again. Strangely, I originally had the impression that the bug was
caused by a misplaced negation (!). It is not. As you said, this one
is really trivial
to detect in a typed language. Now, tell it to the Scheme people :)On Thu, Oct 16, 2014 at 7:43 PM, Raoul Duke rao...@gmail.com wrote:
i think this particular bug would easily be detected if people used
proper safe type aliases instead of raw primitive types, which seems
easier to advertise than saying anything with the word “proof” in it
