Witnessing the effectiveness of types in detecting bugs

[gmhwxi]

I did this sort of practice before. And I paid a closer attention this time.

I implemented an interpreter for ATS3 that could handle programs containing

type-errors. I tried it to test some of the ATS3 library code (consisting of about 15K

lines for now). After I got the non-dependent type-checker for ATS3 working, I tried

type-checking the library code (that had already passed unit tests). Did I find bugs?

A large number of them. And I have been writing this kind of code for more than 20

years!

Once I get the dependent and linear type-checker ready, I am certain that many more

bugs will be flushed out. In particular, I am certain that a lot of memory leak bugs will

be detected.  If I extrapolate a bit, I am pretty certain that the bug ratio in C and C++

code is quite significant.

Regarding the COVID-19 cases out there, I suppose we can find many more of them if

our detection method becomes more effective. The same can be said about the bugs in

our code.

--Hongwei

[Brandon Barker]

I feel like this could make for an interesting publication, though I'll admit, maybe it has been done; I haven't really looked. There are probably a few type systems out there where this sort of thing is possible nowadays with optional type checking being seemingly more popular. I think a more difficult question to answer from an empirical standpoint is: how much does functional programming improve safety and catch errors?

--
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.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/97b1c18a-ae9b-4f17-9322-2122edd1a004o%40googlegroups.com.

--

Brandon Barker
brandon...@gmail.com

[Hongwei Xi]

This is just my personal experience. It is difficult for me to

quantify it. My perspective is from my work on implementing

typed and untyped languages. I will say more elsewhere about

some lessons I learned.

My very point here is that we don't get to see a lot of bugs simply

because our bug detection method is not effective enough to flush

them out for us to see. In other words, there are a lot of bugs lurking

around, waiting to get triggered with some specific input or environment.

There are some interesting similarities between viruses like

COVID-19 and bugs in code. An infectious virus is often much

easier to spread if it is less lethal. This is a bit like bugs causing

memory leaks. As such bugs don't cause immediate crashes, we

can reasonably assume that they must be abundant out there.

>>with optional type checking being seemingly more popular

Gradual typing is a trendy topic nowadays. For instance, Racket is

well-known for its support of gradual typing.

It is not like that we need every program to be memory leak-free. The

real question is how to make sure that you can do it if you want a particular

program to be memory leak-free. I don't see how this can be done with

the kind of gradual typing in Racket.

>>how much does functional programming improve safety and catch errors?

This question is too big :)

In terms of resource handling, functional vs. imperative is a bit like socialism

vs. capitalism :)

Functional programs don't have memory leaks because they don't own memories

in the first place. You can say functional programming improves memory safety in

this regard. And I can claim that I have never lost a single boxing match in my life.

Well, I have participated in none.

--Hongwei

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAORbNRpXJBFObChSYRepeXP4VQtn94T-oyFBp_WNzR7FjgbXCg%40mail.gmail.com.