Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.lang.forth > #15078 > unrolled thread
| Started by | visualforth@rocketmail.com |
|---|---|
| First post | 2012-08-21 21:43 -0700 |
| Last post | 2012-08-22 07:37 -0700 |
| Articles | 20 on this page of 163 — 19 participants |
Back to article view | Back to comp.lang.forth
Comparative Productivity of Programming Languages visualforth@rocketmail.com - 2012-08-21 21:43 -0700
Re: Comparative Productivity of Programming Languages "A. K." <akk@nospam.org> - 2012-08-22 07:07 +0200
Re: Comparative Productivity of Programming Languages Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-08-22 03:35 -0500
Re: Comparative Productivity of Programming Languages John Passaniti <john.passaniti@gmail.com> - 2012-08-22 14:06 -0700
Function Points (was: Comparative Productivity of Programming Languages) anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-23 14:50 +0000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-23 11:43 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-25 14:13 +0000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-25 10:12 -0700
Re: Function Points Doug Hoffman <glidedog@gmail.com> - 2012-08-25 15:39 -0400
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-25 15:09 -0700
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-08-25 12:34 -1000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-25 16:43 -0700
Re: Function Points jacko <jackokring@gmail.com> - 2012-08-25 18:05 -0700
Re: Function Points jacko <jackokring@gmail.com> - 2012-08-25 20:34 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-26 03:24 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-25 22:44 -0700
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-08-25 21:19 -1000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-26 00:36 -0700
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-08-25 21:50 -1000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-26 01:08 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-26 23:20 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-26 19:33 -0700
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-08-27 13:34 -0500
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-27 22:38 +0200
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-08-28 02:45 -0500
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-27 18:14 -0700
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-27 18:24 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-30 14:22 +0000
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-08-28 03:07 -0500
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-28 08:18 -0700
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-08-28 12:15 -0500
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-28 23:05 -0700
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-08-29 03:55 -0500
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-27 22:28 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-27 20:26 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-28 23:17 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-29 01:13 -0700
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-29 02:23 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-30 02:59 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-29 22:18 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-30 20:44 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-31 01:29 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-31 09:33 +0000
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-30 02:58 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-29 19:39 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-30 14:10 +0000
Re: Function Points gavino_himself <visploveslisp@gmail.com> - 2012-08-30 20:08 -0700
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-08-30 17:47 -1000
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-08-27 13:43 -1000
Re: Function Points "Paul E. Bennett" <Paul_E.Bennett@topmail.co.uk> - 2012-08-27 12:14 +0100
Re: Function Points Mark Wills <markrobertwills@yahoo.co.uk> - 2012-08-27 05:12 -0700
Re: Function Points "Paul E. Bennett" <Paul_E.Bennett@topmail.co.uk> - 2012-08-27 15:52 +0100
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-26 13:09 +0000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-27 20:52 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-30 14:08 +0000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-30 10:43 -0700
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-08-30 08:25 -1000
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-08-30 22:42 +0200
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-08-31 01:23 -0400
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-08-31 03:08 -0500
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-08-31 18:56 -0400
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-01 02:35 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-31 23:52 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-01 14:27 +0000
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-01 14:18 +0000
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-01 17:45 +0200
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-01 16:14 +0000
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-01 19:13 +0200
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-09-02 03:19 -0500
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-01 16:18 -0400
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-02 03:04 +0200
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-02 04:02 -0400
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-02 17:40 +0200
Re: Function Points jim@rainbarrel.com - 2012-09-02 10:32 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-02 20:49 +0200
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-02 16:33 -0400
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-02 17:03 -0400
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-09-02 09:02 -1000
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-02 16:35 -0400
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-09-02 13:42 -1000
Re: Function Points jim@rainbarrel.com - 2012-09-02 16:54 -0700
Re: Function Points Mark Wills <markrobertwills@yahoo.co.uk> - 2012-09-03 00:29 -0700
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-03 01:30 -0400
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-09-02 21:21 -1000
Re: Function Points jim@rainbarrel.com - 2012-09-03 10:37 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-04 07:14 +0000
Re: Function Points Coos Haak <chforth@hccnet.nl> - 2012-09-03 21:12 +0200
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-03 17:32 -0400
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-03 17:51 -0400
Re: Function Points John Passaniti <john.passaniti@gmail.com> - 2012-09-03 22:37 -0700
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-04 04:25 -0400
Re: Function Points John Passaniti <john.passaniti@gmail.com> - 2012-09-04 07:35 -0700
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-05 02:13 -0400
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-09-04 20:18 -1000
Re: Function Points John Passaniti <john.passaniti@gmail.com> - 2012-09-05 10:56 -0700
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-05 16:11 -0400
Re: Function Points John Passaniti <john.passaniti@gmail.com> - 2012-09-05 14:07 -0700
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-02 16:27 -0400
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-03 00:52 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-02 16:28 -0700
Re: Function Points jim@rainbarrel.com - 2012-09-02 16:48 -0700
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-02 20:21 -0400
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-09-02 14:45 -1000
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-03 01:12 -0400
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-09-02 21:26 -1000
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-03 01:06 -0400
Re: Function Points Mark Wills <markrobertwills@yahoo.co.uk> - 2012-08-31 03:29 -0700
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-31 10:35 +0000
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-08-31 18:49 -0400
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-01 14:49 +0000
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-09-01 08:36 -1000
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-01 16:11 -0400
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-03 01:58 +0200
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-01 17:54 +0200
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-01 16:19 -0400
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-02 03:05 +0200
Re: Function Points Coos Haak <chforth@hccnet.nl> - 2012-08-31 23:10 +0200
Re: Function Points "Elizabeth D. Rather" <erather@forth.com> - 2012-08-31 15:50 -1000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-01 10:31 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-01 21:52 +0200
Re: Function Points "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-09-01 16:36 -0400
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-01 14:36 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-02 03:30 +0200
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-02 23:15 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-02 15:02 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-03 01:50 +0200
Re: Function Points jim@rainbarrel.com - 2012-09-02 16:57 -0700
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-03 23:11 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-04 14:30 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-04 10:14 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-04 22:10 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-06 00:19 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-06 17:48 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-06 12:01 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-06 22:02 +0200
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-09-06 14:19 -0700
Heap (was: Function Points) anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-07 11:30 +0000
Re: Heap (was: Function Points) Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-07 18:12 +0200
Re: Heap (was: Function Points) anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-07 16:48 +0000
Re: Heap (was: Function Points) Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-07 21:34 +0200
Re: Heap Gerry Jackson <gerry@jackson9000.fsnet.co.uk> - 2012-09-07 22:04 +0100
Re: Heap anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-08 11:52 +0000
Re: Heap Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-08 22:48 +0200
Re: Heap (was: Function Points) anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-08 12:11 +0000
priority queue (was: Function Points) anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-09-03 11:46 +0000
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-03 15:03 +0200
Re: Function Points mhx@iae.nl (Marcel Hendrix) - 2012-09-03 22:36 +0200
Re: Function Points mhx@iae.nl (Marcel Hendrix) - 2012-09-06 20:27 +0200
Re: Function Points Andrew Haley <andrew29@littlepinkcloud.invalid> - 2012-09-02 04:00 -0500
Re: Function Points visualforth@rocketmail.com - 2012-09-03 10:40 -0700
Re: Function Points Bernd Paysan <bernd.paysan@gmx.de> - 2012-09-03 20:26 +0200
Re: Function Points Doug Hoffman <glidedog@gmail.com> - 2012-08-27 11:49 -0400
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-27 09:16 -0700
Re: Function Points Josh Grams <josh@qualdan.com> - 2012-08-28 22:46 +0000
Re: Function Points jacko <jackokring@gmail.com> - 2012-08-28 16:06 -0700
Re: Function Points Doug Hoffman <glidedog@gmail.com> - 2012-08-28 20:50 -0400
Re: Function Points anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-26 12:59 +0000
Re: Function Points Paul Rubin <no.email@nospam.invalid> - 2012-08-26 22:24 -0700
Re: Function Points (was: Comparative Productivity of Programming Languages) John Passaniti <john.passaniti@gmail.com> - 2012-08-23 15:02 -0700
Re: Function Points (was: Comparative Productivity of Programming Languages) anton@mips.complang.tuwien.ac.at (Anton Ertl) - 2012-08-25 14:57 +0000
Re: Comparative Productivity of Programming Languages "Rod Pemberton" <do_not_have@notemailnot.cmm> - 2012-08-22 08:07 -0400
Re: Comparative Productivity of Programming Languages visualforth@rocketmail.com - 2012-08-22 08:12 -0700
Re: Comparative Productivity of Programming Languages visualforth@rocketmail.com - 2012-08-22 07:37 -0700
Page 3 of 9 — ← Prev page 1 2 [3] 4 5 6 7 8 9 Next page →
| From | Bernd Paysan <bernd.paysan@gmx.de> |
|---|---|
| Date | 2012-08-30 20:44 +0200 |
| Subject | Re: Function Points |
| Message-ID | <2936343.pbmfiLh0sr@sunwukong.fritz.box> |
| In reply to | #15258 |
Paul Rubin wrote: > It's untyped in the sense that the compiler doesn't know about the > types: they are solely in the mind of the programmer and in the > comment, i.e. part of the "semantic gap" mentioned earlier. With our "do what I say" philosophy, there is indeed a semantic gap, between "what I mean" and "what I say". The semantics of the Forth compiler is close to that of the hardware, i.e. the thing is an imperative state machine with an array of bytes called "memory", and a few registers like sp/rp/ip. The complaint by the semantic gap idea is that people don't express their toughts in terms of such a state machine, and higher level languages allow them to express their thought in a different way, which then is compiled to state machine code. However, the world of mathematical functions is no less alien to us humans than the world of state machines. IMHO, the mathematical background of Computer Science is what is driving functional programming languages and proof systems: That's their "home turf". For us Forthers, with our mantra "avoid unnecessary abstractions", it is an abstraction with dubious value. It takes you away from the machine, and when you write code for the machine, it may be just in the way. > FWIW, Forth's "types" aren't that precise about functions, e.g.: > > : triple ( n -- n ) 3 * ; > : do-twice ( n xt -- n ) swap over execute swap execute ; > : times-9 ( n -- n ) ['] triple do-twice ; > > In Haskell, we'd give do-twice a type like > > Integer -> (Integer -> Integer) -> Integer > > i.e. something like ( n ( n -- n ) -- n ) in pseudo-Forth notation. Well, xt is a placeholder type, if you document carefully, you would document what xt does. However, "do-twice" should be written : do-twice ( i*x xt -- k*x ) >r r@ execute r> execute ; \ xt's stack effect is ( i*x -- j*x ) so that \ when applied to j*x it gives k*x for good reasons. That way, you can define : f4* ( r -- r ) ['] f2* do-twice ; and the documented rule of the stack effect of xt for do-twice is that it is transitive (i.e. you can apply it to its own output). This is even allowed when the function reduces something: : +3 ( n1 n2 n3 -- nsum ) ['] + do-twice ; : !+ ( x addr -- addr' ) dup cell+ >r ! r> ; : 2! ( d addr -- ) ['] !+ do-twice drop ; The rule of thumb for higher-order Forth words (i.e. words that take an xt) is that you a) specify the stack effect of that xt and b) you allow the word to access the stack beneath. I.e. the higher order function is not allowed to keep things on the stack below the parameters for which it calls xt. Static typing languages like C++ use templates for that, but the result is code explosion, because the compiler recompiles that whenever you use a new type. -- Bernd Paysan "If you want it done right, you have to do it yourself" http://bernd-paysan.de/
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2012-08-31 01:29 -0700 |
| Subject | Re: Function Points |
| Message-ID | <7xzk5b8nxl.fsf@ruckus.brouhaha.com> |
| In reply to | #15277 |
Bernd Paysan <bernd.paysan@gmx.de> writes: > : do-twice ( i*x xt -- k*x ) >r r@ execute r> execute ; > \ xt's stack effect is ( i*x -- j*x ) so that > \ when applied to j*x it gives k*x > > for good reasons. That way, you can define > > : f4* ( r -- r ) ['] f2* do-twice ; Oh thanks, I like this, writing do-twice that way means it's independent of the xt's stack effect. > I.e. the higher order function is not allowed to keep things on the > stack below the parameters for which it calls xt. So my version temporarily had the stack in the state ( xt n xt ) which wasn't so good because of the xt behind the n. I guess avoiding that is a good general guideline. Of course there will still be stuff on the stack from do-twice's caller. > Static typing languages like C++ use templates for that, but the result > is code explosion, because the compiler recompiles that whenever you use > a new type. I think it does that either for C compatibility, or to generate the fastest possible code. It could in principle (unless there's some C++-specific issue preventing it) use an OO-like dispatch based on the argument type instead. GHC does something like that, taking a minor speed hit to avoid duplicating so much code.
[toc] | [prev] | [next] | [standalone]
| From | anton@mips.complang.tuwien.ac.at (Anton Ertl) |
|---|---|
| Date | 2012-08-31 09:33 +0000 |
| Subject | Re: Function Points |
| Message-ID | <2012Aug31.113310@mips.complang.tuwien.ac.at> |
| In reply to | #15302 |
Paul Rubin <no.email@nospam.invalid> writes:
>Bernd Paysan <bernd.paysan@gmx.de> writes:
>> I.e. the higher order function is not allowed to keep things on the
>> stack below the parameters for which it calls xt.
>
>So my version temporarily had the stack in the state ( xt n xt ) which
>wasn't so good because of the xt behind the n. I guess avoiding that is
>a good general guideline. Of course there will still be stuff on the
>stack from do-twice's caller.
Yes, the idea of that principle is to allow to pass data from the
caller to the xt (and back) through the data stack. Of course, if the
caller is a higher-order word itself, it should follow that principle
itself.
>> Static typing languages like C++ use templates for that, but the result
>> is code explosion, because the compiler recompiles that whenever you use
>> a new type.
>
>I think it does that either for C compatibility, or to generate the
>fastest possible code. It could in principle (unless there's some
>C++-specific issue preventing it) use an OO-like dispatch based on the
>argument type instead.
Yes, there is at least one C++-specific issue preventing it: In
general data structures in C++ are not implemented in a way that
allows this. There would be more boxing needed to allow a
one-implementation-fits-all approach. There may be other issues.
- anton
--
M. Anton Ertl http://www.complang.tuwien.ac.at/anton/home.html
comp.lang.forth FAQs: http://www.complang.tuwien.ac.at/forth/faq/toc.html
New standard: http://www.forth200x.org/forth200x.html
EuroForth 2012: http://www.euroforth.org/ef12/
[toc] | [prev] | [next] | [standalone]
| From | Bernd Paysan <bernd.paysan@gmx.de> |
|---|---|
| Date | 2012-08-30 02:58 +0200 |
| Subject | Re: Function Points |
| Message-ID | <1594479.i3UzpqWyUP@sunwukong.fritz.box> |
| In reply to | #15236 |
Paul Rubin wrote: >> Coq's proof system is similar to other formal proof systems (the ones >> formalized in the late 20th of the previous century). > > You mean 1995-2000? No, the systems were formalized before 1930. We got Kurt Gödel's wonderful proof of incompleteness out of that formalization. Coq adds enough expressive power to its "type" system that it comes under the same sort of formalized proof systems. Ah, and the 1995-2000 frame is indeed where enough progress was done on automated proof systems to actually try using it in a programming language. But that's the proof system side. >> No, an error message is a negative feedback, it tells you "you did >> something wrong". > > I mean really, some people are really into it. There's a Haskell blog > whose title is "The power of types compels you": > > The types. At first, they helped me to write programs, then it > turned into an obsession. Compulsive need to turn every possible > programming error into statically checked type error, consumed my > soul. Soon, it was impossible for me to code anymore - inability to > express the proper solution in types and constant strive for > perfection rendered me unable to accept inferior solutions. > > Would I stop myself, three years ago, from writing the first fold? > Of course not, I choose to believe what I was programmed to > believe. > > OK, enough of that, it probably wasn't funny anyway. > (http://paczesiowa.blogspot.com/2010_01_01_archive.html) This poor soul should read Gödel's proof of incompleteness, following by Turing's proof of the unsolvable halting problem as examples that you simply can't do that - or you are restricting yourself too much. >> The specification of the conditions is just as bug-prone as the >> program itself (or even more), so proving equivalence does not prove >> absense of bugs. > > I think that's more true in the hardware control or human interaction > world, than in the purely computational world. It's far easier to > state Fermat's Last Theorem (the specification) than it is to prove it > (the program). That's a particular odd example, real-world examples are not that odd. The usual problem is that you don't have much trouble writing down necessary conditions, but they usually aren't sufficient. The same problem as with testing. >>> you've got some sound but non-trivial reasoning showing that x>0 >> You shouldn't have non-trivial reasonings for that. Trivial >> reasonings are ok, e.g. x is a pointer, and you don't pass null >> pointers around, only allocated objects. > > Every nontrivial algorithm uses nontrivial reasoning, or else the > algorithm would itself be trivial. Do you mean we should only use > trivial algorithms? Of course. Debugging is said to be twice as hard, so you should only write code that is so easy that you yourself can debug it. Proving your code is correct is even worse. So try to keep your code trivial. If your customer likes to have things done which can't be done with trivial code, try to figure out how close you can get to your customer's wishes with trivial code, and negotiate the rest away. >> This is where I think it becomes silly. If you can write your >> reasoning down in a formalized language, you should be able to get a >> working program from that (e.g. using the methods Prolog uses). > > That's a far, far harder problem, that nobody has much clue about > right > now. It amounts to automated theorem proving. Prolog simply uses > exponential search with some unreliable heuristics, so on non-trivial > problems it just won't finish in a practical amount of time. Indeed. You shouldn't do non-trivial problems, see above. > By > comparison, machine-checking the correctness of a human-created proof > is much better understood by now. Yes. The hard work is left to the human. >> I also don't think there is a semantic gap between programmer >> knowledge and program, > > If the programmer can explain or document worthwhile facts about > the program that aren't formally part of the code, then that knowledge > is part of the semantic gap. The "do what I mean" programming language is yet another problem which we don't have any idea how to implement it. We have means of adding the typical formal knowledge a programmer has to a program, which are a) assertions - the programmer knows which assumptions he thinks hold true b) examples - the programmer knows input->output relations for exemplary data. We call this test cases. Systems like Coq add a third layer: c) proofs - the programmer knows proofs for correctness of his program. >> If you have forgotten how most of your program works, adding a new >> feature is futile. > > Of course programmers are required all the time to add new features to > unfamiliar legacy code. If you wrote the code yourself and forgot > most of the details, you're still a few steps ahead of someone who has > never seen the code before. And they curse about that, and the typical reaction to this request is "the code must be rewritten from scratch, as it is an unmaintainable mess" :-). >> Though, some programs make it easier for bad programmers to be >> learned, and I'd say, Haskell is really driving bad programmers to >> Python and PHP. > > I'm not sure what you mean by this. PHP certainly has a lot of crap > code written by low-skill programmers, while getting past Haskell's > early learning curve takes quite a lot of effort. Yes, that's what I mean. > Haskell programmers > tend to be extremely skillful, which is one of the things that > attracts > me to the Haskell community. (Forth is the same way, which is part of > why I still hang around here). I don't know of anyone switching from > Haskell to Python or PHP; it's always the other direction. Hehe. >>> Automatic tests help, but they aren't a silver bullet. >> But automated proofs are no silver bullet, either. Essentially, >> there is no silver bullet. > > This guy claims there is something like Moore's law for programmer > productivity: http://people.cs.umass.edu/~yannis/law.html > Why would this be? Languages would seem to have something to do with > it. Languages, methodologies, and response times of our machines. One thing that is particular about Forth is that the machine responds to the programmer in real time (i.e. fast enough that the human doesn't have to wait for the machine). This sort of response is now available for more programming languages than it used to be, because our machines are faster now. >> Haskell would probably give me some headaches with the low-level >> code, where I just need to get nanoseconds from the OS timer, and >> pack bytes together into a packet to be send at the given time >> through a network socket, but it should have no problem to compute >> the sending rate. > > Just reading the system timer and writing bytes at a given time is no > problem. If you need consistent sub-millisecond accuracy, random GC > delays might get in the way of that, but you could queue the packets > through a separate real-time process. No, random delays are not actually a problem, as we see random delays like that in the rest of the network, too - and I don't use real-time processes now, either. Any other process can interfere. This sort of hickups are part of the problem space. -- Bernd Paysan "If you want it done right, you have to do it yourself" http://bernd-paysan.de/
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2012-08-29 19:39 -0700 |
| Subject | Re: Function Points |
| Message-ID | <7xzk5dt85u.fsf@ruckus.brouhaha.com> |
| In reply to | #15255 |
Bernd Paysan <bernd.paysan@gmx.de> writes: >>> Coq's proof system is similar to other formal proof systems > ...the systems were formalized before 1930. Coq adds > enough expressive power to its "type" system that it comes under the > same sort of formalized proof systems. Hmm, Coq is really quite a bit different than a Hilbert-style deductive system if that's what you mean. There have been significant mathematical advances in proof theory between the 1920's and now. After Gödel we got Gentzen's sequent calculus (mid 1930's), then the Curry-Howard correspondence (1950's?), then intuitionistic (constructive) type theory (1970's), and Coq is basically an elaboration on that. Girard's book "Proofs and types" that I linked earlier goes into the theory of this, but as mentioned, I haven't read it and it's a bit too technical for me at the moment. >> Compulsive need to turn every possible programming error into >> statically checked type error, consumed my soul > This poor soul should read Gödel's proof of incompleteness, following by > Turing's proof of the unsolvable halting problem as examples that you > simply can't do that - or you are restricting yourself too much. Well of course he was joking, but really, undecidability usually isn't an issue for what he was talking about. Usually when we write a program, we have some hopefully-sound reasoning (usually informal) saying why the program should work as intended. "Proving" is simply a matter of writing the reasoning down, sometimes formally. >>> The specification of the conditions is just as bug-prone > That's a particular odd example, real-world examples are not that odd. We could start with simple conditions like "this subscript will not overflow", "this program will not multiply two pointers together and dereference the result", etc. The red-black tree from earlier is another example. > Of course. Debugging is said to be twice as hard, You know, I think debugging is not as hard as it used to be, mostly because of type safety (including through runtime checks rather than static types). Java code and C++ code are fairly resemblant to each other, and they take about equally long to write, but Java debugging time seems to be much shorter, because when a program goes wrong there is usually an immediate error and stack dump. There's no pointer errors silently corrupting memory, causing difficult debugging sessions. >> It amounts to automated theorem proving. Prolog simply uses >> exponential search with some unreliable heuristics, > Indeed. You shouldn't do non-trivial problems, see above. Eh? Humans are better at reasoning than Prolog is, so it's just a matter of choosing algorithms that you can reason about. >> that knowledge is part of the semantic gap. > The "do what I mean" programming language is yet another problem which > we don't have any idea how to implement it. We don't know how to program "do what I mean". We've always known how to program "do what I say". We're now entering an era where we can program "this is what I mean" in a machine-understandable way, even though we don't expect the computer to automatically turn that meaning into actions. This is new, and it means when we supply the instructions along with the meaning, the computer can now check that carrying out the instructions will lead to the desired end result. It's still highly tedious, but it's one of those things like speech recognition, that was useless a decade or two ago but has been improving steadily since then. > And they curse about that, and the typical reaction to this request is > "the code must be rewritten from scratch, as it is an unmaintainable > mess" :-). Nah, programs have varying amount of cruft in them and sometimes benefit from incremental refactoring, but it's usually possible to make a patch. 5+ years ago someone told me Google's main search application was around 100 MLOC of C++. That's not a candidate for rewriting all at once. People they hire are expected to sit down and deal with the existing code. > about Forth is that the machine responds to the programmer in real > time (i.e. fast enough that the human doesn't have to wait for the > machine). Yeah, that's most helpful in situations where you want to poke at an unfamiliar interface and see how it works. Other situations, it's ok to think for a while, then write code in a text editor, then use a batch compiler. Of course having to wait long periods for results is bad. Compiling speed doesn't always help, if (e.g.) the program takes 2 seconds to compile and overnight to run. Big compute clusters help ;-). > No, random delays are not actually a problem, Haskell is probably workable then. You might also like Erlang, which has Lisp-style runtime typing, and built-in distribution and fault recovery methods.
[toc] | [prev] | [next] | [standalone]
| From | anton@mips.complang.tuwien.ac.at (Anton Ertl) |
|---|---|
| Date | 2012-08-30 14:10 +0000 |
| Subject | Re: Function Points |
| Message-ID | <2012Aug30.161056@mips.complang.tuwien.ac.at> |
| In reply to | #15214 |
Paul Rubin <no.email@nospam.invalid> writes:
>Bernd Paysan <bernd.paysan@gmx.de> writes:
>> Yes, but that's not "right first time". A program is "right first time"
>> if - after internal debugging - it gets out error-free to the customer.
>
>There's another aspect: how do you convince the customer (or anyone
>else) of the absence of errors?
Why should I? Do customers care? They prefer to use (and buy) the
good-enough software that's available now and has some other benefits
(e.g., compatibility, glitz) over supposedly-perfect software that's
available next year and costs a fortune.
Moreover, even with formal methods and whatnot there is no guaranteed
error-free program as far as the custormer is concerned because formal
methods only can show that the code implements the specification, but
not that the specification is correct or that the requirements are
correct.
- anton
--
M. Anton Ertl http://www.complang.tuwien.ac.at/anton/home.html
comp.lang.forth FAQs: http://www.complang.tuwien.ac.at/forth/faq/toc.html
New standard: http://www.forth200x.org/forth200x.html
EuroForth 2012: http://www.euroforth.org/ef12/
[toc] | [prev] | [next] | [standalone]
| From | gavino_himself <visploveslisp@gmail.com> |
|---|---|
| Date | 2012-08-30 20:08 -0700 |
| Subject | Re: Function Points |
| Message-ID | <e12a1875-08bb-4166-ac3b-55361b20c9eb@googlegroups.com> |
| In reply to | #15182 |
On Sunday, August 26, 2012 2:20:15 PM UTC-7, Bernd Paysan wrote:
> Paul Rubin wrote:
>
> > Are you talking about compiling programs of similar size, on similar
>
> > hardware, with compilers that do similar levels of optimization? It's
>
> > certainly plausible that given more CPU power, fancy compilers will
>
> > use it to do more optimization and automation, rather than just doing
>
> > the same stuff as before and finishing sooner.
>
>
>
> No, I'm comparing a bloated Java+C++ project to a non-bloated Forth
>
> project. But even when I compare two non-bloated projects, GCC is
>
> hellish slow.
>
>
>
> > Maybe you should try TCC (tinycc.org) for development builds.
>
> > It's around 10x faster than GCC, though the output code is nowhere
>
> > near as optimized.
>
>
>
> Unfortunately, TCC is also lacking features. And using a different
>
> compiler for debug builds than for production builds is a bad idea - if
>
> you run into bugs of the production build compiler, what do you do then?
>
> The usual Forth approach to coding is making small incremental changes,
>
> because then you don't have to search long for the reasons why it
>
> doesn't work - it's very likely the small change you just did now.
>
>
>
> >> That also guides to my most-used debugging method: Inserting ~~ in
>
> >> suspicious places.
>
> >
>
> > This still takes a lot of runs of the program and possible creation of
>
> > new test cases, which can be pretty tedious.
>
>
>
> Well, it does not feel "a lot" if you can do these runs pretty quickly.
>
>
>
> >>> IMHO Haskell's type system makes it practical to program in a style
>
> >>> that while not impossible, would be much harder to manage in
>
> >>> Forth....
>
> >> I'm not sure why you claim it is error-prone and to be avoided....
>
> >> Forth is a programming language which tells you to avoid unnecessary
>
> >> abstractions.
>
> >
>
> > Right, the reason it tells you to avoid unnecessary abstractions is
>
> > that using abstraction in Forth is error-prone.
>
>
>
> No, that's not the case. You should avoid unnecessary abstractions
>
> since they don't pay off. You can use necessary abstractions, and are
>
> encouraged to do so.
>
>
>
> > I wasn't thinking really
>
> > of postpone and create/does, but more of a style where you pass around
>
> > execution tokens a lot, and those xt's may take other xt's as
>
> > arguments
>
> > to invoke over generic data structures, and so on.
>
>
>
> After I added quotations to my system, I started doing that regularly.
>
> Not exactly as in Haskell, but MINOS, using an OOP system, does that
>
> sort of stuff. Juggling around many things on the stack is bad Forth
>
> code, so pass xts around that take another xts quite likely will result
>
> in many parameters on the stack. Don't do that.
>
>
>
> The OOP system I use in MINOS handles that: You pack the several xts
>
> into one class, and use that. No need for several xts flying around,
>
> the class framework wrap them up into one entity, which is much easier
>
> to pass around.
>
>
>
> > In Haskell, it's
>
> > natural to program that way, and the code still feels solid. In
>
> > Scheme or Python you can write basically the same code, but with no
>
> > type system watching over you, it feels like walking on a tightrope
>
> > without a safety net.
>
>
>
> Don't fear the program crash! As I said, in a strong typed language, I
>
> feel like in a straightjacket. I wouldn't walk a tightrope in such a
>
> language, regardless of safety net or not.
>
>
>
> > I've programmed that way in Forth a little bit, but have been
>
> > advised against it.
>
> >
>
> >> No type system prevents programs from going wrong.
>
> >
>
> > Well, I'd say a well-typed program, including something like Lisp with
>
> > runtime type-checking, can at least have well-defined semantics, while
>
> > an untyped (e.g. Forth or C) program can go completely into the weeds
>
> > if there is a type error (such as a subscript overflow).
>
>
>
> A subscript overflow is not exactly a type error.
>
>
>
> >> It applies a number of low-hanging fruit checks,
>
> >
>
> > Haskell typechecking can be quite powerful. I like this example:
>
> > https://gist.github.com/2659812
>
> >
>
> > Explanation: Red-black trees are binary trees with the following
>
> > invariants:
>
> > 1. Each internal node is colored either red or black.
>
> > All leaves are black and the root is black.
>
> > 2. All children of red nodes must be black. Black nodes can
>
> > have children of either or both colors.
>
> > 3. All paths from the root to the leaf contain the
>
> > same number of black nodes.
>
> >
>
> > This means the tree is approximately balanced: any path from the root
>
> > to a leaf contains n black nodes, and between 0 and n red nodes, so
>
> > the
>
> > worst case search depth is no more than 2x the best case. You can't
>
> > get
>
> > a completely lopsided tree. To insert or delete a node, you have to
>
> > do somewhat complicated juggling operations ("tree rotations") to
>
> > preserve the invariants, and it's easy to make mistakes coding these
>
> > operations. The C++ implementation that I looked at has assert
>
> > statements that check at runtime that the code didn't hit some weird
>
> > edge case that messed the
>
> > invariants up. Even after extensive testing, the assert statements
>
> > are still there in the program.
>
> >
>
> > It turns out to be pretty straightforward to express those invariants
>
> > as
>
> > a Haskell datatype (seen in the url above). Any value belonging to
>
> > the
>
> > type must be a properly balanced tree. That means that the juggling
>
> > code cannot possibly mess up the invariants. Any attempt to make an
>
> > unbalanced tree will cause a type-checking error, and the program
>
> > won't
>
> > compile.
>
>
>
> That's exactly what I don't like. This is a rather complicated thing,
>
> and I'm sure neither of us will write a perfect program first time. As
>
> I try to write incremental programs, my first approach to a r/b tree
>
> would be a general tree program, and let the tree be as unbalanced as I
>
> like. If this works, I would start adding balancing rotation
>
> operations, one after the other (you know, there are several cases you
>
> have to think about). Each of them is tested, but of course, the tree
>
> will still be lopsided.
>
>
>
> Maybe you can do that in Haskell, too, by just trying with the full
>
> blown type, and doing the test runs with a reduced type information,
>
> which doesn't care about balancing.
>
>
>
> > It would be pointless to have assert statements in the
>
> > executable since the compiler has statically verified that the
>
> > asserted
>
> > conditions hold. I would not call this low-hanging fruit. It's a
>
> > sophisticated condition being checked, that's a source of bugs in
>
> > other real-world implementations, and the compiler verifies it to
>
> > higher confidence than even quite a lot of unit tests could give.
>
> >
>
> > As an even more extreme example, Coq's type system is even stronger
>
> > than Haskell's: it can express any mathematical proposition, so it has
>
> > to be Turing complete, meaning it can't do inference and you have to
>
> > manually
>
> > supply type derivations (which is tedious). But it can encode (for
>
> > example) the semantics of assembly code fragments (Hoare triples) as
>
> > types. So if you have a compiler optimization pass that is annotated
>
> > to take one fragment and returns another fragment of the same type,
>
> > the Coq typechecker is able to verify that the input and output have
>
> > the same semantics and the optimization pass has not introduced any
>
> > semantic
>
> > bugs. I think I mentioned before, a sizable part of a C compiler has
>
> > been written that way (CompCert). This is not low hanging fruit at
>
> > all. It is probably the future, especially as better automation
>
> > becomes available for developing this sort of code.
>
>
>
> Calling this still a "type system" is a misnomer. Yes, this is no low-
>
> hanging fruit, but as you said, it is also tedious to use. And if
>
> that's useful during development depends on the error message. Let's
>
> say I have a code transformation pattern
>
>
>
> BEGIN code WHILE REPEAT -> BEGIN code UNTIL
>
>
>
> to skip the empty part between WHILE and REPEAT, the transformation is
>
> wrong, because the flag for WHILE means the opposit as for UNTIL. If
>
> the code system tells me just "your transformation is wrong", then I
>
> have no clue why, and can only guess. If I unit-test this thing, I'd
>
> give it a simple task and look at the results, and since the results are
>
> runable programs, I'll see why the two are different.
>
>
>
> >> while at the same time putting a straitjacket onto the programmer.
>
> >> At least that's how I feel when I program in a language with a strong
>
> >> type system. The compiler tells me "no, you can't do this", and "no,
>
> >> you can't do that".
>
> >
>
> > I never felt terribly straitjacketed programming in C, but I also felt
>
> > that the type system wasn't helping me that much.
>
>
>
> C has no really strong type system. A type mismatch usually results in
>
> a warning, it doesn't even fail to compile. I'm not that much
>
> complaining about C, C's type system is more a simple operator
>
> overloading system than anything else.
>
>
>
> > I was comfortable
>
> > programming with lots of void*'s, and programming in Lisp with runtime
>
> > types. Trying Haskell was really eye-opening for me. I'm a long way
>
> > from being a Haskell expert but I find it tremendously interesting and
>
> > different (whether that means "better" is of course a separate
>
> > matter).
>
>
>
> Yes, of course. It is quit different.
>
>
>
> >>> http://cdsmith.wordpress.com/2011/01/09/an-old-article-i-wrote/
>
> >> Performance is not a problem? Come on. I'm constantly seeing
>
> >> software which is slow as molasses,
>
> >
>
> > He's talking about compiled code with runtime type checks, vs.
>
> > compiled code that has been statically checked but otherwise does the
>
> > same stuff,
>
> > e.g. Lisp vs ML. If the compiler is any good, the performance
>
> > difference is usually a small constant factor, maybe just a few
>
> > percent. The large, order-of-magnitude slowdowns you're seeing in the
>
> > examples you mention are due to architectural issues in the slow
>
> > programs.
>
>
>
> Yes. Usually several architectural issues stacked on each others, like
>
> using a complicated delegate-style OOP program (nobody really wants to
>
> solve the problem, so it gets delegated over and over again) on top of a
>
> slow Java VM with a bad JIT - if there is a JIT at all.
>
>
>
> >> What I think would be worth to do for analytic compilers which track
>
> >> that information anyways: Have a stack effect checker.
>
> >
>
> > Yes, that would have caught my + vs. F+ bugs. StrongForth does
>
> > that sort of checking as you're probably aware.
>
>
>
> It does a bit more, and there's even a version which runs on top of
>
> Gforth.
>
>
>
> >> Warnings when it doesn't match, please, it should compile, because
>
> >> running it (with inserted ~~) will identify the problem quickly.
>
> >
>
> > GHC now has a command-line option that lets it produce executable code
>
> > even if the program has type errors. You then get a runtime error
>
> > only
>
> > if the program tries to actually evaluate an ill-typed expression.
>
>
>
> Nice. This allows you to check what actually happens.
>
>
>
> > This turns out to be handy during development even though the compiler
>
> > has
>
> > already told you where the errors are. It's sometimes useful to be
>
> > able test the successfully compiling parts of your program right away,
>
> > postponing dealing with the unsuccessful parts til later.
>
>
>
> Given that fact, I'm less opposed than before. How useful is GHCi (the
>
> interactive command line)?
>
>
>
> >> Forth's interactivity and abstraction avoidance is what makes it
>
> >> strong. Interactivity is more than just a command line promt, it
>
> >> also
>
> >> means that you can recompile quickly. "Blink", not "lunch".
>
> >
>
> > I sometimes like to imagine what it must have been like to program in
>
> > Forth or Lisp in the glory days of those languages. I'd be interested
>
> > in seeing a demo sometime (maybe on video) of someone hacking on Forth
>
> > code that does something complicated, using good interactive Forth
>
> > tools.
>
>
>
> We Forthers really try hard to not do something complicated ;-). When I
>
> implemented bigForth' fast dictionary search, I explored several
>
> options, hashing and AVL trees. AVL trees were more complicated, and
>
> they lost to hashing in every metric: Time to write, execution
>
> performance, memory usage, and bugs to fix during development.
>
>
>
> In many cases you have an option which is simple, fast, and correct.
>
> Don't try to use the other option.
>
>
>
> > When I started using Python, I found myself thinking "this is
>
> > what the old-time Maclisp hackers must have felt like". Haskell is
>
> > different, completely different, a vision as powerful as Lisp but
>
> > unlike
>
> > anything that had been used for programming before. That in some
>
> > sense outweighs any difficulties involved in trying to actually use
>
> > it. ;-)
>
>
>
> I'm still wondering how useful that would be for me. The main
>
> challanges in the programs I write are the outside world, not the inner
>
> logic of the program. E.g. take my net2o flow control, which took me
>
> quite some time to develop. The code for it is rather simple, and it
>
> always was rather simple, didn't crash or anything. That's not the
>
> challange. The challange is to fill a network with packets just fast
>
> enough, so they don't pile up in buffers, but yet leave no unused
>
> bandwidth under real world conditions, which means things like Wifi with
>
> rapidly changing quality, competing with multiple TCP/IP, BitTorrent or
>
> net2o itself. This was a serious issue which I underestimated, given
>
> how bold other people were about their results (like LEDBAT). I thought
>
> I could just copy that, but it turned out to be not good enough.
>
>
>
> A type system won't help at all here. The type system will catch the
>
> low hanging fruits like f+ vs. + or similar. I don't have problems with
>
> those, these are "declinations", and something the human brain can
>
> handle quite well (the grammar engine).
>
>
>
> --
>
> Bernd Paysan
>
> "If you want it done right, you have to do it yourself"
>
> http://bernd-paysan.de/
How do you know which abstractions are needed and which are not?
Is the lisp and haskell claim that abstraction is most important hollow?
Are abstractions not needed many times?
[toc] | [prev] | [next] | [standalone]
| From | "Elizabeth D. Rather" <erather@forth.com> |
|---|---|
| Date | 2012-08-30 17:47 -1000 |
| Subject | Re: Function Points |
| Message-ID | <M-ednY4VNdtVrt3NnZ2dnUVZ_q-dnZ2d@supernews.com> |
| In reply to | #15287 |
On 8/30/12 5:08 PM, gavino_himself wrote: ... > How do you know which abstractions are needed and which are not? > Is the lisp and haskell claim that abstraction is most important hollow? > Are abstractions not needed many times? > It all depends on the needs of the application. Some applications benefit more from abstractions than others. Cheers, Elizabeth -- ================================================== Elizabeth D. Rather (US & Canada) 800-55-FORTH FORTH Inc. +1 310.999.6784 5959 West Century Blvd. Suite 700 Los Angeles, CA 90045 http://www.forth.com "Forth-based products and Services for real-time applications since 1973." ==================================================
[toc] | [prev] | [next] | [standalone]
| From | "Elizabeth D. Rather" <erather@forth.com> |
|---|---|
| Date | 2012-08-27 13:43 -1000 |
| Subject | Re: Function Points |
| Message-ID | <AOqdneJFnpqkm6HNnZ2dnUVZ_oydnZ2d@supernews.com> |
| In reply to | #15166 |
On 8/25/12 7:44 PM, Paul Rubin wrote: ... >>> IMHO Haskell's type system makes it practical to program in a style >>> that while not impossible, would be much harder to manage in Forth.... >> I'm not sure why you claim it is error-prone and to be avoided.... >> Forth is a programming language which tells you to avoid unnecessary >> abstractions. > > Right, the reason it tells you to avoid unnecessary abstractions is that > using abstraction in Forth is error-prone. I wasn't thinking really of > postpone and create/does, but more of a style where you pass around > execution tokens a lot, and those xt's may take other xt's as arguments > to invoke over generic data structures, and so on. In Haskell, it's > natural to program that way, and the code still feels solid. In Scheme > or Python you can write basically the same code, but with no type system > watching over you, it feels like walking on a tightrope without a safety > net. I've programmed that way in Forth a little bit, but have been > advised against it. I meant to comment on this last week, but got distracted. I don't like "a style where you pass around execution tokens a lot, and those xt's may take other xt's as arguments to invoke over generic data structures, and so on" but my reasons have nothing to do with data types or type checking, pro or con. It's just not a natural style for Forth. Most of the time, words are to be called, not treated as data. To be sure, there are times when explicit use of an xt is appropriate (with CATCH, with DEFERs, and in indexable tables of function pointers, mainly), but those are very specific application needs. The examples of that sort of thing I've seen posted here all strike me as wildly unreadable and unnecessarily obscure, and usually quite inefficient. Cheers, Elizabeth -- ================================================== Elizabeth D. Rather (US & Canada) 800-55-FORTH FORTH Inc. +1 310.999.6784 5959 West Century Blvd. Suite 700 Los Angeles, CA 90045 http://www.forth.com "Forth-based products and Services for real-time applications since 1973." ==================================================
[toc] | [prev] | [next] | [standalone]
| From | "Paul E. Bennett" <Paul_E.Bennett@topmail.co.uk> |
|---|---|
| Date | 2012-08-27 12:14 +0100 |
| Subject | Re: Function Points |
| Message-ID | <aa135hF50vU1@mid.individual.net> |
| In reply to | #15160 |
Elizabeth D. Rather wrote: [%X] >> Anyway, if a type-checked language lets me write a page full of code and >> fix the compile-time errors to usually get working program, while the >> typeless counterpart makes me stop what I'm doing after basically every >> single line to check for problems the type checker would have caught >> automatically, I'd say the type checker has made itself worthwhile. > > Unit-testing every definition pays off handsomely in saved debugging > time by catching all kinds of bugs, not just type errors. > > And my experience is similar to Anton's, in that I make very few type > errors. This may be because I'm accustomed to matching the right > operators to the right data type, whereas folks who are used to > languages that do type inference are less conscious of it. But the > majority of errors (not only for me but for programmers I work with) are > logic/algorithm errors, and they're readily detected by unit testing > each definition. Takes seconds, can save hours! Writing a whole page of code at a time just has the wrong feel to doing the job right. Concentrate on the correctness of one function at a time, review the intent (as expressed in the glossary text you wrote to specify what was to happen) and test each word as you complete it (ensuring it meets the specification of the glossary). On this basis I built the techniques for certification of Forth code to ensure compliance with specification. No real hunting required for the hidden bugs as you should expunge them as you go to ensure they are not introduced in the first place. Of course, you need to really concentrate on getting the specification right first. -- ******************************************************************** Paul E. Bennett...............<email://Paul_E.Bennett@topmail.co.uk> Forth based HIDECS Consultancy Mob: +44 (0)7811-639972 Tel: +44 (0)1235-510979 Going Forth Safely ..... EBA. www.electric-boat-association.org.uk.. ********************************************************************
[toc] | [prev] | [next] | [standalone]
| From | Mark Wills <markrobertwills@yahoo.co.uk> |
|---|---|
| Date | 2012-08-27 05:12 -0700 |
| Subject | Re: Function Points |
| Message-ID | <86b6066f-415d-4632-a8d3-3fbc28ab01ba@n9g2000yqn.googlegroups.com> |
| In reply to | #15189 |
On Aug 27, 12:14 pm, "Paul E. Bennett" <Paul_E.Benn...@topmail.co.uk> wrote: > Elizabeth D. Rather wrote: > > [%X] > > > > > > >> Anyway, if a type-checked language lets me write a page full of code and > >> fix the compile-time errors to usually get working program, while the > >> typeless counterpart makes me stop what I'm doing after basically every > >> single line to check for problems the type checker would have caught > >> automatically, I'd say the type checker has made itself worthwhile. > > > Unit-testing every definition pays off handsomely in saved debugging > > time by catching all kinds of bugs, not just type errors. > > > And my experience is similar to Anton's, in that I make very few type > > errors. This may be because I'm accustomed to matching the right > > operators to the right data type, whereas folks who are used to > > languages that do type inference are less conscious of it. But the > > majority of errors (not only for me but for programmers I work with) are > > logic/algorithm errors, and they're readily detected by unit testing > > each definition. Takes seconds, can save hours! > > Writing a whole page of code at a time just has the wrong feel to doing the > job right. Concentrate on the correctness of one function at a time, review > the intent (as expressed in the glossary text you wrote to specify what was > to happen) and test each word as you complete it (ensuring it meets the > specification of the glossary). On this basis I built the techniques for > certification of Forth code to ensure compliance with specification. No real > hunting required for the hidden bugs as you should expunge them as you go to > ensure they are not introduced in the first place. Of course, you need to > really concentrate on getting the specification right first. > > -- > ******************************************************************** > Paul E. Bennett...............<email://Paul_E.Benn...@topmail.co.uk> > Forth based HIDECS Consultancy > Mob: +44 (0)7811-639972 > Tel: +44 (0)1235-510979 > Going Forth Safely ..... EBA.www.electric-boat-association.org.uk.. > ********************************************************************- Hide quoted text - > > - Show quoted text - Agreed. And you also have to accept that you can't get your documentation 100% perfect up-front. It's just a fact of life that you'll discover something during the physical implementation that may require you to add a new function (perhaps to handle an unanticipated exception, for example) that will require you to re-vist and update your documentation. It's not Necessarily a design failure. It's just reality! We spend weeks working on up-front software documentation. Working in the mission-critical oil and gas business, it's just a normal part of the design process. We're pretty good at it (we can design to SIL-1 on our in-house designed and manufactured controllers) but we still come across issues that we failed to anticipate, despite numerous peer reviews and design reviews! They're never show-stoppers, but there's always a gotcha lurking in there somewhere!
[toc] | [prev] | [next] | [standalone]
| From | "Paul E. Bennett" <Paul_E.Bennett@topmail.co.uk> |
|---|---|
| Date | 2012-08-27 15:52 +0100 |
| Subject | Re: Function Points |
| Message-ID | <aa1fv9F6tvU1@mid.individual.net> |
| In reply to | #15191 |
Mark Wills wrote: [%X] >> Writing a whole page of code at a time just has the wrong feel to doing >> the job right. Concentrate on the correctness of one function at a time, >> review the intent (as expressed in the glossary text you wrote to specify >> what was to happen) and test each word as you complete it (ensuring it >> meets the specification of the glossary). On this basis I built the >> techniques for certification of Forth code to ensure compliance with >> specification. No real hunting required for the hidden bugs as you should >> expunge them as you go to ensure they are not introduced in the first >> place. Of course, you need to really concentrate on getting the >> specification right first. > Agreed. And you also have to accept that you can't get your > documentation 100% perfect up-front. It's just a fact of life that > you'll discover something during the physical implementation that may > require you to add a new function (perhaps to handle an unanticipated > exception, for example) that will require you to re-vist and update > your documentation. This is so true too. I estimate that you will probably visit each part of the system 3 times during development (especially working on critical systems). > It's not Necessarily a design failure. It's just reality! > > We spend weeks working on up-front software documentation. Working in > the mission-critical oil and gas business, it's just a normal part of > the design process. Do you have a good grasp of the total concept at that time or is the specification still a collection of "I would like" type items? I have seen many organisations that do the up-front documentation on half baked design specs that still have lots of un-answered questions. The trick is usually to be a lot clearer about the full explicit requirements that will mean mission success early enough, even if all the fine details haven't yet emerged. This may take a number of review sessions that truly walk the problem space before the design really begins. > We're pretty good at it (we can design to SIL-1 on > our in-house designed and manufactured controllers) but we still come > across issues that we failed to anticipate, despite numerous peer > reviews and design reviews! They're never show-stoppers, but there's > always a gotcha lurking in there somewhere! There is no reason why you shouldn't deal with SIL-3 or SIL-4 requirements if you are able to improve your early design and development processes. Eliminate the systematic bugs before they get into the system design and you save a lot of time, effort and money in the later stages. -- ******************************************************************** Paul E. Bennett...............<email://Paul_E.Bennett@topmail.co.uk> Forth based HIDECS Consultancy Mob: +44 (0)7811-639972 Tel: +44 (0)1235-510979 Going Forth Safely ..... EBA. www.electric-boat-association.org.uk.. ********************************************************************
[toc] | [prev] | [next] | [standalone]
| From | anton@mips.complang.tuwien.ac.at (Anton Ertl) |
|---|---|
| Date | 2012-08-26 13:09 +0000 |
| Subject | Re: Function Points |
| Message-ID | <2012Aug26.150931@mips.complang.tuwien.ac.at> |
| In reply to | #15159 |
Paul Rubin <no.email@nospam.invalid> writes:
>Doug Hoffman <glidedog@gmail.com> writes:
>> If you are writing short, factored words, and testing each word before
>> continuing then that "+ instead of F+" should have become immediately
>> apparent and so no problem at all to notice and fix. No type checker
>> needed if you follow the recommended Forth way of writing a program.
>
>As I remember, it wasn't so immediately apparent what the problem was,
>since the failure didn't occur til a little ways after the + happened.
>And the symptom was that the program crashed without much clue about
>what had happened. Of course fancy debugging tools would have made it
>easier to trace and fix the problem, and it's not inherent in Forth that
>the implementation I used didn't happen to have them.
In my experience such a basic error as writing a + where there should
be an F+ shows up really quick, but maybe I avoid writing code where
it would not show up quickly.
Concerning fancy tools, I use the ~~ tracer (a more convenient variant
of what C programmers call printf debugging), and Gforth has
backtraces to let you know where an error happened. Some people like
a stepping debugger, but in my experience it's a good recipe for
wasting time. A back-stepping debugger with reverse watchpoints, now
that would be useful; apparently newer versions of gdb have that, but
I have not found the need for that yet.
>Anyway, if a type-checked language lets me write a page full of code and
>fix the compile-time errors to usually get working program, while the
>typeless counterpart makes me stop what I'm doing after basically every
>single line to check for problems the type checker would have caught
>automatically, I'd say the type checker has made itself worthwhile.
Why would I stop after every line? I typically write code until I
think it's time to test and debug, and then I start to test and debug.
While testing and debugging, it helps to have short words that can be
called individually.
- anton
--
M. Anton Ertl http://www.complang.tuwien.ac.at/anton/home.html
comp.lang.forth FAQs: http://www.complang.tuwien.ac.at/forth/faq/toc.html
New standard: http://www.forth200x.org/forth200x.html
EuroForth 2012: http://www.euroforth.org/ef12/
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2012-08-27 20:52 -0700 |
| Subject | Re: Function Points |
| Message-ID | <7xbohvy8pc.fsf@ruckus.brouhaha.com> |
| In reply to | #15176 |
anton@mips.complang.tuwien.ac.at (Anton Ertl) writes: > In my experience such a basic error as writing a + where there should > be an F+ shows up really quick, but maybe I avoid writing code where > it would not show up quickly. I think it took a while for me to debug because I hadn't yet gotten used to hitting that kind of error. > Some people like a stepping debugger, but in my experience it's a good > recipe for wasting time. A back-stepping debugger with reverse > watchpoints, now that would be useful I find single stepping to be very helpful. I haven't tried a back-stepping debugger but I can remember having wanted such a thing. > Why would I stop after every line? Other people on this newsgroup have been advising me to test each word before writing the next one. Most of my words are 1 line. Yeah in practice I tend to write several words before testing. It's certainly seems true that testing in very small units helps quickly narrow what part of the code is probably going wrong. Better diagnostics make that narrowing less important, so I can code and test larger units, speeding up development.
[toc] | [prev] | [next] | [standalone]
| From | anton@mips.complang.tuwien.ac.at (Anton Ertl) |
|---|---|
| Date | 2012-08-30 14:08 +0000 |
| Subject | Re: Function Points |
| Message-ID | <2012Aug30.160847@mips.complang.tuwien.ac.at> |
| In reply to | #15215 |
Paul Rubin <no.email@nospam.invalid> writes:
>anton@mips.complang.tuwien.ac.at (Anton Ertl) writes:
>> Why would I stop after every line?
>
>Other people on this newsgroup have been advising me to test each word
>before writing the next one. Most of my words are 1 line.
And what benefit would a stepping debugger have in that scenario?
- anton
--
M. Anton Ertl http://www.complang.tuwien.ac.at/anton/home.html
comp.lang.forth FAQs: http://www.complang.tuwien.ac.at/forth/faq/toc.html
New standard: http://www.forth200x.org/forth200x.html
EuroForth 2012: http://www.euroforth.org/ef12/
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2012-08-30 10:43 -0700 |
| Subject | Re: Function Points |
| Message-ID | <7xmx1cmg1t.fsf@ruckus.brouhaha.com> |
| In reply to | #15267 |
anton@mips.complang.tuwien.ac.at (Anton Ertl) writes: >> Most of my words are 1 line. > And what benefit would a stepping debugger have in that scenario? Eh? It's very helpful to execute one step at a time to see where the word is going wrong, e.g. with a conditional breakpoint in a loop (~~ can spew too much output), examining variables (not just the stack) during execution, etc. >>There's another aspect: how do you convince the customer (or anyone >>else) of the absence of errors? >Why should I? Do customers care? 1) Besides customers you may also have to convince your co-workers (code review) and yourself. It's certainly common enough (at least for me) to write some code, test it and see that it seems to work, but be left with doubts that my testing may have missed an obscure case. 2) Yes customers do care. I worked on a financial product and customers (banks) did technical audits on us several times, particularly on our security stuff. They asked what we did to prevent various specific failures and we had to answer convincingly. I'm not saying static types would have helped the above cases all that much, but it tells me that incorporating reasoning about correctness into programs is a sensible aspirational goal. > Moreover, even with formal methods and whatnot there is no guaranteed > error-free program ... because formal methods only can show that the > code implements the specification, but not that the specification is > correct or that the requirements are correct. Sure, but that's mostly a red herring. Of course it's near-impossible to write a spec that captures ALL the desired behavior of a program. Type systems instead let you assert the absence of specific incorrect behaviors, which still helps a lot. "This program must never dereference a null pointer for any input" is simple enough to specify and easy for a reasonable type system to ensure, but decades of C program failures show it's very hard to supply by pure design and testing. Thus the saying "the last good thing written in C was Schubert's Ninth Symphony". ;-). > I have never implemented a balanced tree... For every potential use I > have encountered there has been a less complex and usually more > efficient data structure (usually a hash table). They're useful and I keep wanting them in Python. They let you access (i.e. add, delete, lookup) arbitrary keys, and also traverse the keys in order. A real-world example where I wanted this is a priority queue where you can update elements (think of an alarm clock with N updateable alarms). Databases are another frequent application (B-trees). Balanced trees also guarantee O(log n) access and update, which stops some real-world denial of service attacks that have happened in internet programs, based on triggering hash collisions on purpose. And, persistent versions make it easy to take snapshots as updates happen, which is handy in concurrent programs among other places. > So, the example illustrates that Haskell's type system may help me > with a problem that I have never encountered. Not very convincing as > far as real-world usage is concerned. The example gets categorized as > "cool, but useless". I thought it was amazing how easy it was to write a type signature that captured the red-black tree invariants. I don't have a sense of how hard it was for that guy to write the code that went with the signature. It might have actually been too difficult for everyday programming. It still seems significant as an example of emerging technology not quite ready for prime time, in addition to being cool.
[toc] | [prev] | [next] | [standalone]
| From | "Elizabeth D. Rather" <erather@forth.com> |
|---|---|
| Date | 2012-08-30 08:25 -1000 |
| Subject | Re: Function Points |
| Message-ID | <spGdnZyKIo2aLaLNnZ2dnUVZ_qidnZ2d@supernews.com> |
| In reply to | #15273 |
On 8/30/12 7:43 AM, Paul Rubin wrote: > anton@mips.complang.tuwien.ac.at (Anton Ertl) writes: >>> Most of my words are 1 line. >> And what benefit would a stepping debugger have in that scenario? > > Eh? It's very helpful to execute one step at a time to see where the > word is going wrong, e.g. with a conditional breakpoint in a loop (~~ > can spew too much output), examining variables (not just the stack) > during execution, etc. Ok, we're talking about debugging a 1-line (or very short) definition. Here's how I do it: 1. Test it by giving it reasonable inputs and examining the outputs. 2. If it gives a wrong answer, error message, or other indication of trouble, I look at it. Since it is very small, usually the error becomes apparent, so I fix it and repeat #1. 3. In the rare case when the error is still elusive, I type through the definition, looking at the stack. If there's a loop, I type through the body of the loop (remember, this is a 1-line definition!). A very common source of trouble is stack overflow or underflow in a loop; this will reveal what's happening. 4. When the definition appears to work, I write a test word that takes it through a reasonable range of input values and run that. Now, obviously when there is hardware involved the method differs. I always test the hardware first, which in Forth you can do interactively with little or no actual code. Examine ports using C@ (or a custom P@ if code is required to read a port), write to control or data registers using C! or P!, to prove that the device responds appropriately. Then I test the code using the 4 steps above, supplying reasonably dummy data. Then I put it all together. This is all preliminary testing at low levels of an application, of course. As the application develops, similar procedures apply to higher level processes. >>> There's another aspect: how do you convince the customer (or anyone >>> else) of the absence of errors? >> Why should I? Do customers care? > > 1) Besides customers you may also have to convince your co-workers (code > review) and yourself. It's certainly common enough (at least for me) to > write some code, test it and see that it seems to work, but be left with > doubts that my testing may have missed an obscure case. > > 2) Yes customers do care. I worked on a financial product and customers > (banks) did technical audits on us several times, particularly on our > security stuff. They asked what we did to prevent various specific > failures and we had to answer convincingly. I'm thinking of all the tales we hear about versions of Windows and other big programs released with upwards of 100,000 known bugs! But, for sure there are applications where you really do need a high degree of confidence in the correctness of the code. Paul Bennett (a clf regular) has written some papers on certifying Forth programs. What you need in these cases are well-designed, thorough test suites to apply to major sections of the program, and the program overall. > I'm not saying static types would have helped the above cases all that > much, but it tells me that incorporating reasoning about correctness > into programs is a sensible aspirational goal. Absolutely, "incorporating reasoning about correctness into programs is a sensible aspirational goal." But type checking has little to do with this. Of all the major programs I've been involved in developing and testing, errors of type have simply not been issues for which elaborate type checking compilers would be any help. That kind of check may be appropriate in a programming style that involves pages of code, but not short Forth definitions. ... >> I have never implemented a balanced tree... For every potential use I >> have encountered there has been a less complex and usually more >> efficient data structure (usually a hash table). > > They're useful and I keep wanting them in Python. They let you access > (i.e. add, delete, lookup) arbitrary keys, and also traverse the keys in > order. A real-world example where I wanted this is a priority queue > where you can update elements (think of an alarm clock with N updateable > alarms). Databases are another frequent application (B-trees). > Balanced trees also guarantee O(log n) access and update, which stops > some real-world denial of service attacks that have happened in internet > programs, based on triggering hash collisions on purpose. And, > persistent versions make it easy to take snapshots as updates happen, > which is handy in concurrent programs among other places. The database system in polyFORTH had a B-tree option for a while. I can remember one application in which it was useful. But I think of things like that as library functions that may be appropriate in certain applications, not language features. Cheers, Elizabeth -- ================================================== Elizabeth D. Rather (US & Canada) 800-55-FORTH FORTH Inc. +1 310.999.6784 5959 West Century Blvd. Suite 700 Los Angeles, CA 90045 http://www.forth.com "Forth-based products and Services for real-time applications since 1973." ==================================================
[toc] | [prev] | [next] | [standalone]
| From | Bernd Paysan <bernd.paysan@gmx.de> |
|---|---|
| Date | 2012-08-30 22:42 +0200 |
| Subject | Re: Function Points |
| Message-ID | <2250796.QNINORRiYk@sunwukong.fritz.box> |
| In reply to | #15273 |
Paul Rubin wrote: >> Moreover, even with formal methods and whatnot there is no guaranteed >> error-free program ... because formal methods only can show that the >> code implements the specification, but not that the specification is >> correct or that the requirements are correct. > > Sure, but that's mostly a red herring. Of course it's near-impossible > to write a spec that captures ALL the desired behavior of a program. No, the real world fact is that it is near-impossible to write a spec that is even close to what the customer really wants - other than in "do what I mean" notation. E.g. the project I worked on two years ago was a battery monitor, and the customer wanted things like "accurate to about 1%" and "below 10µA current budget", "smaller number is better". Yes, the latter is partly a software requirement, as this thing was running on a b16 processor, and the current consumption can go up to milliamps if the CPU runs all the time at high clock speed. > Type systems instead let you assert the absence of specific incorrect > behaviors, which still helps a lot. "This program must never > dereference a null pointer for any input" is simple enough to specify > and easy for a reasonable type system to ensure, but decades of C > program failures show it's very hard to supply by pure design and > testing. Thus the saying "the last good thing written in C was > Schubert's Ninth Symphony". ;-). But C's main problem is one fundamental mistake: buffers are passed around as pointers, without length. This is a direct invitation to buffer overflows. The problem of C is not just a lack of type information, it is the lack of a very vital information: the lack of knowing how big a buffer actually is. Forth doesn't know about types, but its buffer operations all know about the size of the buffer. >> I have never implemented a balanced tree... For every potential use I >> have encountered there has been a less complex and usually more >> efficient data structure (usually a hash table). > > They're useful and I keep wanting them in Python. They let you access > (i.e. add, delete, lookup) arbitrary keys, and also traverse the keys > in order. In what order? Alphabetical order? Does that matter? Do you really want all fruits from apples to bananas listed? We use alphabetical orders to quickly index things, like a dictionary or an address book. > A real-world example where I wanted this is a priority queue > where you can update elements (think of an alarm clock with N > updateable alarms). Yes, that is an example where you have an order over the entries which actually matters. > Databases are another frequent application (B-trees). Database implementers like B-trees particularly, because they can easily be made transaction-safe. I.e. when you do a transaction, you copy the parts of the tree which contain the new state, and then you only update the root pointer - or, when you have to unroll your transaction, you just throw away these copies. As databases often have several indices per table, transactions have to update all of them, and this should not be costly. > Balanced trees also guarantee O(log n) access and update, which stops > some real-world denial of service attacks that have happened in > internet programs, based on triggering hash collisions on purpose. The other way to deal with that problem is to have a unique hash function, which the attacker can't create hash collisions for (for being "unique", something quite simple is completely sufficient: xor all strings with the same secret). For me, this sort of B-trees or priority queues are problems which you face during university, because they are popular data structures. In "real life", they don't happen that often. If you really need them, you write them once, and then they are part of your toolbox. The priority queue I wrote (for MINOS) didn't get a complicated data structure, because the usual case is that there aren't many events waiting. Therefore, just having an array and direct insert was both the quickest to write *and* the most performant. It is O(n), but the constant overhead is very low. I've made some thought about how I would implement the priority queue of a gate-level simulator, and my preferred data structure would be an array with a fixed time scale, because each element has a delay (e.g. at least an inverter delay), so if your fixed time scale is less than the minimum delay, you can perform the operations in arbitrary order (no finer grain for sorting needed). So in reality, you quite often have opportunities to slightly change the requirements so that you can use a much easier solution. With the "constant time scale per schedule bucket = minimum delay" equation mentioned above, I'd be curious how that would look in Coq. It's provable, the proof is that whatever data you update, the next update it triggers must not go to the same bucket, because execution inside the same bucket is not ordered. That's stuff I think you can reason about without writing down much stuff, but making it formal so that an assisted proof system like Coq can proof you do meet the requirements of a full-blown priority queue under these constraints: I think that's pretty hard. After all, the delay data is not part of the program, you read in the delay annotations, extract the minimum delay, and use that value as scheduler bucket delta-t. -- Bernd Paysan "If you want it done right, you have to do it yourself" http://bernd-paysan.de/
[toc] | [prev] | [next] | [standalone]
| From | "Rod Pemberton" <do_not_have@notemailnot.cmm> |
|---|---|
| Date | 2012-08-31 01:23 -0400 |
| Subject | Re: Function Points |
| Message-ID | <k1phj0$lr8$1@speranza.aioe.org> |
| In reply to | #15280 |
"Bernd Paysan" <bernd.paysan@gmx.de> wrote in message news:2250796.QNINORRiYk@sunwukong.fritz.box... [...] > But C's main problem is one fundamental mistake: buffers are passed > around as pointers, without length. If you knew anything about C, you'd know that the length of a buffer is always known. It's either in the declaration of the buffer, or was needed to allocate the buffer dynamicly, or is available with sizeof() or strlen() etc. Whether or not the length is available when needed is a programmer implementation issue. > This is a direct invitation to buffer overflows. That doesn't follow. C's buffer overflows are the result of: 1) unlimited keyboard input functions 2) delimited buffers without the required delimiter 3) abuse of the single stack (common, not required) used for control-flow, parameters, and data How is Forth any different? C doesn't require a stack, but most use one in order to: a) implement recursion of procedures b) reduce memory allocation requirements > The problem of C is not just a lack of type information, it is > the lack of a very vital information: the lack of knowing how > big a buffer actually is. > Example 1) - static allocation #define BSIZ 32 char buf[BSIZ]; len0=BSIZ; len1=sizeof(buf); Example 2) - dynamic allocation #define BSIZ 32 char str[]="ABCDEF"; len0=BSIZ; malloc(len0); len1=80*sizeof(char); malloc(len1); len2=10*strlen(str); malloc(len2); The length is needed to allocate a buffer, staticly or dynamicly. The length is known from then on, or can be determined by using the appropriate function or size operator. > Forth doesn't know about types, but its buffer operations > all know about the size of the buffer. Which "buffer operations" in C don't? The few memory functions in C operate on any data and are passed a length. Their data is not delimited. So, they require a length. The many string functions in C operate on strings, which in C is an array of characters delimited by C's definition of a byte, set to all bits cleared (zero). Other C string functions operate on strings delimited by other characters. > The other way to deal with that problem is to have a unique hash > function, which the attacker can't create hash collisions for (for being > "unique", something quite simple is completely sufficient: xor all > strings with the same secret). There is no guarantee that for two non-XOR'd strings which are hash collisions that their two XOR'd strings won't be hash collisions also. If the hash function has low collisions, then it's unlikely the XOR'd strings will collide, but that's also true for the non-XOR'd strings. If the hash function has high collisions (for simplicity, or speed etc.), then it's likely the XOR'd strings will collide too, but that's also true for the non-XOR'd strings. Even with a low collision hash function, I think the idea of XOR-ing is a bad idea. For a set of non-XOR'd strings, collisions will occur for certain strings. With a set of XOR'd strings, collisions will occur for certain strings too. I.e., the probability or frequency of collisions is the same. The XOR has no effect on that probability. The hash function hasn't changed. A certain percentage will collide. So, all I believe XOR-ing will do is change which inputs collide, but it won't reduce the frequency of the collisions. If this works for you, it's because the strings are limited in the numeric range of their characters, and you've shifted which hash collisions occur via the use of XOR-ing "secret" string. The reason why I think this is a bad idea is because you've effectively tuned the hash to produce low collisions for a _specific_ set of input strings and a _specific_ "secret" string. However, both that input set of strings and "secret" string can be changed. If they are changed, the hash needs to be retuned. What needs to be done instead of XOR-ing is to increase the randomness of the string data. String data has a narrow numeric range of values. An array of randomized data with a larger range than the character range can be used to translate the the strings' characters to the random data prior to the hash. Rod Pemberton
[toc] | [prev] | [next] | [standalone]
| From | Andrew Haley <andrew29@littlepinkcloud.invalid> |
|---|---|
| Date | 2012-08-31 03:08 -0500 |
| Subject | Re: Function Points |
| Message-ID | <b-mdnS3hM6567d3NnZ2dnUVZ8midnZ2d@supernews.com> |
| In reply to | #15294 |
Rod Pemberton <do_not_have@notemailnot.cmm> wrote: > "Bernd Paysan" <bernd.paysan@gmx.de> wrote in message > news:2250796.QNINORRiYk@sunwukong.fritz.box... > > [...] > >> But C's main problem is one fundamental mistake: buffers are passed >> around as pointers, without length. > > If you knew anything about C, you'd know that the length of a buffer > is always known. It's either in the declaration of the buffer, or > was needed to allocate the buffer dynamicly, or is available with > sizeof() or strlen() etc. Whether or not the length is available > when needed is a programmer implementation issue. Well, yes. It's the "programmer implementation issue" that Bernd is talking about. It's the fact that if someone passes you an int[] you can't say "How big is this?" Yes, you can insist that they also pass you the size, but that doesn't change the fact that the language doesn't. >> The other way to deal with that problem is to have a unique hash >> function, which the attacker can't create hash collisions for (for being >> "unique", something quite simple is completely sufficient: xor all >> strings with the same secret). > > There is no guarantee that for two non-XOR'd strings which are hash > collisions that their two XOR'd strings won't be hash collisions > also. If the hash function has low collisions, then it's unlikely > the XOR'd strings will collide, but that's also true for the > non-XOR'd strings. You're missing the point. The idea of the unique hash function is not to make collisions impossible but to make them unpredictable: the scenario is one where the attacker knows the hash function and deliberately creates collisions. Andrew.
[toc] | [prev] | [next] | [standalone]
Page 3 of 9 — ← Prev page 1 2 [3] 4 5 6 7 8 9 Next page →
Back to top | Article view | comp.lang.forth
csiph-web