A chemist, physicist and a computer scientist were asked to prove a thesis that every odd number is a prime. A chemist started checking the numbers — 3 prime, 5 prime, 7, still prime number. We can conclude we have proven the thesis. Next was physicist — 3 prime, 5 too, 7 too, 9, oh, wait, not a prime number, but let’s continue, 11 prime, and 13 is prime as well. OK, thesis is proven, we had just an experimental error with 9. The last one was computer scientist who decided to be smart and write a program to prove the thesis. Once he did the program displayed the output: 3 is a prime number, 3 is a prime number, 3 is a prime number, 3 is a prime number…
There is already written a lot about static and dynamic type-checking and why one is better than the other. So I’ll start from different angle — why Skila has static type-checking and actually more than that. Two things about me:
- I am a lazy guy, that is why I use computer to make computer do all the mundane work — it would be insane for me that computer would sip a cold drink and I would do all hard work,
- I am demanding guy — I don’t want my computer to do any job (like formatting hard drive or sending spam), but to do things I need and moreover to do them correctly.
No wonder, I write programs. And let’s think for a second how I could write them, say a function. Like this:
def something(x)
or like this:
IEnumerable<T> something(IEnumerable<T> x)
First version does not tell me the things the second version does — that parameter is a collection, and the type of elements in result is exactly the same as in parameter. Let’s fix it:
# this function takes a collection
# type of elements in result is exactly
# the same as in parameter
def something(x)
Since I started this post from mentioning the work, let’s compare just for fun the amount of keystrokes:
# this function takes a colle
ction # type of elements in
result is exactly # the same
as in parameter
IEnumerable<T>IEnumerable<T>
3.5 vs. 1. But the story does not end here. This was just a comment! You know how important a comment is for a computer, right? We have to write unit test. Since I am a lazy person I skip this step here, but you should have the picture already:
- dynamic type-checking and forcing every user to write excessive comments and units tests every time,
- static type-checking with a guarantee on types, allowing users to test the logic of the program, not the language.
The last part is kind of important — covering basic features, like agreement of types in unit tests does not give user any guarantee, see the joke — those guys were not proving anything, all they did was unit testing. It also means that in order to have some “degree of guarantee” you have to write those tests every freaking time you write a new function.
As far I am concerned I prefer to write this “test” just once in my lifetime — it is called static type checking.
But being correct is more than types — I will throw into Skila whatever I can that removes the necessity of writing unit test. Because writing once is better than many times, and knowing is better than believing. Example?
/// this function takes 3 to 5 strings
void something(params string[] text)
{
if (text.Length<3 || text.Length>5)
throw new ArgumentException("pass 3 to 5 strings");
}
Not bad, but! You will know about problem during runtime. Also if you change your mind you would have to change comment and the code (no single point of control).
Skila way (not implement yet):
def something(params[3..5] text String)
If the user passes the arguments in expanded form — something("hello", "world", "!") — the check will be done in compile time, if as an array it will be done in compile time, but the point is — peace of mind. Prove (once) everything that can be proven, and leave the tests for the rest.
Skila 