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: 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 =)
