Re: OT: Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
It was well said that when we learn lisp we all start thinking things like that. ;) As to what theo said about interfaces, of course it is correct, but on the other hand (as a design tool) doesn't Hal Abelman on the SICP lectures say, that it is a powerfull techinique to be able to create interfaces that you forget everything about them afterwards? He goes on to demonstrate... In my mind the thing boils down to this: in the PC as it is structured (HW-wise) you can't impose functional programming (at least in an elegant/meaningfull way). But if you consider as specially built arch for executing LISP code as the Connection Machine (from thinking machines) then it could get interesting ;) and yes sorry for talking and not working on clisp :( DsP On Thu, Jun 9, 2011 at 6:38 AM, Super Biscuit super_bisq...@yahoo.com wrote: I know neither C(++), or LISP, or PERL, or python or any other language. I've worked on VirtualBox porting to FreeBSD. I am working on GNOME3 on FreeBSD for ppc and sparc64 in my spare time. No lisp, no c, no other language . This is just from being able to read and understand code. I know how far emacspeak can be compiled on OpenBSD PPC and what is needed. Many people can do what I do; but, I don't consider them a waste of mind as you do. Your head is so far up your ass that you have a ring of shit for a necklace. --- On Wed, 6/8/11, Thomas de Grivel billi...@gmail.com wrote: From: Thomas de Grivel billi...@gmail.com Subject: Re: OT: Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems. To: misc@openbsd.org misc@openbsd.org Date: Wednesday, June 8, 2011, 10:23 AM [Other shit removed to concentrate on the ignorance of the last line.] Any hacker not knowing a couple of Lisp macros is a waste of mind. -- Thomas de Grivel I must plunge into the water of doubt again and again.
Re: OT: Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
I believe SICP has much culture but not always so great style. I'm not learning lisp. Who are you to know of all lisp learners ? Why are you associating lisp with functional programming ? CL in itself is not really functional, but being a metalanguage you can make it so. You could also make it sort perforated cards. Is it a perforated cards programming language ? Lisp is not important, the way we can program it is important, and it just comes from its syntax. Lisp machines are long dead, there are excellent compilers available for more current archs. Looks to me like you are still learning lisp. -- Thomas de Grivel http://b.lowh.net/billitch/
Re: OT: Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
On Fri, 10 Jun 2011 03:58:40 +0200, Thomas de Grivel wrote: I believe SICP has much culture but not always so great style. I'm not learning lisp. Who are you to know of all lisp learners ? Why are you associating lisp with functional programming ? CL in itself is not really functional, but being a metalanguage you can make it so. You could also make it sort perforated cards. Is it a perforated cards programming language ? Lisp is not important, the way we can program it is important, and it just comes from its syntax. Lisp machines are long dead, there are excellent compilers available for more current archs. Looks to me like you are still learning lisp. -- Thomas de Grivel http://b.lowh.net/billitch/ Get rid of your Lisp - it can be done. See the movie now! The King's Speech The King's Speech won the Academy Award for Best Picture, Best Director (Hooper), Best Actor (Firth), and Best Original Screenplay (Seidler). Also won seven British Academy Awards. Then you can stop trolling around here where you are about as welcome as a fart in a crowded elevator stuck between floors. *** NOTE *** Please DO NOT CC me. I am subscribed to the list. Mail to the sender address that does not originate at the list server is tarpitted. The reply-to: address is provided for those who feel compelled to reply off list. Thankyou. Rod/ --- This life is not the real thing. It is not even in Beta. If it was, then OpenBSD would already have a man page for it.
Re: OT: Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
+1 --- On Wed, 6/8/11, Theo de Raadt dera...@cvs.openbsd.org wrote: From: Theo de Raadt dera...@cvs.openbsd.org Subject: Re: OT: Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems. To: Nicholas Marriott nicholas.marri...@gmail.com Cc: Thomas de Grivel billi...@gmail.com, Christiano F. Haesbaert haesba...@haesbaert.org, misc@openbsd.org misc@openbsd.org Date: Wednesday, June 8, 2011, 3:10 AM You are either trolling or just very mixed up, the important thing is not how quickly machines can parse it or how quickly you can write a lexer but how quickly humans can parse it and what they can do with it. C is not the best here but it is way ahead of any kind of useless functional language. Indeed. People write in languages they can understand, just like we are emailing in a language we can all understand. English sucks, yet we all use it. Why are you not trying to miscommunicate with us in dutch, Mr. de Grivel? Because it would fail (though you probably speak the perfect langauge of gmail). You fail anyways since you come off as a salesman of a perfection mythos. When we start writing something in C or any other language, we are writing a chunks of interface code and chunks of data management code. We layer the code using interfaces we decide on very early so that it is easier to determine where the bugs are, at least early on. However almost every time the interface decisions made early on carry on far into the future and eventually screw us. We fix all the data management bugs, and then the interface layers end up being flawed. Subtly, but flawed. They are our next problem. Then when we try to fix them, we introduce new subtle problems. However here is where you are entirely wrong: C is not different. All the languages are like that. That is because we write in the way that we think, and the way we think is biased towards the way we remember. Why the way we remember? That is so that when we see the code again, we can remember what we were thinking. When we make changes in any of them to fix a structural problem, we start to forget layers of our previous thoughts. It becomes less recognizeable. No language or programming system designed to this day is flexible enough so that we can remember the steps of our thought process, and yet also be flexible enough that it allows us to change the interfaces (without us not remembering it next time; the process is highly iterative). And then some details make it even gets worse. We are trying to develop userland programs, and libraries, and the portable include infrastructable managing the variation chaos between 32 bit and 64 bit and signed char vs unsigned char and whatnot layers of variaion; and we are trying to writing boot code, and we are writing kernels to run all this. Add in the bullshit we support it the ports subsystem, and it is no wonder our brains are struggling. When someone tells anyone that there is an answer and some cohesive language will solve this is problem... they are flat out deluded and that delusion comes out of blind stupidity. You obviously have zero experience. The only thing you have experience in is trolling mailing lists acting as if you are some expert. The real experts are the people struggling with these systems, not the pulpit heros.
Re: OT: Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
I'm not really selling anything. I'm seeing a deeply rooted bug in our way of thinking programming languages. Struggling is not necessary unless you want to punish yourself. My experience, and I feel I have enough in C to speak untroubled, is that not all languages are like C when it comes to laying out your thoughts. I used to think so, all my mind was trapped in this. The language is very well defined, but cannot understand itself. Cannot be worked itself like we work other data, except with a gigantic piece of software. If the code does not reflect the layers of thoughts, of course it cannot scale, or very slowly. You need good abstractions to solve complex problems. And good data structure, C has that better than any other language. In CL I can speak my mind in terms of layers and these layers fit nice, or are easy to fix because there is no duplicate code. This also means very short code. This is not because of the semantics of the language, C is much better defined at precise memory handling, but precisely because part of the art of programming in s-exp is partly in generating the uninteresting part of the code, or reading it with a function, checking for some bug patterns. I could try to explain it another way : we are compilers. We have ideas we need to translate into C, knowing that in turn C will be compiled into some behaviour of the system. That pipeline is broken when your layers do not fit well into the language. To fix this we'd need macros to generate code, but C macros generate not code but text ! How's that in any way useful ? Other hint debunks : - CL is much much older than C. Again not talking about the semantics, but at the time it was out, C compiler technology was really not state of the art. Though it had much more focused semantics, which made it win most system code. - CL is not functional, it is procedural like C and can generate native code. - You can encode any language in s-exp. Actually this is done at AST level though we cannot access it with these bulky C compilers. The good features of lisp are just from symbolic expressions. What Theo said remains true to all programming. How the language is processed is what I'm talking about. Any hacker not knowing a couple of Lisp macros is a waste of mind. -- Thomas de Grivel I must plunge into the water of doubt again and again.
Re: OT: Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
Like I said before, there is amply enough work in the ports tree for lisp hackers. Go work on porting clisp to other OpenBSD architectures. Give us something concrete. Talk is very, very cheap.
Re: OT: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
Here's a helpful start: http://www.unlambda.com/lisp/mit.page Enjoy!
Re: OT: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
This really has nothing to do on this list, but here I go...
@ Ariane van der Steldt ari...@stack.nl wrote (2011-06-08 14:00+0200):
I did say that. I said code proof (assisted or manual) is a lot of work.
Yes, we should start over. If we start over we can make it so much
better! We can do this and that and... spend ten times as much time to
reach where we are now.
We're doing that already. And we're much better in it than you.
I don't know what fighting on the same plane means. Can you please
explain?
Bingo.
Huh, point? Where?
Well this monday i really planned to darken down your (all of you)
day, with this:
#include fcntl.h
#include stdio.h
#include stdlib.h
#include unistd.h
#include sys/mman.h
int
main(void)
{
#define ERROR(T,MSG)if (T) { perror(MSG); exit(1); }
void *mp;
ssize_t wb;
off_t off;
char sb[8];
int fd = open(test.dat, O_RDWR | O_CREAT | O_EXCL, 0600);
ERROR(fd 0, open);
off = lseek(fd, (off_t)0xfffdUL, SEEK_SET);
ERROR(off 0, lseek);
wb = write(fd, abcd, 4);
ERROR(wb != 4, write);
/*ERROR(fcntl(fd, F_FULLFSYNC), fcntl(F_FULLFSYNC)); fsync() insuff.
*/
mp = mmap(NULL, 0x10001ULL, PROT_READ, MAP_PRIVATE, fd, 0);
ERROR(mp == NULL, mmap);
sb[0] = *((char*)mp + 0xfffdUL + 0) - '0'; write(1, sb, 1);
sb[0] = *((char*)mp + 0xfffdUL + 1) - '0'; write(1, sb, 1);
sb[0] = *((char*)mp + 0xfffdUL + 2) - '0'; write(1, sb, 1);
sb[0] = *((char*)mp + 0xfffdUL + 3) - '0'; write(1, sb, 1);
write(1, \n, 1);
ERROR(munmap(mp, 0x10001ULL), munmap);
ERROR(close(fd), close);
return 0;
}
running on OS X (it was due to the vmmap thread), and the
expected behaviour should have been
ab
SIGBUS
and then i wanted to talk about that i don't believe that Open
Source software will last over time because you have to walk
yourself instead of being driven in a nice shuttle bus etc. etc.
Even free heroin shipped by SuperBiscuit can't beat that, unless
- maybe - on a perfect day...
(I did not know about the super cheap hotel mail at that time.)
But guess what? Apple fixed the mmap bug on sparse files!
No nore
3. For at least sparse files the VMS of Mac OS X is unable to
create an accessible mmap(2)ing if the size of the mapping is
in the inclusive range
UINT32_MAX+1 .. UINT32_MAX + PAGESIZE (== 4096)
and the file has been written to.
(but maybe still
killed all tests which spent more than about three minutes first,
later i did so whenever 900M was not reached in top(1) output -
it seems to me that Apple's VM is not intelligent enough to
detect that it effectively has entered an endless loop!!!)
I was so disappointed! I maybe roared like a non-useless lion
would. No useful contribution by me in 2011.
--
Ciao, Steffen
sdaoden(*)(gmail.com)
() ascii ribbon campaign - against html e-mail
/\ www.asciiribbon.org - against proprietary attachments
Re: OT: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
On Wed, Jun 08, 2011 at 02:00:03PM +0200, Ariane van der Steldt wrote: On Wed, Jun 08, 2011 at 02:24:14AM +0200, Thomas de Grivel wrote: Just like C, OCaml has skills in its semantics, but they both suck at grammar : parsing ml requires a full lex/yacc above and below gcc. Not really checked code but if the bug hasnt shown it must not exist. Or in the next release. Ah, OCaml is cool because you have not seen a bug in a compiler... There are lots of good points and bad points in Ocaml. One thing you won't find is a bug in its Garbage-Collector (that was Damien Doligez's thesis, and he had to fix all the bugs in it to finish the proof that it was bug-free). As far as I know, similar work has not been done in the remaining parts of OCaml. So there are definitely bugs in it. Just because no-one hasn't found them doesn't mean they don't exist (and there are few system hackers as brilliant as Damien). There are less cool parts of ocaml development, like feuds between various sets of developers, but I won't go there, it's just the nitty gritty of a real life language, thus very much imperfect. Of course, ocaml type system sucks. But so do all type systems, since type-inference is a semi-decidable problem, and all smart languages out there are making-do by using a suitable approximation of the best matching type for a given construct... Well, if de Grivel likes ocaml so much, why doesn't he improve our port ? like figure out why it doesn't run on hppa (at a wild guess, ocaml assumes things about stack orientation...), or to polish the compiler so that it actually compiles on, say, arm, for instance...
Re: OT: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
Le 06/08/11 14:00, Ariane van der Steldt a icrit : On Wed, Jun 08, 2011 at 02:24:14AM +0200, Thomas de Grivel wrote: This really has nothing to do on this list, but here I go... Pfft, this mail sucks. If you had actually responded properly, instead of reiterating your arguments, I would have enjoyed it. You're just baiting. Oh well, I'll take the bait. I'll just pretend you actually replied to my e-mail (and for the love of clean, threaded mailinglists, please make proper use of mail threading; no fun to have to look all over the place to find your mail). Sorry for that. Frankly you were much more interesting about vmmap and avl trees. I did not mean to disturb you. I'll answer anyway because you flame me just for the sake of flaming. Languages are like gods : there can be only one, and its perfect, and everywhere, and we show our faith. Sure.. who wants to believe that crap ? Well... you do. Obviously no. You completely misconceived my intentions. That was a gross caricature, but also what I felt of previous comments by programmers. Languages have flaws, they are (slightly) bugged to the core and we're so much into their usage^Wabuse that we dont see walls anymore. Hey my windows works fine at home when installing every year !! This paragraph added nothing to the discussion. Yes, a lot of programmers are lost in trust to their language being the one true way to think programming. It was linked to the previous paragraph. You dismiss assisted code proof because proving code is not verified itself. I did say that. I said code proof (assisted or manual) is a lot of work. What if it could be ? Actually it has been done with a compiler of a subset of C and a few ML like languages. Compiled assembly code of compiler was proven correct by humans. Writing an assisted proof compiler for C is just as trivial as writing one for lisp. I'm not talking about assisted proof, but proving the compiler correct. This way, when you can prove the code by hand or assisted, then you can be sure the binary is correct. This was indeed a lot of work, like you said. The ML like languages, along with type theory, are now used to study math theorems by writing them in types and proving the theorem by writing a program of that type. IIRC this is Curry-Howard correspondence. Turing machines are used in proofs. I think we should ditch the current architectures and switch to really-long-tape! You think that because a language is suitable for one thing, it is suitable for everything. A common fallacy. I am precisely advocating the discovery of other languages, not one true language. When you start looking around you see the flaws in each of them. Most often it is syntax, since if the language is useful the semantics are quite right. I'm wondering, what other languages do you know along with C ? In languages like ocaml every expression has a static type, possibly removing all need for runtime type info. I also think the ocaml grammar and static typing sucks, but programs that compile *always* work and are fast. C has static typing! int a; really describes an int, not a float... Programs don't *always* work. Malloc may return NULL, mmap may fail, for many reasons. And that's just memory. I don't think you understand what it takes to run a program. Anyway, C programs work for the same value of *always* and the same value of fast. Why are you talking about C here ? It was about ocaml. You don't seem to know how it works and its type system. In 1996, a researcher named J.L Krivine took the theorem of the completeness of classical logic (we all use in science, math, programming), expressed it in type theory, and actually proved it by writing a step by step userland disassembler. Pure wtf, but true. Mind blower to me. Good for him. What has that to do with C or lisp or other programming languages? You'll have to dig up youself. That writing a disassembler is equivalent to proving a fundamental theorem of mathematics is awesome enough to me. Just like C, OCaml has skills in its semantics, but they both suck at grammar : parsing ml requires a full lex/yacc above and below gcc. Not really checked code but if the bug hasnt shown it must not exist. Or in the next release. Ah, OCaml is cool because you have not seen a bug in a compiler... Parsing lisp, i can explain to a 2 year old. Bold statement. You know 2 year olds aren't known for their ability at abstract thinking? Yeah I've always thought too much wonders about kids. Maybe 5 years old. Do it in *any* language. In less than 1kb. On the syntax, Lisp is the red pill. Bla bla bla, no arguments supplied. Arguments ? Do I need to explain a 50 years old widely taught academic root of computing here to be heard ? If you care why don't you try it ? I bet that with your skills (i read very interesting things from you on tech@) writing a s-exp parser would be a less than 2 hours task. If C was so easy to parse,
Re: OT: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
Just wanna say Thanks to Thomas and his big, dumb, yet fun show. But now I think we're all bored.
Re: OT: Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
I know neither C(++), or LISP, or PERL, or python or any other language. I've worked on VirtualBox porting to FreeBSD. I am working on GNOME3 on FreeBSD for ppc and sparc64 in my spare time. No lisp, no c, no other language . This is just from being able to read and understand code. I know how far emacspeak can be compiled on OpenBSD PPC and what is needed. Many people can do what I do; but, I don't consider them a waste of mind as you do. Your head is so far up your ass that you have a ring of shit for a necklace. --- On Wed, 6/8/11, Thomas de Grivel billi...@gmail.com wrote: From: Thomas de Grivel billi...@gmail.com Subject: Re: OT: Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems. To: misc@openbsd.org misc@openbsd.org Date: Wednesday, June 8, 2011, 10:23 AM [Other shit removed to concentrate on the ignorance of the last line.] Any hacker not knowing a couple of Lisp macros is a waste of mind. -- Thomas de Grivel I must plunge into the water of doubt again and again.
OT: Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
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. 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 ? 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. 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.
Re: OT: Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
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
Re: OT: Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
On 7 June 2011 07:08, Thomas de Grivel billi...@gmail.com 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. Please, C is very far from shitty, C is wonderful, although not perfect and not easily-parseable. 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 ? Check your facts again, and see who said what, I'm quite fond of scheme. 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. 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. You're just passing though a *phase*, that's ok, it happens to all of us when we learn lisp. I'd advice getting back to reality now. Now, think again, parsing a language is nice, but it's almost never the most important thing. You also should not try to convert old school unix hackers into lispers, there may be rape.
Re: OT: Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
On Tue, Jun 07, 2011 at 11:19:11AM -0300, Christiano F. Haesbaert wrote: [...] Now, think again, parsing a language is nice, but it's almost never the most important thing. You also should not try to convert old school unix hackers into lispers, there may be rape. s/may be/will be/ -- Gilles Chehade http://www.poolp.org
Re: OT: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
This really has nothing to do on this list, but here I go... Languages are like gods : there can be only one, and its perfect, and everywhere, and we show our faith. Sure.. who wants to believe that crap ? Languages have flaws, they are (slightly) bugged to the core and we're so much into their usage^Wabuse that we dont see walls anymore. Hey my windows works fine at home when installing every year !! You dismiss assisted code proof because proving code is not verified itself. What if it could be ? Actually it has been done with a compiler of a subset of C and a few ML like languages. Compiled assembly code of compiler was proven correct by humans. The ML like languages, along with type theory, are now used to study math theorems by writing them in types and proving the theorem by writing a program of that type. IIRC this is Curry-Howard correspondence. In languages like ocaml every expression has a static type, possibly removing all need for runtime type info. I also think the ocaml grammar and static typing sucks, but programs that compile *always* work and are fast. In 1996, a researcher named J.L Krivine took the theorem of the completeness of classical logic (we all use in science, math, programming), expressed it in type theory, and actually proved it by writing a step by step userland disassembler. Pure wtf, but true. Mind blower to me. Just like C, OCaml has skills in its semantics, but they both suck at grammar : parsing ml requires a full lex/yacc above and below gcc. Not really checked code but if the bug hasnt shown it must not exist. Or in the next release. Parsing lisp, i can explain to a 2 year old. Do it in *any* language. In less than 1kb. On the syntax, Lisp is the red pill. Languages like C let the humans do all the deducive work, though this is something machines do better. Are you reviewing the bits on your disk by hand after hard reboot ? No you write a program for that. Do you have to check every piece of assembled functionality in your OS by hand ? Yes because the code cannot understand the code. Checking for errors is good, machines are better than humans at repetitive tasks. I'm not saying it has to be automatized, just we could have had more powerful tools at hand if C was not an outdated tech the day it was made.. I'm not fixing this but we have to wake up. And fix the problems at their root. Not so OT actually ? That some system programmers still ignore much of the details of what was achieved in programming languages is no surprise, our community is broken by our beliefs that they are fighting on the same plane. To express all programs. Language esthetes fail to like C semantics, all lost in high-levelness or using C when too close to the metal. C programmers often not aware that non-fortran-like languages actually do wonders. Once again, I can only praise the C semantics for what is achieved by hand in this project. But i cannot shut up about its grammar. It is the worst wormed gift ever made to the programming world. Along with INTERCAL. Actually it was not really a gift, more of a prank. I'm not advising anyone let off C and those waiting for me to tell them some truth about programming languages are fucking zombies. But you cannot blind yourself into C like the world wants you to. There are way more beautiful things to see in this world, dont you know ? Grammar is the tool at the base of your trust : you assume you can express what your twisted and experienced mind wants to see in forming a sequence of tokens. In the grammar of C you assemble characters to form a tree of tokens. You cannot see them, just trust they are actually there. Or not : optimizations, defines, bad macros, missing ;, broken lexer, broken compiler,.. hairy errors. In symbolic computing to can actually avoid all duplication of code, review or even step-step through compilation, define new compilation macros, extending compiler e.g checking for some type of errors without duplicating code - true macros. - avoid needing so much complexity just for parsing/compiling = more trust, less to check by hand This is not because of the language itself, which is actually not better defined than C, but because of its parsability. Code is actually not text : it is a tree of tokens. I think I made my point, maybe now I'll try to shut up. And Christiano, you know, technically its only a rape if i do not consent. And `sed` threats dont really work on me. All in all, i trust all the distrust in OpenBSD to build an awesome product. I thought I'd share some distrust regarding some of our most important tools. Maybe not paranoia. Be safe =)
Re: OT: Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
You are either trolling or just very mixed up, the important thing is not how quickly machines can parse it or how quickly you can write a lexer but how quickly humans can parse it and what they can do with it. C is not the best here but it is way ahead of any kind of useless functional language. 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. 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 ? 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. 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.
Re: OT: Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
On Jun 7, 2011, at 19:46, Nicholas Marriott nicholas.marri...@gmail.com wrote: You are either trolling or just very mixed up, the important thing is not how quickly machines can parse it or how quickly you can write a lexer but how quickly humans can parse it and what they can do with it. C is not the best here but it is way ahead of any kind of useless functional language. C is superior; get used to it. All languages invented after pretty much suck. CS has been done a long time ago. Most new shit is just that, new shit. Shiny and mostly worthless. What the fuck ever about $language-du-jour. 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. 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 ? 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. 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.
Re: OT: Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
You are either trolling or just very mixed up, the important thing is not how quickly machines can parse it or how quickly you can write a lexer but how quickly humans can parse it and what they can do with it. C is not the best here but it is way ahead of any kind of useless functional language. Indeed. People write in languages they can understand, just like we are emailing in a language we can all understand. English sucks, yet we all use it. Why are you not trying to miscommunicate with us in dutch, Mr. de Grivel? Because it would fail (though you probably speak the perfect langauge of gmail). You fail anyways since you come off as a salesman of a perfection mythos. When we start writing something in C or any other language, we are writing a chunks of interface code and chunks of data management code. We layer the code using interfaces we decide on very early so that it is easier to determine where the bugs are, at least early on. However almost every time the interface decisions made early on carry on far into the future and eventually screw us. We fix all the data management bugs, and then the interface layers end up being flawed. Subtly, but flawed. They are our next problem. Then when we try to fix them, we introduce new subtle problems. However here is where you are entirely wrong: C is not different. All the languages are like that. That is because we write in the way that we think, and the way we think is biased towards the way we remember. Why the way we remember? That is so that when we see the code again, we can remember what we were thinking. When we make changes in any of them to fix a structural problem, we start to forget layers of our previous thoughts. It becomes less recognizeable. No language or programming system designed to this day is flexible enough so that we can remember the steps of our thought process, and yet also be flexible enough that it allows us to change the interfaces (without us not remembering it next time; the process is highly iterative). And then some details make it even gets worse. We are trying to develop userland programs, and libraries, and the portable include infrastructable managing the variation chaos between 32 bit and 64 bit and signed char vs unsigned char and whatnot layers of variaion; and we are trying to writing boot code, and we are writing kernels to run all this. Add in the bullshit we support it the ports subsystem, and it is no wonder our brains are struggling. When someone tells anyone that there is an answer and some cohesive language will solve this is problem... they are flat out deluded and that delusion comes out of blind stupidity. You obviously have zero experience. The only thing you have experience in is trolling mailing lists acting as if you are some expert. The real experts are the people struggling with these systems, not the pulpit heros.
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
I don't want to engage in language wars, as i wrote before there is a gap in programming culture and reinforcing trust in my favorite lang or OS won't help. We trust our languages to mean something but writing correct programs strangely is still a struggle even to skilled programmers, and takes much testing. Again, i don't mean to hurt but C is really not KISS, at all. Its paradigm is appropriate for system but its grammar is a huge mess. And we're all happy to struggle with it ? Is it out of pride ? There is no easy fix but i recognize this is the core source of many ugly bugs. They're just symptoms of this. And noone cares at all.
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
The answer is too write all OS code in Machine language for each Architecture! YEA! We're waiting for your code! I'm super duper excited! :-0 On Mon, 06 Jun 2011 11:10 +0200, Thomas de Grivel billi...@gmail.com wrote: I don't want to engage in language wars, as i wrote before there is a gap in programming culture and reinforcing trust in my favorite lang or OS won't help. We trust our languages to mean something but writing correct programs strangely is still a struggle even to skilled programmers, and takes much testing. Again, i don't mean to hurt but C is really not KISS, at all. Its paradigm is appropriate for system but its grammar is a huge mess. And we're all happy to struggle with it ? Is it out of pride ? There is no easy fix but i recognize this is the core source of many ugly bugs. They're just symptoms of this. And noone cares at all.
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
On 06/06/11 11:36, Eric Furman wrote: I'm super duper excited! :-0 do you need a towel ? -- Thomas de Grivel http://b.lowh.net/billitch I must plunge into the water of doubt again and again.
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
I'm super duper excited! :-0 do you need a towel ? do you need a keyboard or two? Now that you have decided to write your own OS from scratch in s-expressions like language? bwaaahh
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
On 6 June 2011 06:10, Thomas de Grivel billi...@gmail.com wrote: I don't want to engage in language wars, as i wrote before there is a gap in programming culture and reinforcing trust in my favorite lang or OS won't help. We trust our languages to mean something but writing correct programs strangely is still a struggle even to skilled programmers, and takes much testing. Again, i don't mean to hurt but C is really not KISS, at all. Its paradigm is appropriate for system but its grammar is a huge mess. And we're all happy to struggle with it ? Is it out of pride ? There is no easy fix but i recognize this is the core source of many ugly bugs. They're just symptoms of this. And noone cares at all. Oh great, you pointed out something that *could* be better. Yeah, C has its problems, so how are *YOU* going to start fixing it ? Now, again, I lost the part where you say what you are doing to make it better. You made no questions and no statements that could result in any productive work what-so-ever. Honestly, what are you trying to achieve ?
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
On Mon, Jun 06, 2011 at 05:36:03AM -0400, Eric Furman wrote: The answer is too write all OS code in Machine language for each Architecture! YEA! We're waiting for your code! I'm super duper excited! :-0 Perhaps he should go work on this project: BareMetal OS BareMetal is a 64-bit OS for x86-64 based computers. The OS is written entirely in Assembly, whil e applications can be written in Assembly or C/C++. Clearly someone is trying to get rid of ugly languages!
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
brainfuck OS sould be a good idea too... :D of course this is a joke, forth language should be more usefull From: Chris Bennett ch...@bennettconstruction.biz Sent: Mon Jun 06 18:49:16 CEST 2011 To: misc@openbsd.org Subject: Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems. On Mon, Jun 06, 2011 at 05:36:03AM -0400, Eric Furman wrote: The answer is too write all OS code in Machine language for each Architecture! YEA! We're waiting for your code! I'm super duper excited! :-0 Perhaps he should go work on this project: BareMetal OS BareMetal is a 64-bit OS for x86-64 based computers. The OS is written entirely in Assembly, whil e applications can be written in Assembly or C/C++. Clearly someone is trying to get rid of ugly languages! Cordialement Francois Pussault 3701 - 8 rue Marcel Pagnol 31100 ToulouseB FranceB +33 6 17 230 820 B +33 5 34 365 269 fpussa...@contactoffice.fr
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
On Mon, 6 Jun 2011 11:49:16 -0500 Chris Bennett wrote: BareMetal is a 64-bit OS for x86-64 based computers. The OS is written entirely in Assembly, I believe some/all newer models? of the Sonicwall range were rewritten in assembly, to increase performance. My cousin loves em.
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
On Mon, Jun 06, 2011 at 11:49:16AM -0500, Chris Bennett wrote: On Mon, Jun 06, 2011 at 05:36:03AM -0400, Eric Furman wrote: The answer is too write all OS code in Machine language for each Architecture! YEA! We're waiting for your code! I'm super duper excited! :-0 Perhaps he should go work on this project: BareMetal OS BareMetal is a 64-bit OS for x86-64 based computers. The OS is written entirely in Assembly, whil e applications can be written in Assembly or C/C++. Clearly someone is trying to get rid of ugly languages! http://www.menuetos.net/ ?
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
On Mon, Jun 06, 2011 at 10:31:29AM -0500, Amit Kulkarni wrote: do you need a keyboard or two? Now that you have decided to write your own OS from scratch in s-expressions like language? We should send this guy bullshit to the Linux kernel mailing-list so they can have some fun too. Hey. Those guys are doing open source, we can share the fun even if they're stuck stuffing penguins at home while we get red-leather chicks on our side... -- Threepwood
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
On Mon, Jun 06, 2011 at 01:33:31PM -0300, Christiano F. Haesbaert wrote: Honestly, what are you trying to achieve ? I bet 10 canadian dollars on his 15 minute fame, and eternal storage in Google newsgroup servers of YARGTKBTOD* (*) Yet Another Random Guy That Knows Better Than OpenBSD Developers -- Bill Gates
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
How about he proves to us he can write good lisp code first, by maintaining ecl and maxima and sbcl for a while ?
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
X86 machine language sucks big rocks. Everyone should write in microcode for full speed! Sent from my iPhone On Jun 6, 2011, at 12:49 PM, Chris Bennett ch...@bennettconstruction.biz wrote: On Mon, Jun 06, 2011 at 05:36:03AM -0400, Eric Furman wrote: The answer is too write all OS code in Machine language for each Architecture! YEA! We're waiting for your code! I'm super duper excited! :-0 Perhaps he should go work on this project: BareMetal OS BareMetal is a 64-bit OS for x86-64 based computers. The OS is written entirely in Assembly, whil e applications can be written in Assembly or C/C++. Clearly someone is trying to get rid of ugly languages!
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
I see your brainfuck and raise you APL Sent from my iPhone On Jun 6, 2011, at 1:11 PM, Francois Pussault fpussa...@contactoffice.fr wrote: brainfuck OS sould be a good idea too... :D of course this is a joke, forth language should be more usefull From: Chris Bennett ch...@bennettconstruction.biz Sent: Mon Jun 06 18:49:16 CEST 2011 To: misc@openbsd.org Subject: Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems. On Mon, Jun 06, 2011 at 05:36:03AM -0400, Eric Furman wrote: The answer is too write all OS code in Machine language for each Architecture! YEA! We're waiting for your code! I'm super duper excited! :-0 Perhaps he should go work on this project: BareMetal OS BareMetal is a 64-bit OS for x86-64 based computers. The OS is written entirely in Assembly, whil e applications can be written in Assembly or C/C++. Clearly someone is trying to get rid of ugly languages! Cordialement Francois Pussault 3701 - 8 rue Marcel Pagnol 31100 ToulouseB FranceB +33 6 17 230 820 B +33 5 34 365 269 fpussa...@contactoffice.fr
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
On Mon, Jun 06, 2011 at 08:17:11PM -0400, goodb...@gmail.com wrote: X86 machine language sucks big rocks. x86 is not executed on x86 processors since the Pentium 4. Intel (and AMD) are using RISC cores at the heart of their processors. x86 instructions are translated into RISC code and this code is the one that gets executed. The x86 CISC is just a shell around an RISC heart. -- Overflow
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
Actually you're right : the C paradigm is straightforward and perfect to handle system code. What I meant to criticize is its grammar : it sucks that we cannot parse C with a simple program. It's not KISS at all and we all pay the price when checking for errors and everytime we wish to process these weird formatted text files. On the other hand, languages based on s-expressions have this unique feature of being very easy to parse and can be processed as regular data, every aspect of the syntax being clean and regular. The problem is that these languages were historically used by pretentious folks on rare supercomputers and thus were not developed to fit the low level paradigm very well. This does not have to be. We should bridge this gap that was forced by ice age investors. Of course i really don't know how nor how it relates to OpenBSD, apart from this common goal of achieving correctness. -- Thomas de Grivel Lisp is the red pill
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
On Sun, Jun 05, 2011 at 03:10:42PM +0200, Thomas de Grivel wrote: [..] We should [..] Those two words are the exact spot where the problem really is. That we. OpenBSD is worked upon by developers. They do it, the hard work so people like me, users, can benefit from good code, solid software, trusty operating system. They do it : they write the code. Debug it. Maintain it. Fix it. So, if any change of tools is done, it will be done by them, and them alone. Not me, nor anyone else. Thus, there is no we. There is the developers on one side, and the users on the other. If developers do want the C langage to be replaced by something else, they will do it. Because they will get a benefit from it, and OpenBSD too. Until this happens, C will remain the langage used. If your idea can be, you will have to implement it. You (or someone that shares that same idea) will have to design a compiler that compiles a kernel and gives you a shell like OpenBSD does. It has to work as well as OpenBSD does, be able to do all the things it does, and show by the proof that the langage then used really makes working on it better. Make it work. Like scientists make experiments that are reproductible before saying to the other bald guys in white blouses : guys, it works. You can even try it and check the fact for yourselves, here's the recipe how to do it. We should not tell people that do the work how they should do it. Because they are the ones doing it, since years, and obviously, they're doing a pretty damn good job. If Theo ever hears you say we should in order to tell them how they should code _their_ operating system, I am afraid he will send his special monkey killing-squad and you will vanish from the face of this island. Beware of the monkeys. Especially those that not only eat the banana, but also its skin. -- Guybrush
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
Actually you're right : the C paradigm is straightforward and perfect to handle system code. there you go. as unfortunate as that is, it is still true. Sometimes, I am very surprised C is still around for so long, and essentially unchanged. But its limitations are well known. What I meant to criticize is its grammar : it sucks that we cannot parse C with a simple program. It's not KISS at all and we all pay the price when checking for errors and everytime we wish to process these weird formatted text files. On the other hand, languages based on s-expressions have this unique feature of being very easy to parse and can be processed as regular data, every aspect of the syntax being clean and regular. The problem is that these languages were historically used by pretentious folks on rare supercomputers and thus were not developed to fit the low level paradigm very well. Allegro just recently got SMT/SMP, all others are probably (no research, just throwing it out there) still stuck in single land. While the folks on the supercomputers today are running SMT/SMP in their zillions. That's the cool thing for them and your s-expressions won't help them today. This does not have to be. We should bridge this gap that was forced by ice age investors. Of course i really don't know how nor how it relates to OpenBSD, apart from this common goal of achieving correctness. Just yesterday, I tried chicken scheme and compiled it to C code. The C was unintelligible, why? Because it is setting up the JVM like environment. This goes back to the vmmap thread. Many people try to play OS designers, when very few of them are capable of it. Just leave the OS stuff to the OS people, they will get it right eventually.
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
I was actually referring to the people seeking correctness in software development. Feel free to say you are not interested. And threats about killer monkey squads do not apply here, get lost. On 5 juin 2011 20:38, gilbert.fernan...@orange.fr wrote: On Sun, Jun 05, 2011 at 03:10:42PM +0200, Thomas de Grivel wrote: [..] We should [..] Those two words are the exact spot where the problem really is. That we. OpenBSD is worked upon by developers. They do it, the hard work so people like me, users, can benefit from good code, solid software, trusty operating system. They do it : they write the code. Debug it. Maintain it. Fix it. So, if any change of tools is done, it will be done by them, and them alone. Not me, nor anyone else. Thus, there is no we. There is the developers on one side, and the users on the other. If developers do want the C langage to be replaced by something else, they will do it. Because they will get a benefit from it, and OpenBSD too. Until this happens, C will remain the langage used. If your idea can be, you will have to implement it. You (or someone that shares that same idea) will have to design a compiler that compiles a kernel and gives you a shell like OpenBSD does. It has to work as well as OpenBSD does, be able to do all the things it does, and show by the proof that the langage then used really makes working on it better. Make it work. Like scientists make experiments that are reproductible before saying to the other bald guys in white blouses : guys, it works. You can even try it and check the fact for yourselves, here's the recipe how to do it. We should not tell people that do the work how they should do it. Because they are the ones doing it, since years, and obviously, they're doing a pretty damn good job. If Theo ever hears you say we should in order to tell them how they should code _their_ operating system, I am afraid he will send his special monkey killing-squad and you will vanish from the face of this island. Beware of the monkeys. Especially those that not only eat the banana, but also its skin. -- Guybrush
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
What point are you making ? Some scheme code generated uselless C ? Too bad.. i don't care. It is actually possible to express the C paradigm in a simple grammar. Would be quite simple to translate back and forth too. But maybe it's not enough to prove correctness. On 5 juin 2011 21:01, Amit Kulkarni amitk...@gmail.com wrote: Actually you're right : the C paradigm is straightforward and perfect to handle system code. there you go. as unfortunate as that is, it is still true. Sometimes, I am very surprised C is still around for so long, and essentially unchanged. But its limitations are well known. What I meant to criticize is its grammar : it sucks that we cannot parse C with a simple program. It's not KISS at all and we all pay the price when checking for errors and everytime we wish to process these weird formatted text files. On the other hand, languages based on s-expressions have this unique feature of being very easy to parse and can be processed as regular data, every aspect of the syntax being clean and regular. The problem is that these languages were historically used by pretentious folks on rare supercomputers and thus were not developed to fit the low level paradigm very well. Allegro just recently got SMT/SMP, all others are probably (no research, just throwing it out there) still stuck in single land. While the folks on the supercomputers today are running SMT/SMP in their zillions. That's the cool thing for them and your s-expressions won't help them today. This does not have to be. We should bridge this gap that was forced by ice age investors. Of course i really don't know how nor how it relates to OpenBSD, apart from this common goal of achieving correctness. Just yesterday, I tried chicken scheme and compiled it to C code. The C was unintelligible, why? Because it is setting up the JVM like environment. This goes back to the vmmap thread. Many people try to play OS designers, when very few of them are capable of it. Just leave the OS stuff to the OS people, they will get it right eventually.
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
Uh isn't the biggest problem that all the system code was written in an almost unparsable grammar and practically impossible to audit automatically ? If the language was considered formalized data as well as the data it operates on, such formalized checking features would be easy to grab. Ever heard of s-expressions ? On 31 mai 2011 18:58, Amit Kulkarni amitk...@gmail.com wrote:
Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
http://www.techrepublic.com/blog/security/working-towards-bug-free-secure-software/5560?tag=nl.e036
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
Op 31-5-2011 17:51, Kevin Chadwick schreef: http://www.techrepublic.com/blog/security/working-towards-bug-free-secure-software/5560?tag=nl.e036 Actually they go full steps further. They have produced a formally verified OS kernel, was in the news august 13, 2009: http://tech.slashdot.org/story/09/08/13/0827231/Worlds-First-Formally-Proven-OS-Kernel Erik
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
On Tue, May 31, 2011 at 05:36:17PM +0200, Erik wrote: | Op 31-5-2011 17:51, Kevin Chadwick schreef: | http://www.techrepublic.com/blog/security/working-towards-bug-free-secure-software/5560?tag=nl.e036 | | Actually they go full steps further. They have produced a formally | verified OS kernel, was in the news august 13, 2009: http://tech.slashdot.org/story/09/08/13/0827231/Worlds-First-Formally-Proven-OS-Kernel Beware of bugs in the above code; I have only proved it correct, not tried it. -- Donald E. Knuth -- [++-]+++.+++[---].+++[+ +++-].++[-]+.--.[-] http://www.weirdnet.nl/
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
On Tue, May 31, 2011 at 06:02:39PM +0200, Paul de Weerd wrote: On Tue, May 31, 2011 at 05:36:17PM +0200, Erik wrote: | Op 31-5-2011 17:51, Kevin Chadwick schreef: | http://www.techrepublic.com/blog/security/working-towards-bug-free-secure-software/5560?tag=nl.e036 | | Actually they go full steps further. They have produced a formally | verified OS kernel, was in the news august 13, 2009: http://tech.slashdot.org/story/09/08/13/0827231/Worlds-First-Formally-Proven-OS-Kernel Beware of bugs in the above code; I have only proved it correct, not tried it. Besides that, they use formal proof tools, which are probably much more complex than the code thay are trying to verify and thus have bugs of their own. While formal proofs have their utility (by some accident I studied with Peter van Emde Boas. The above famous quote comes from a letter by Don Knuth to Peter) I don't think formal proofs have a lot of significance when trying to verify a whole OS. -Otto
Re: Seems OpenBSD isn't absolutely alone in it's quest, atleast on embedded systems.
Besides that, they use formal proof tools, which are probably much more complex than the code thay are trying to verify and thus have bugs of their own. While formal proofs have their utility (by some accident I studied with Peter van Emde Boas. The above famous quote comes from a letter by Don Knuth to Peter) I don't think formal proofs have a lot of significance when trying to verify a whole OS. +1. Academics who produce tools which really help in the trenches and remain free to use are rare and to be treasured. It takes lots of time for those kind of formal verification systems and they are for the most part used to beef up the resume. For daily use something like LLVM warnings/errors is much more approachable, and the OpenBSD way of using such stuff daily, and sweeping the codebase for similar bugs. http://blog.llvm.org/2011/05/c-at-google-here-be-dragons.html and how LLVM is designed http://www.aosabook.org/en/llvm.html
