On Tue, Jun 07, 2011 at 12:08:26PM +0200, Thomas de Grivel wrote:
> Before even thinking of "fixing it" i'm trying to see if i'm alone in my
> quest. I like code correctness and feel what's done in OpenBSD is epic given
> the shitty language all the devs are dealing with. I love this much epic.
I don't consider C to be a shitty language... It's very suitable for
writing code that does what I expect from it and to maintain that code.
That's what I want from a language.
> Now if you want to know what code I'm writing, first I'm writing english
> because as you can see when a bring s-exp i'm answered "asm" and
> "brainfuck". Seriously did you even google the thing ?
What wikipedia turns up is lisp. It reads awful.
The purpose of a programming language is to enable reading and writing
of code. It's hard enough to understand what code does without having to
build a full parser in my brain.
I can see how S-expressions are nice to use in a proof. However it's
useless to me, since I'm trying to get work done. If I need to proof
something, it's the code I wrote. If I require a big conversion from
written code to something completely different, I am likely to introduce
mistakes thereby invalidating any proofs.
Likewise, when I want to deduct an algorithm, I prefer to write it in a
langauge as close to the implementation language as possible. Again to
minimize errors in the conversion between proof and real code.
If you wish to proof code, either do it directly or use a language that
closely resembles the imlementation language.
> And i never criticized the semantics of the code. Just that it's a 1 month
> project to build a fudgy C lexer, when parsing s-exp is more powerful and
> takes 2 days while watching pr0n, and 2 hours without.
And this is where the beauty of programming really shines: that C parser
has been written a long time ago and works. We don't reimplement a new C
parser every release. :)
> This is clearly off topic, and don't mean to rewrite an OS but there clearly
> is a need for cleaner programming languages in this world. I used to love C
> and i'm still quite proficient at it but when i had a glimpse of Lisp i
> realized how narrow was my vision of programming. And how much i trusted the
> languages i used to mean something.
Language is a vehicle to translate the ideas in my head to something the
computer understands. For kernel and userland programming, C is not just
adequate, it fulfills alot of our needs.
Especially for kernel work, we want to be able to predict memory and
runtime characteristics. Since C is very close to the underlying
assembler, those characteristics are easily deducted.
I have a question for you. You like S-expressions, because they
are easy to proof. But how often have you actually proven the code you
wrote?
In the real world, code is rarely proven. It's a lot of work, therefore
expensive. And the proof depends on underlying functions (libraries,
like the C library and systems calls, for instance) to be correct, your
assumptions about how they function to be correct and to not change
in a way as to invalidate your earlier assumptions.
What we try instead is to provide an environment where a bug will be
triggered early, often and resulting in a crash. This is important to
fix bugs: bugs only get hunted down and fixed when a failure hints at
them. When we talk about providing a hostile environment to code, this
is what we mean: making the environment as hostile as possible to bugs.
In this thread, I see complaints that C is hard to parse and prove, but
that's bollocks. C is a list of statements, which can be converted to
whatever that proof checker needs. The problem with proof checkers, is
that they need assistence. And you can't give that assistence without
doing the steps that the program is designed to do for you.
Example: the uvm_map_entry_link macro from sys/uvm/uvm_map.c before vmmap:
(map)->nentries++;
(entry)->prev = (after_where);
(entry)->next = (after_where)->next;
(entry)->prev->next = (entry);
(entry)->next->prev = (entry);
This is C, but it's easy to transform to GCL, if you want something that
has proof rules defined.
map->nentries := map->nentries + 1;
entry->prev := after_where;
entry->next := after_where->next;
entry->prev->next := entry;
entry->next->prev := entry;
But if you want to prove this is correct, you first need to define the
pre condition
{ map->nentries = (#x : x in map->entries) and
(all x : x in map->entries :
(x->next != NULL -> x->next->prev = x) and
(x->prev != NULL -> x->prev->next = x)) and
entry not in map->entries
}
and the post condition
{ map->nentries = (#x : x in map->entries) and
(all x : x in map->entries :
(x->next != NULL -> x->next->prev = x) and
(x->prev != NULL -> x->prev->next = x)) and
entry in map->entries
}
You can't deduct the pre and post condition, because they are what is to
be proven.
Now you need to apply each statement, updating the condition and verify
that pre condition + all mutations reaches the post condition.
This is a very trivial piece of code and it's easy to spot that this is
a manually implemented doubly linked list. But only writing down the
pre and post condition costs me more space than the snippet itself.
Not to mention that the time spent thinking them up cost me more time
than writing the original code.
Note that the proof checker cannot use this, since it has no idea how to
traverse the map->entries collection (which does not exist, since it
depends on map->header being the first and last element in that
collection instead).
--
Ariane
