# Serious kernel bug caused by programming in C

**URL:** <https://discourse.ats-lang.org/t/serious-kernel-bug-caused-by-programming-in-c/204>\
**Category:** Google Group\
**Created:** [October 16, 2014, 11:31pm UTC](https://discourse.ats-lang.org/t/serious-kernel-bug-caused-by-programming-in-c/204 "2014-10-16T23:31:04Z")\
**Posts on this page:** 3\
**Page:** 1

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [October 16, 2014, 11:31pm UTC](https://discourse.ats-lang.org/t/serious-kernel-bug-caused-by-programming-in-c/204/1 "2014-10-16T23:31:04Z")

</div>

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.

---

<div class="post-metadata">

**Author:** ![Raoul\_Duke](https://avatars.discourse-cdn.com/v4/letter/r/bbe5ce/32.png) [@Raoul\_Duke](https://discourse.ats-lang.org/u/Raoul_Duke)\
**Post date:** [October 16, 2014, 11:43pm UTC](https://discourse.ats-lang.org/t/serious-kernel-bug-caused-by-programming-in-c/204/2 "2014-10-16T23:43:41Z")

</div>

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  
🙂

---

<div class="post-metadata">

**Author:** ![gmhwxi](https://avatars.discourse-cdn.com/v4/letter/g/67e7ee/32.png) [@gmhwxi](https://discourse.ats-lang.org/u/gmhwxi)\
**Post date:** [October 17, 2014, 12:51am UTC](https://discourse.ats-lang.org/t/serious-kernel-bug-caused-by-programming-in-c/204/3 "2014-10-17T00:51:43Z")

</div>

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](mailto: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  
> 🙂
> 
> –  
> 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 [ats-lang-user...@googlegroups.com](mailto:ats-lang-user...@googlegroups.com).  
> To post to this group, send email to [ats-lan...@googlegroups.com](mailto:ats-lan...@googlegroups.com).  
> Visit this group at [http://groups.google.com/group/ats-lang-users](http://groups.google.com/group/ats-lang-users).  
> To view this discussion on the web visit  
> [https://groups.google.com/d/msgid/ats-lang-users/CAJ7XQb4iYbh-F1BKQeN4zLc8LbEvsSbMFsvvy0LfxYGBv4f6nw%40mail.gmail.com](https://groups.google.com/d/msgid/ats-lang-users/CAJ7XQb4iYbh-F1BKQeN4zLc8LbEvsSbMFsvvy0LfxYGBv4f6nw%40mail.gmail.com)  
> .