| Author |
Message |
|
| flaig at hablas.com |
 Posted: Thu May 29, 2003 7:58 am |
 |
|
|
Guest
|
Hi all,
from my bit of Italian, I think it ought to be "Eppur suga" -- the Latin -t is dropped in the 3rd person singular AFAIK, and it is certainly not reflexive... it does not suck itself, that were recursion.
 ))
Now for something more serious... I think the basic sentiment we all share is that Java sucks, and that C++ sucks. They do, and very badly too, and it is annoying to see that they have become a kind of de facto standard.
I have used both (more than Erlang, I am afraid -- as a molecular biologist, I have to deal with megabyte arrays, and that is not quite what Erlang was designed for -- sinner repent -- well Ocaml is quite nice too ), and I am equally fed up with the cobolesque boilerplate of
"private final static paralyzed karl.otto.gustav emil = (karl.otto.gustav) ((egon.kasimir) foo.bar().blah[anything])"
and the orkish scrawls of
"#define n<m>(x,i,j) {*++(*x)->y %= (i>j)?&i--:--&j}", not to mention memory leaks and, and, and... Maybe OO itself does not suck but a concept without implementation is void.
But I think we are missing the point. The important thing is not that OO is an inferior concept but that FP (or COPL, if you please) is a superior one. Erlang were still great even Stroustrup and Gosling had never come near a computer -- because it enables you to be productive, to write clear and concise code, to cope with errors and, last but not least, because it allows reasoning.
This latest thing is what I have really been missing. Erlang is a functional language, so it should be possible to employ automatic theorem provers and all that kind of stuff. Cummings wrote about ML: "We are not trying to develop 'safer' programs by testing, but developing SAFE programs by reasoning." This is a very philosophical matter. Let me say that Java and C++ rely on induction, Erlang allows deduction, and Sir Karl Popper has said the rest about that, decades ago. So are there any theorem provers for Erlang, as there are for Lisp and ML? Can we prove a program's correctness by reasoning? If not, let's do that!
The other point is that the power of Erlang's concurrency is often underestimated by folks who are not interested in parallelism itself. I am a complete layman to that field but I think that neuronal networks would be a great thing do with Erlang. Has anybody tried this before? Are there any projects in similar fields? Personally, I was attracted to Erlang because I felt that simulation of complex biological processes would be easy to implement. Imagine you have a microbe with some 4000 genes, each with a state of activity and each influencing a couple of others. In Erlang, this would be straightforward... I met a guy who did the like and spend a year on that programming the basic mechanism in Java! So I think we could get away from that "Erlang? Oh, that's for telephones only" image.
Has anybody worked on this yet?
Skål,
Ruediger Marcus Flaig
Dr. Dr. Ruediger Marcus Flaig
Institute for Immunology
University of Heidelberg
Im Neuenheimer Feld 305
D-69120 Heidelberg
<flaig_at_cirith-ungol.sanctacaris.net>
Tel. +49-172-7652946
| +49-6221-56-5402
| +49-6221-432963
_____________________________________________________________
Free eMail .... the way it should be....
http://www.hablas.com
_____________________________________________________________
Select your own custom email address for FREE! Get you_at_yourchoice.com w/No Ads, 6MB, POP & more! http://www.everyone.net/selectmail?campaign=tag
Post generated using Mail2Forum (http://m2f.sourceforge.net) |
|
|
| Back to top |
|
| erlang at manderp.freeser |
| Posted: Thu May 29, 2003 9:09 am |
|
|
|
Guest
|
Have a look here:
http://www.sics.se/fdt/projects/vericode/index.html
However, I'm not so sure that the proof of correctness is either
absolutely necessary or even achievable. But I'm a pragmatist, not a
mathematician, and pragmatically I find that Erlang has a vastly
superior way of dealing with the unexpected. In all other languages I
know there is nothing that equals the process linking and exit trapping
provided by Erlang. Being able to effectively and efficiently firewall
suspect code with supervisor processes is remarkably powerful. It
doesn't guarantee that code will _always_ work correctly, but it does
prevent a mistake becoming a disaster!
<rant>
Even when there is a basic error trapping mechanism, as with C++
exceptions, I've found that some programmers *avoid* using it due to
efficiency concerns with stack unrolling! When something has failed,
what's the point of rushing to bring the *whole* system down?! If the
error is handled correctly by a conscientious programmer, they would
perform the same process of unrolling with no discernable benefit and
possibly introduce more bugs too.
I've tried to explain this to these hot-heads but they didn't get it!
How can one sell the virtues of program verification to code monkeys
like them? I think firewalling their code is the only solution!
</rant>
Pete.
Dr.Dr.Ruediger M.Flaig wrote:
> Hi all,
>
> from my bit of Italian, I think it ought to be "Eppur suga" -- the Latin -t is dropped in the 3rd person singular AFAIK, and it is certainly not reflexive... it does not suck itself, thaat were recursion.
> ))
>
> Now for something more serious... I think the basic sentiment we all share is that Java sucks, and that C++ sucks. They do, and very badly too, and it is annoying to see that they have become a kind of de facto standard.
>
> I have used both (more than Erlang, I am afraid -- as a molecular biologist, I have to deal with megabyte arrays, and that is not quite what Erlang was designed for -- sinnerr repent -- well Ocaml is quite nice too ), and I am equally fed up with the cobolesque boilerplate of
> "private final static paralyzed karl.otto.gustav emil = (karl.otto.gustav) ((egon.kasimir) foo.bar().blah[anything])"
> and the orkish scrawls of
> "#define n<m>(x,i,j) {*++(*x)->y %= (i>j)?&i--:--&j}", not to mention memory leaks and, and, and... Maybe OO itself does not suck but a concept without implementation is void.
>
> But I think we are missing the point. The important thing is not that OO is an inferior concept but that FP (or COPL, if you please) is a superior one. Erlang were still great even Stroustrup and Gosling had never come near a computer -- because it enables you to be productive, to write clear and concise code, to cope with errors and, last but not least, becaause it allows reasoning.
>
> This latest thing is what I have really been missing. Erlang is a functional language, so it should be possible to employ automatic theorem provers and all that kind of stuff. Cummings wrote about ML: "We are not trying to develop 'safer' programs by testing, but developing SAFE programs by reasoning." This is a very philosophical matter. Let me say that Java and C++ rely on induction, Erlang allows deduction, and Sir Karl Popper has said the rest about that, decades ago. So are there any theorem provers for Erlang, as there are for Lisp and ML? Can we prove a program's correctness by reasoning? If not, let's do that!
>
> The other point is that the power of Erlang's concurrency is often underestimated by folks who are not interested in parallelism itself. I am a complete layman to that field but I think that neuronal networks would be a great thing do with Erlang. Has anybody tried this before? Are there any projects in similar fields? Personally, I was attracted to Erlang because I felt that simulation of complex biological processes would be easy to implement. Imagine you have a microbe with some 4000 genes, each with a state of activity and each influencing a couple of others. In Erlang, this would be straightforward... I met a guy who did the like and spend a year on that programming the basic mechanism in Java! So I think we could get away from that "Erlang? Oh, that's for telephones only" image.
>
> Has anybody worked on this yet?
>
>
> Sk |
|
|
| Back to top |
|
| serge at hq.idt.net |
| Posted: Thu May 29, 2003 3:16 pm |
|
|
|
Guest
|
I happened to have quite a bit of experience with Neural Networks, (I
got a Master degree in biomedical engineering, doing research in retinal
image processing and automated feature extraction and classification
using neural nets).
For the past several months I've been studying Erlang, and see that
while it is extreemly compact and efficient in solving distributed and
concurrent problems, it lacks the computational power (which it wasn't
designed for anyway).
In Neural Nets one needs to perform a lot of calculations involved in
training a network of neurons. The goal is given an input and knowing
the output to find a distribution of weights between N interconnected
nodes a multi-layered network that allows the network to be
deterministic with respect to given input/output templates. The
training involves a lot of iterations that are in the order of the
number of neurons times the number of interconnects divided by some scalar.
So in my opinion Erlang is not quite well suited for this
performance-wise, as in my iterative tests it was about 10 to 13 times
slower than C / Pascal.
Regards,
Serge
Dr.Dr.Ruediger M.Flaig wrote:
> Hi all,
>
> from my bit of Italian, I think it ought to be "Eppur suga" -- the
Latin -t is dropped in the 3rd person singular AFAIK, and it is
certainly not reflexive... it does not suck itself, thaat were recursion.
> ))
>
> Now for something more serious... I think the basic sentiment we all
share is that Java sucks, and that C++ sucks. They do, and very badly
too, and it is annoying to see that they have become a kind of de facto
standard.
>
> I have used both (more than Erlang, I am afraid -- as a molecular
biologist, I have to deal with megabyte arrays, and that is not quite
what Erlang was designed for -- sinnerr repent -- well Ocaml is quite
nice too ), and I am equally fed up with the cobolesque boilerplate of
> "private final static paralyzed karl.otto.gustav emil =
(karl.otto.gustav) ((egon.kasimir) foo.bar().blah[anything])"
> and the orkish scrawls of
> "#define n<m>(x,i,j) {*++(*x)->y %= (i>j)?&i--:--&j}", not to mention
memory leaks and, and, and... Maybe OO itself does not suck but a
concept without implementation is void.
>
> But I think we are missing the point. The important thing is not that
OO is an inferior concept but that FP (or COPL, if you please) is a
superior one. Erlang were still great even Stroustrup and Gosling had
never come near a computer -- because it enables you to be productive,
to write clear and concise code, to cope with errors and, last but not
least, becaause it allows reasoning.
>
> This latest thing is what I have really been missing. Erlang is a
functional language, so it should be possible to employ automatic
theorem provers and all that kind of stuff. Cummings wrote about ML: "We
are not trying to develop 'safer' programs by testing, but developing
SAFE programs by reasoning." This is a very philosophical matter. Let me
say that Java and C++ rely on induction, Erlang allows deduction, and
Sir Karl Popper has said the rest about that, decades ago. So are there
any theorem provers for Erlang, as there are for Lisp and ML? Can we
prove a program's correctness by reasoning? If not, let's do that!
>
> The other point is that the power of Erlang's concurrency is often
underestimated by folks who are not interested in parallelism itself. I
am a complete layman to that field but I think that neuronal networks
would be a great thing do with Erlang. Has anybody tried this before?
Are there any projects in similar fields? Personally, I was attracted to
Erlang because I felt that simulation of complex biological processes
would be easy to implement. Imagine you have a microbe with some 4000
genes, each with a state of activity and each influencing a couple of
others. In Erlang, this would be straightforward... I met a guy who did
the like and spend a year on that programming the basic mechanism in
Java! So I think we could get away from that "Erlang? Oh, that's for
telephones only" image.
>
> Has anybody worked on this yet?
>
>
> Sk |
|
|
| Back to top |
|
| cpressey at catseye.mb.ca |
| Posted: Thu May 29, 2003 10:01 pm |
|
|
|
Guest
|
On Thu, 29 May 2003 00:58:27 -0700 (PDT)
"Dr.Dr.Ruediger M.Flaig" <flaig_at_hablas.com> wrote:
> [...]
> So are there any theorem provers for Erlang, as there are for
> Lisp and ML?
Yes, it's called "the human mind" :)
Seriously, I think it's a lot more effective for the programmer to prove
their code to his/herself while writing it, than to prove it
mechanically after the fact. In fact I think most (good) programmers do
this subconsciously, and testing is part of it, to reassure themselves
that they wrote what they meant to write.
I do think there's room for more verification in Erlang (e.g. inferring
type signatures...) but I think it's more suited to the ground-up
'linting' variety.
Disclaimer: I'm mostly a pragmatist too.
-Chris
Post generated using Mail2Forum (http://m2f.sourceforge.net) |
|
|
| Back to top |
|
| matthias at corelatus.se |
| Posted: Thu May 29, 2003 10:29 pm |
|
|
|
Guest
|
Dr.Dr.Ruediger M.Flaig writes:
> This latest thing is what I have really been missing. Erlang is
> a functional language, so it should be possible to employ
> automatic theorem provers and all that kind of stuff.
Thomas Arts is one of the people who have been involved in work in
this area. You can read about it here
http://www.sics.se/fdt/projects/vericode/evt.html
or on the links you get from google if you enter "Erlang Theorem
Prover".
Matthias
Post generated using Mail2Forum (http://m2f.sourceforge.net) |
|
|
| Back to top |
|
| tony at rogvall.com |
| Posted: Thu May 29, 2003 10:47 pm |
|
|
|
Guest
|
On Thu, 2003-05-29 at 23:59, Chris Pressey wrote:
> On Thu, 29 May 2003 00:58:27 -0700 (PDT)
> "Dr.Dr.Ruediger M.Flaig" <flaig_at_hablas.com> wrote:
>
> it's called "the human mind" 
>
> Seriously, I think it's a lot more effective for the programmer to prove
> their code to his/herself while writing it, than to prove it
> mechanically after the fact. In fact I think most (good) programmers do
> this subconsciously, and testing is part of it, to reassure themselves
> that they wrote what they meant to write.
>
I guess this is a flame, I wont go for it :-)
/Tony
Post generated using Mail2Forum (http://m2f.sourceforge.net) |
|
|
| Back to top |
|
| cpressey at catseye.mb.ca |
| Posted: Fri May 30, 2003 12:31 am |
|
|
|
Guest
|
On 30 May 2003 00:47:31 +0200
Tony Rogvall <tony_at_rogvall.com> wrote:
> On Thu, 2003-05-29 at 23:59, Chris Pressey wrote:
> > On Thu, 29 May 2003 00:58:27 -0700 (PDT)
> > "Dr.Dr.Ruediger M.Flaig" <flaig_at_hablas.com> wrote:
> >
> > it's called "the human mind"
> >
> > Seriously, I think it's a lot more effective for the programmer to
> > prove their code to his/herself while writing it, than to prove it
> > mechanically after the fact. In fact I think most (good)
> > programmers do this subconsciously, and testing is part of it, to
> > reassure themselves that they wrote what they meant to write.
> >
>
> I guess this is a flame, I wont go for it
>
> /Tony
Not at all, my good man! Although perhaps I stated it less than
elegantly.
Took me a while, but I managed to find where I picked up the notion:
_Theories of Programming Languages_ by John C Reynolds (Cambridge
University Press, 1998), p. 54 (emphasis mine):
"This is not to say that every program merits formal proof. Experience
with formal proof methods, however, also increases a programmer's
ability to detect flaws in informal arguments. The inference rules
introduced in this chapter are fundamental laws about imperative
programming, in the same sense that the associative, commutative, and
distributative laws are fundamental laws about arithmetic. When
mathematically literate people perform or check an elementary algebraic
manipulation, they rarely descend to the level of applying such laws
explicitly, but their knowledge of these laws, and their experience in
applying them, underly their ability to avoid and detect errors. _A
similar knowledge and experience of program-proof systems can buttress
such an ability for programming_."
Further on, p. 71:
"As a second example, we will prove the total correctness of a program
that computes x^n in log n time. In this case, we want to demonstrate
that _one does not have to prove programs after the fact, but that
program proof can go hand in hand with program construction_."
p. 72:
"At this point, we have an informal account of the first step in a
top-down program construction: _we know how to write the program if we
can write a while body B with certain properties_."
In other words: start with the specification, derive the program from it
while proving it, and the program will be correct "out of the box".
Of course, running the program through a proof-checker after all is said
and done can't hurt either. But it seems like the long way around, and
might be subject to the "seatbelt effect" where the programmer feels he
or she can afford to be sloppy, not realizing that mistakes, even when
caught, will still have to be fixed eventually.
To say nothing about determining whether the specification for a large
program is, itself, correct - oi!
-Chris
Post generated using Mail2Forum (http://m2f.sourceforge.net) |
|
|
| Back to top |
|
| wuji |
| Posted: Wed Sep 12, 2012 7:04 am |
|
|
|
User
Joined: 10 Aug 2012
Posts: 654
|
first heard this story, I think my initial reaction is to be be cheap replica designer *beep* be a little bit in disbelief, and a little bit horrified," said
Charles Sophy, a psychiatrist. "There's a lot of psychological damage that can can jordan 11 concords can be caused."MTV Producer Gabriel Ben-Meir Killed: Two Suspects HeldPolice Arrest Pair
Connection With Killings of Ben-Meir and Another Man.By MICHAEL S. JAMES and and replica designer *beep* and RUSSELL GOLDMANMay 12, 2011 — A man and a woman are
held on suspicion of murder in the shotgun deaths of an MTV MTV cheap replica designer *beep* MTV producer early Sunday morning and another man a week earlier.Jabaar Vincent
and Destiny Young were arrested Wednesday evening in connection with the killings killings replica designer *beep* killings of MTV music coordinator Gabriel Ben-Meir, 30, outside his home in |
|
|
| Back to top |
 
|
|
|
All times are GMT
|
|
You cannot post new topics in this forum
You cannot reply to topics in this forum
You cannot edit your posts in this forum
You cannot delete your posts in this forum
You cannot vote in polls in this forum
You cannot attach files in this forum
You cannot download files in this forum
|
|
|
Digg It
Del.icio.us
Reddit
Facebook
Stumble Upon
Technorati
