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, why is pcc still in infancy and gcc so
oftenly broken ?
Languages like C let the humans do all the deducive work, though this is
something machines do better.
Wrong! Machines can parse C just as well. Just because you have only
learned lisp doesn't mean other languages are suddenly impossible to
prove.
I happen to know C much better than any Lisp.
Can machines generate C easily ? No.
Do I still use C ? Yes.
Do I see good points in both languages ? Yes.
Are they incompatible ? No !
But everyone gets hurt when we talk about languages. Get over it.
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.
Bwaha. C provers exist. It's not like its rocket science.
You still have to write all the details by hand. Hand-checking small
code is easier. Checking a small code generator is easier than writing
and checking the whole thing.
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..
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.
Or we could actually, you know, fix what already exists.
I'm not fixing this but we have to wake up. And fix the problems at their
root.
We're doing that already. And we're much better in it than you. But
since you express a need to fix problems at their root, please fix the
lisp interpreters in the ports tree.
You are asking me to fix ports because I see a problem in the syntax of
C ? Will you donate hardware ? My implementations work very fine on
-stable amd64. I used to have a -current/amd64 laptop and help with
testing ports/patches but it died not long ago.
Not so OT actually ?
Your original e-mails were about a technique. But now you've switched
from arguing technical merits to preaching. Quite a disappointment
actually.
Do you expect me to spit pro-lisp arguments here ? Go read on your own
if you are that interested
http://www.gigamonkeys.com/book/introduction-why-lisp.html
That some system programmers still ignore much of the details of what was
achieved in programming languages is no surprise,
Flame bait!
What flame ? This is a mere constatation. I do happen to personally know
a few system programmers, not necessarily into OpenBSD though.
our community is broken by
our beliefs that they are fighting on the same plane.
I don't know what "fighting on the same plane" means. Can you please
explain?
There is no one true language. I'm not restating what I've tried to say
before. I separate syntax and semantics. I wish your high opinion of C
was not so tied to its complex syntax. I wish the lispers would embrace
more the semantics of C. Do you really feel the need of excommuniating
me because of heresy about C syntax ?
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.
They're called procedural languages.
C is procedural. Lisp is procedural. Not all languages are procedural.
Along with INTERCAL.
Don't know it, don't care.
Haha you are missing something. Completely useless, unless you enjoy
laughing =)
I'm not advising anyone let off C and those waiting for me to tell them some
truth about programming languages are fucking zombies.
Yeah, let's help the discussion along by name calling!
I don't care about zombies. I really didn't think you'd take it for you !
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 ?
Opinion. But you're right. When I need to get something done, I do
choose the most pretty language in the world to do it.
I think you need to learn what programmers mean with elegance.
Beauty/ugliness is a really useful feeling. Don't you ever see beauty in
the code ? I find much beauty in OpenBSD, and in Lisp.
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.
No no no, not a tree! A string! We write strings of tokens, not trees.
A tree. The string is parsed and converted to an AST. In every C
compiler on earth.
You cannot see them, just trust they are actually there. Or not :
optimizations, defines, bad macros, missing ;, broken lexer, broken
compiler,.. hairy errors.
You're spewing an awful lot of text that makes no sense...
You're not one of those Eliza scripts are you?
You really do not see what I'm trying to say here ?
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.
Ah, much better than the fake ones we always use.
Are you aware that you just rambled your way into functions? Although a
poor explanation it is.
This is not about the better language : its about finding a right
representation for the code. You obviously do not understand lisp macros
and I wont spit a book about them here. And yes, C macros are not true
macros, just a text processing hack that sucks and make parsing C really
a hard task, breaking the pipeline in two. I'm really not saying
incredible things here.
- avoid needing so much complexity just for parsing/compiling => more trust,
less to check by hand
Yes, they're called functions.
No, functions (when not inlined) are run-time interfaces. I'm talking
about source-code representation and transformation. This is very
different in nature. I cannot explain Lisp macros here, sorry.
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.
Hmm, tokens.
I think I made my point,
Huh, point? Where?
maybe now I'll try to shut up.
And there was much rejoycing.
You're boring me.
I'm not boring you. You replied, mischaracterizing what I said, forcing
me to not shut up.
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.
Distrust to our biggest tools? You're right, I do distrust you.
Thanks.. Now how can you trust your distrust of me, having not even
considered what I was saying ? You clearly did not try to read about
anything I pointed at, and clearly do not know much about it. You seem
pretty confident about bringing me down don't you ?
--
Thomas de Grivel
"I must plunge into the water of doubt again and again."
