Marcel Hendrix <mhx@iae.nl> writes:
>Ok, can we at least ask that the prover processes its own source code
>with positive results?

Unlikely, at least in full; you probably run into one of Goedel's
incompleteness theorems or something similar. You can probably have
the prover prove properties of most of its code, but there will be a
part P that is beyond its capabilities. In theory it's possible to
write a more complex prover that can prove that part, but then how do
you prove that prover? A more practical approach is to prove P
manually.

- 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 2021: https://euro.theforth.net/2021

"minf...@arcor.de" <minforth@arcor.de> writes:
>"Unfortunately" Forth is type-free and any cell can be used or abused to any
>clever trick or even mayhem. But it would still be a correct Forth program.
>IIUC provers wouldn't help much unless one puts a lot of restrictions (contracts)
>on Forth.

A prover proves a property of the program, and you have to specify the
property. E.g., for a sorting program you (at least) specify that the
output contains all the same element as the input, and that they are
sorted. Whether the compiler or run-time system knows about type
probably has little effect at that point.

- 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 2021: https://euro.theforth.net/2021

anton@mips.complang.tuwien.ac.at (Anton Ertl) writes:
> Concerning libraries, you don't need big companies for that, as Python
> demonstrates. But you need a community and system implementors that
> want libraries, understand what features are needed for libraries, and
> are willing to add the features that are needed for libraries.

Yes. Also, Python quickly added a number of "programming in the large"
features (modules, __init__.py, etc.) which made it very clear and easy
to add chunks of functionality.

A single standard CPython provided a common target for those efforts.

Andy Valencia
Home page: https://www.vsta.org/andy/
To contact me: https://www.vsta.org/contact/andy.html

anton@mips.complang.tuwien.ac.at (Anton Ertl) writes:
> Unlikely, at least in full; you probably run into one of Goedel's
> incompleteness theorems or something similar. You can probably have
> the prover prove properties of most of its code, but there will be a
> part P that is beyond its capabilities.

Another approach, used by Microsoft's SPEC prover, is to notice that
Goedel's theorem only applies to theories strong enough to support a
fragment of arithmetic that includes addition and multiplication, since
you need both of those to create the self-referential Goedel sentence.

If you drop multiplication so your arithmetic only supports addition,
you get a weaker theory called Presburger arithmetic, to which Goedel's
theorem doesn't apply, and in fact your prover can work automatically as
long as your program never multiplies two variables together.
(Multiplication a variable by a constant doesn't "count", since it can
be formalized as repeated addition. So that handles most array
subscripting.)

You usually wouldn't use SPEC on an entire program. It is instead used
mostly (I believe, I've never looked at it) to verify that some chunk of
code is free of buffer overflow bugs.

> In theory it's possible to write a more complex prover that can prove
> that part, but then how do you prove that prover? A more practical
> approach is to prove P manually.

Making sure P is small enough to validate by inspection is called the de
Bruijn criterion. Another approach, used by HOL Light, is to use the
same prover, but make its theory more powerful by adding an extra axiom.
That lets the version with the extra axiom check the consistency of the
version without it.

HOL Light is based on set theory (so called Zermelo set theory Z if that
matters), and the extra axiom asserts the exitence of a so-called
inaccessible cardinal in Z. This is a so-called large cardinal axiom,
which even mathematicians (other than set theorists) consider to be one
of the most abstruse and useless topics in mathematics. Yet there it
is, being used in a practical piece of software (HOL Light is used to
verify some things about Intel microprocessors, iirc).

It is worse. What if HOL Light's implementation of Z is inconsistent,
due to a bug or because Z itself is inconsistent? Can't it prove its
own consistency already then? A consistent theory (per Goedel) can't do
that, but of course an inconsistent theory can prove anything, even
2+2=5. And if HOL Light starts out inconsistent, it's still
inconsistent with the new axiom.

But, the idea is that such an self-consistency proof would be very weird
and roundabout, and the proof with the inaccessible cardinal likely
wouldn't go through. That is mathematically unrigorous, but it doesn't
seem worse than the horrible things that electrical engineers have
always done with complex numbers, so we can let it by.

So there you have an *engineering* use of a large cardinal (it's not a
valid mathematical use because of the non-rigor). From a certain
perspective, that is utterly amazing. There was a mathematician named
Solomon Feferman who believed that all the mathematics used in science,
and even almost all of pure mathematics, could be handled with fairly
weak axioms. I wanted to ask him about this large cardinal example but
unfortunately he died a few years ago, before I could do so. He was
mathematically active into his 80's though.

Paul Rubin schrieb am Mittwoch, 29. Dezember 2021 um 22:12:42 UTC+1:
> But, the idea is that such an self-consistency proof would be very weird
> and roundabout, and the proof with the inaccessible cardinal likely
> wouldn't go through. That is mathematically unrigorous, but it doesn't
> seem worse than the horrible things that electrical engineers have
> always done with complex numbers, so we can let it by.

LOL!!! How gracious of you! :-)

Engineers pollute the Platonic world of numbers, geometries, algebras
and mathematical relations by abusing them for earthly matters! Bah!!

Make Forth a finite state machine without side effects! It will eat energy
without increasing information entropy (just thermal entropy by heat loss).
Much neater.

"minf...@arcor.de" <minforth@arcor.de> writes:
> Engineers pollute the Platonic world of numbers, geometries, algebras
> and mathematical relations by abusing them for earthly matters! Bah!!

Nah, I just mean mathematicians have a pretty hardcore notion of what it
means to prove a theorem. Engineers and scientists tend to be more
pragmatic about it, and many physics "theorems" aren't really
mathematically sound even though they seem to work in practice.
Like I remember a proof of the Cauchy integral theorem from physics
class, and it made sense for well behaved curves, but would break down
for messy (e.g. fractal-like) curves that physicists didn't care about.

In fancier physics, it's even worse. Mathematicians still apparently
have quite a lot of trouble formalizing quantum field theory, for
example. A math prof once told me that QFT as done by physicists
involves finding an infinite series some of whose terms are themselves
infinite, ignoring those terms, and adding up the rest. That gives
astoundingly accurate answers that can be verified by experiment, but is
mathematically "lolwut".

There are various mathematical attempts to fix this but all are pretty
painful, from what I gather.

On Wednesday, December 29, 2021 at 10:12:42 PM UTC+1, Paul Rubin wrote:
> That is mathematically unrigorous, but it doesn't
> seem worse than the horrible things that electrical engineers have
> always done with complex numbers, so we can let it by.

I'm interested, please tell! (I've used them as size-2 double arrays
but survived.)

-marcel

On 30/12/2021 04:55, Andy Valencia wrote:
> anton@mips.complang.tuwien.ac.at (Anton Ertl) writes:
>> Concerning libraries, you don't need big companies for that, as Python
>> demonstrates. But you need a community and system implementors that
>> want libraries, understand what features are needed for libraries, and
>> are willing to add the features that are needed for libraries.
>
> Yes. Also, Python quickly added a number of "programming in the large"
> features (modules, __init__.py, etc.) which made it very clear and easy
> to add chunks of functionality.
>
> A single standard CPython provided a common target for those efforts.

Also I expect Python isn't a federation of implementers where each wants
to 'have their cake and eat it too'. There are no political compromises
to slow development or muddy the language. Developers might even have a
common understanding of what Python is and what it's about. Where users
are given exactly two choices 'take it or leave it'. Can't speak for
others but I find no appeal in being held to ransom or living out my days
a second-hand person fulfilling someone else's dream.

On Wednesday, December 29, 2021 at 9:45:06 AM UTC-7, Anton Ertl wrote:
> dxforth <dxf...@gmail.com> writes:
> >You say Forth lacks ready-to-use libraries. If they've not materialized
> >with what's been added thus far, then what
> ...
> Ideally time-travel back to the 1980s, spread these ideas, get them in
> the '94 standard, and a community will grow around it that builds the
> libraries. Instead, we lost many so-minded people to other languages,
> resulting in a Forth community where many (not all) have an
> anti-library sentiment.

It is certainly true that Elizabeth Rather has an anti-library sentiment,
and all ANS-Forth cult members are required to also hate libraries.

Anton wants to spread these ideas (libraries).
His problem is that he doesn't know how to implement a general-purpose
data-structure. None of the Forth-200x committee members know how to do this.
Peter Knaggs failed badly at implementing a linked-list, which is pretty easy.
https://groups.google.com/g/comp.lang.forth/c/cMa8wV3OiY0/m/INBDVBh0BgAJ

The Forth-200x committee has banned my rquotations, which work well for
implementing general-purpose data-structures. There are two possible reasons:
1.) They are just too dumb to understand the concept.
2.) They wanted a dumbed-down worthless version of quotations to be standard
in Forth-200x so Stephen Pelc could "invent" rquotations as a proprietary VFX feature.

The #2 explanation assumes that the goal of the Forth-200x committee is not to
provide the Forth community with a viable Forth standard that multiple Forth
compiler-writers could adhere to, but rather to help Stephen Pelc make money
by forcing the Forth community into a false dichotomy of either VFX ($$$)
or a free pile of garbage (Forth-200x). This #2 explanation seems to be the most
likely, considering that Stephen Pelc is the chair-person of the Forth-200x committee.

I said this previously:
On Monday, December 27, 2021 at 7:34:17 PM UTC-7, Hugh Aguilar wrote:
> The purpose of the rquotations is to support general-purpose data-structures.
> The idea is to have a HOF that traverses the data-structure executing the
> rquotation for every node. The rquotation communicates information back to
> the parent function that called the HOF by modifying the parent function's
> local variables.
>
> In the novice-package I had pseudo-quotations, (called "touchers" in my documentation
> because I didn't know the word "pseudo-quotation" at the time. These were just colon words.
> I expected the HOF to not have any data on the data-stack at the time that the
> pseudo-quotation was executed. This is the pseudo-quotation could communicate information
> back to the parent function that called the HOF by modifying the parent function's
> data on the data-stack (also, the pseudo-quotation could communicate information
> back to the parent function in global variables). This is a very kludgy work-around for
> ANS-Forth's lack of rquotations that allow information to be communicated back to the
> parent function via the parent function's local variables. When I wrote the rquotations
> (an upgrade on HumptyDumpty's prototype that lacked the crucial feature) this really
> made pseudo-quotations obsolete. Rquotations are a major break-through for Forth.
>
> The Forth-200x committee has standardized the Paysan-faked quotations that are just
> syntactic sugar for pseudo-quotations (they use :NONAME rather than colon to provide
> a cute but fake quotation-like syntax, but they lack the functionality of rquotations).
> The Forth-200x committee deserves to be completely discredited and disbanded
> for standardizing the Paysan-faked quotations --- this is like spray-painting
> a brick with gold paint, and then claiming that it is a solid-gold brick.
> This is disgraceful fakery! The Forth-200x committee don't deserve to be forgiven.

On Thursday, December 30, 2021 at 6:12:43 AM UTC+3, dxforth wrote:
> On 30/12/2021 04:55, Andy Valencia wrote:
> > an...@mips.complang.tuwien.ac.at (Anton Ertl) writes:
> >> Concerning libraries, you don't need big companies for that, as Python
> >> demonstrates. But you need a community and system implementors that
> >> want libraries, understand what features are needed for libraries, and
> >> are willing to add the features that are needed for libraries.
> >
> > Yes. Also, Python quickly added a number of "programming in the large"
> > features (modules, __init__.py, etc.) which made it very clear and easy
> > to add chunks of functionality.
> >
> > A single standard CPython provided a common target for those efforts.
> Also I expect Python isn't a federation of implementers where each wants
> to 'have their cake and eat it too'. There are no political compromises
> to slow development or muddy the language. Developers might even have a
> common understanding of what Python is and what it's about. Where users
> are given exactly two choices 'take it or leave it'. Can't speak for
> others but I find no appeal in being held to ransom or living out my days
> a second-hand person fulfilling someone else's dream.

https://www.python.org/dev/peps/pep-0001/

dxforth <dxforth@gmail.com> writes:
> Also I expect Python isn't a federation of implementers where each wants
> to 'have their cake and eat it too'.

Since that's human nature, I expect it was _a_ factor which was present.

One of the greatest strengths of Python--especially in its formative
years--was the unique personality of Guido van Rossum. A fair portion of
Python's "secret sauce" is how Guido was able to guide the overall community,
and hold it together.

Andy Valencia
Home page: https://www.vsta.org/andy/
To contact me: https://www.vsta.org/contact/andy.html

Nickolay Kolchin <nbkolchin@gmail.com> writes:
> full featured OS are unable to handle modern realtime requirements. I.e.
> microsecond precision

Yeah if your application needs that, you have to offload it to a
coprocessor or FPGA. But really, that's a niche within a niche. MCU's
contain hardware UARTs, PWM, maybe ADC SARs, etc. that manage those
fast operations that might have been done in software back in the day.
The Beaglebone Black chip also has a pair of realtime coprocessors (200
mhz 32 bit RTU's), and the Raspberry Pi Pico has those PIO units, though
the Pico doesn't run a heavyweight OS.

> P.S. But we kinda moved away from Forth again.

Yeah, as for "future Forth", I don't think Python-like Forths have much
attraction. Maybe of more interest is tethered Forths that move the
text interpreter to a remote host, instead of just using a serial port
and resident interpreter. This is already done with the professional
Forths but I'd like to see it in hobbyist Forths. There should also be
some modifications to e.g. DOES> to be friendlier for target cpus with
program memory in flash instead of ram.

This was also of interest: https://queue.acm.org/detail.cfm?id=3212479

It says that the old flat-memory single-threaded cpu abstraction no
longer really reflects the hardware. So maybe it's best to e.g. get rid
of the cache hierarchy and explicitly expose multiple levels of slower
and faster memory. If that results in new kinds of cpus, maybe Forth
could be suitable for them.

On Tuesday, December 21, 2021 at 6:05:06 PM UTC+1, minf...@arcor.de wrote:
> 2) ISO/ANS Forth with little progress and barely usable for real world apps
> 3) hundreds of personal/hobby/academic Forths or VMs, often severely
> crippled and unmaintained

That's because it's extremely easy to make a Forth compiler - but quite a steep path in learning how to program it. After having played with the toy, kids gets bored. That's how it is.
Still, I don't think 2) and 3) are true categories - since lots of "hobby" Forths adhere to the standard.

> Ad 2) and 3) There seems a tendency towards permanently reinventing
> or retuning old wheels. Hence no progress there as well.
I don't agree here as well. Know that there are TWO Forth's: the architecture and the language. NASA still uses the Forth architecture in some of their development systems. Factor is my no means Forth language-wise, but it uses its architecture. Even ColorForth is more of an architecture descendant than a language one. So don't say architecture wise there are no developments.

Forths "standards" have always been problematic IMHO and while ANS did clear up the sky a bit, I think Forth 20xx is AGAIN a step in the wrong direction. It adds the same "pragmatic" constraints to the language that e.g. Forth-83 did, doesn't fill the gaps that need to be filled (stringwise, anybody?) and adds wordsets which universal usefulness is at least questionable.

Coming from C, I've never questioned the usefulness of libraries in general.. It's true that you can make several variants - depending on certain requirements like speed, compactness or features - but that doesn't mean you have to reinvent the wheel each and every time. I learned quite a few things from Chuck, but here I do absolutely not agree. And I've found no circumstances in which I had to change my mind in that regard. Most often than not - if it happened, I merely added another library to the arsenal.

Like C, it is hard to distinguish the extensions to the language from the language itself. My own C-libraries need an inclusion of the prototypes and are linked in a similar fashion. Forth is the same thing. Every Forth compiler has at least some "extra" words attached to it. When talking about the "core" words, I don't think you've seen much development in C during that period as well. Even more, I think - even when comparing just the years '70-'90 - Forth has seen much more development - CELLS, CHAR+, ?DO, CASE..ENDCASE, just to name a few. Add [: and ;] for good measure.

And then: the rebels. The ones that do *NOT* adhere (completely) to the standard. I could name a few offhand like oForth, StrongForth, 8th and even Factor. It's not *TOO* hard so add at least some Factor features to ordinary Forth. 4tH has proven that in the recent release of v3.64.0. All of these variants carried some concepts that are compatible with Forth; or - like 8th.. oForth or Factor - a complete reimagining of Forth.

I do agree that some of these variants have not been maintained for long, but that doesn't mean they're incomplete - and hence unusable. Excuse me if I'm making errors here (I apologize beforehand), but often there has been little or no activity - for reasons unknown. It could be that the writers consider their tools "rounded" and "ready for use" and are still using it for their own development. We don't know.

Lots of people here maintain their own compilers. I can't speak for them, of course. If they still use it for their own development, let them speak up.. I can only speak for myself. I developed 4tH almost 30 years ago - and development is still ongoing. My last commit was a week ago. In the meanwhile I'm also maintaining 500+ libraries, quietly doing "drop in replacements" when need be. Since I've developed 4tH, I've hardly used C - except for maintaining the compiler itself.

Speaking of that compiler, it doesn't follow the Forth architecture - at all. The support for tables is unique, as is its I/O system. It has a preprocessor, which allows for a unique OOP model called FOOS. It has abstracted the STRING wordset, since it uses ASCIIZ strings internally. It has a complete set of string words - the entire preprocessor was built in 4tH - what more proof do you need? You can write Jason, LateX, HTML, XLS and even RTF. It features libraries to read CSV and XML. So yes, I wrote and write "real world" applications in 4tH - both personally and professionally. A lot of them are still used every day. And I'm not alone. I know for sure my highly regarded confrere Aaron who wrote 8th can sing a similar song.

I suppose you can only see what you want to see - but IMHO there are and have been numerous developments in Forth. And yes, people are still developing in Forth. I just wish we would see more useful stuff presented here - and if people do, they would help to improve these instead of playing the "standard Nazis", taking away all the fun in publishing stuff here in the first place. And another big tip: if you don't like locals, prove you can write a better one without these pesky things instead of starting to whine. People do that all the time in Rosetta Code.

Hans Bezemer

Marcel Hendrix <mhx@iae.nl> writes:
>I just found a bug in a program and your comment sparks interest.
>
>The bug was in a floating-point equivalent of /mod, i.e.
>
>FP/REM "f-p-slash-rem"
> ( F: x y -- rem[x/y] ) ( -- q[x/y] )
> Compute the remainder r and divisor q of x divided by y.
> When y is not 0, the remainder rem is defined regardless of the
> current rounding mode by the exact mathematical relation
> r = x - y * q, where q is the integer nearest the exact
> number x/y, with round to nearest.
>
>: test 20e-6 2e-6 FP/REM . e. 10e 2e-6 F* 2e-6 FP/REM . e. ; ok
>test 10 1.240771e-24 10 2.000000e-6 ok
>
>How would one use SPARK to usefully catch such a problem?

And the problem is? I don't think SPARK can catch anything if you
don't tell it in another way what your intention is.

I find the example interesting: 20e-6 seems to be quite close to ten
times 2e-6, so the remainder is small. By contrast, 2e-6 should be
the same as 2e-6, and 10e is representable exactly, and F* should
introduce only a small rounding error, so I would expect that the
remainder is small in that case, too.

Let's see:

Gforth 0.7.9_20211216 (same with 0.7.3):
20e-6 10e 2e-6 f* f- fs. \ output: 3.38813178901720E-21

iForth 5.1-mini:
FORTH> 20e-6 10e 2e-6 f* f- fs. \ 1.654361e-24 ok

Looks ok (better accuracy thanks to 80-bit floats). So the problem
seems to lie with FP/REM.

vfx64 5.11 RC2:
20e-6 10e 2e-6 f* f- fs. \ 0.0000000e+00

- 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 2021: https://euro.theforth.net/2021

the.bee...@gmail.com schrieb am Donnerstag, 30. Dezember 2021 um 18:00:23 UTC+1:
> On Tuesday, December 21, 2021 at 6:05:06 PM UTC+1, minf...@arcor.de wrote:
> > 2) ISO/ANS Forth with little progress and barely usable for real world apps
> > 3) hundreds of personal/hobby/academic Forths or VMs, often severely
> > crippled and unmaintained
>
> That's because it's extremely easy to make a Forth compiler - but quite a steep path in learning how to program it. After having played with the toy, kids gets bored. That's how it is.
> Still, I don't think 2) and 3) are true categories - since lots of "hobby" Forths adhere to the standard.
>
> > Ad 2) and 3) There seems a tendency towards permanently reinventing
> > or retuning old wheels. Hence no progress there as well.
> I don't agree here as well. Know that there are TWO Forth's: the architecture and the language. NASA still uses the Forth architecture in some of their development systems. Factor is my no means Forth language-wise, but it uses its architecture. Even ColorForth is more of an architecture descendant than a language one. So don't say architecture wise there are no developments.
>
> Forths "standards" have always been problematic IMHO and while ANS did clear up the sky a bit, I think Forth 20xx is AGAIN a step in the wrong direction. It adds the same "pragmatic" constraints to the language that e.g. Forth-83 did, doesn't fill the gaps that need to be filled (stringwise, anybody?) and adds wordsets which universal usefulness is at least questionable.
>
> Coming from C, I've never questioned the usefulness of libraries in general. It's true that you can make several variants - depending on certain requirements like speed, compactness or features - but that doesn't mean you have to reinvent the wheel each and every time. I learned quite a few things from Chuck, but here I do absolutely not agree. And I've found no circumstances in which I had to change my mind in that regard. Most often than not - if it happened, I merely added another library to the arsenal.
>
> Like C, it is hard to distinguish the extensions to the language from the language itself. My own C-libraries need an inclusion of the prototypes and are linked in a similar fashion. Forth is the same thing. Every Forth compiler has at least some "extra" words attached to it. When talking about the "core" words, I don't think you've seen much development in C during that period as well. Even more, I think - even when comparing just the years '70-'90 - Forth has seen much more development - CELLS, CHAR+, ?DO, CASE..ENDCASE, just to name a few. Add [: and ;] for good measure.
>
> And then: the rebels. The ones that do *NOT* adhere (completely) to the standard. I could name a few offhand like oForth, StrongForth, 8th and even Factor. It's not *TOO* hard so add at least some Factor features to ordinary Forth. 4tH has proven that in the recent release of v3.64.0. All of these variants carried some concepts that are compatible with Forth; or - like 8th. oForth or Factor - a complete reimagining of Forth.
>
> I do agree that some of these variants have not been maintained for long, but that doesn't mean they're incomplete - and hence unusable. Excuse me if I'm making errors here (I apologize beforehand), but often there has been little or no activity - for reasons unknown. It could be that the writers consider their tools "rounded" and "ready for use" and are still using it for their own development. We don't know.
>
> Lots of people here maintain their own compilers. I can't speak for them, of course. If they still use it for their own development, let them speak up. I can only speak for myself. I developed 4tH almost 30 years ago - and development is still ongoing. My last commit was a week ago. In the meanwhile I'm also maintaining 500+ libraries, quietly doing "drop in replacements" when need be. Since I've developed 4tH, I've hardly used C - except for maintaining the compiler itself.
>
> Speaking of that compiler, it doesn't follow the Forth architecture - at all. The support for tables is unique, as is its I/O system. It has a preprocessor, which allows for a unique OOP model called FOOS. It has abstracted the STRING wordset, since it uses ASCIIZ strings internally. It has a complete set of string words - the entire preprocessor was built in 4tH - what more proof do you need? You can write Jason, LateX, HTML, XLS and even RTF. It features libraries to read CSV and XML. So yes, I wrote and write "real world" applications in 4tH - both personally and professionally. A lot of them are still used every day. And I'm not alone. I know for sure my highly regarded confrere Aaron who wrote 8th can sing a similar song.
>
> I suppose you can only see what you want to see - but IMHO there are and have been numerous developments in Forth. And yes, people are still developing in Forth. I just wish we would see more useful stuff presented here - and if people do, they would help to improve these instead of playing the "standard Nazis", taking away all the fun in publishing stuff here in the first place. And another big tip: if you don't like locals, prove you can write a better one without these pesky things instead of starting to whine. People do that all the time in Rosetta Code.
>

With all due respect, I really don't see how the development of numerous new,
but among themselves incompatible, dialects can contribute to modernizing
Forth. Of course exploring new concepts is the way to go for Occam's razor test,
but incompatible and thus unsharable libraries are a dead end IMO.

BTW I use Forth locals a lot... ;-)

On Thursday, December 30, 2021 at 11:02:03 PM UTC+1, minf...@arcor.de wrote:
> the.bee...@gmail.com schrieb am Donnerstag, 30. Dezember 2021 um 18:00:23 UTC+1:
> > On Tuesday, December 21, 2021 at 6:05:06 PM UTC+1, minf...@arcor.de wrote:
> > > 2) ISO/ANS Forth with little progress and barely usable for real world apps
> > > 3) hundreds of personal/hobby/academic Forths or VMs, often severely
> > > crippled and unmaintained
> >
> > That's because it's extremely easy to make a Forth compiler - but quite a steep path in learning how to program it. After having played with the toy, kids gets bored. That's how it is.
> > Still, I don't think 2) and 3) are true categories - since lots of "hobby" Forths adhere to the standard.
> >
> > > Ad 2) and 3) There seems a tendency towards permanently reinventing
> > > or retuning old wheels. Hence no progress there as well.
> > I don't agree here as well. Know that there are TWO Forth's: the architecture and the language. NASA still uses the Forth architecture in some of their development systems. Factor is my no means Forth language-wise, but it uses its architecture. Even ColorForth is more of an architecture descendant than a language one. So don't say architecture wise there are no developments.
> >
> > Forths "standards" have always been problematic IMHO and while ANS did clear up the sky a bit, I think Forth 20xx is AGAIN a step in the wrong direction. It adds the same "pragmatic" constraints to the language that e.g. Forth-83 did, doesn't fill the gaps that need to be filled (stringwise, anybody?) and adds wordsets which universal usefulness is at least questionable.
> >
> > Coming from C, I've never questioned the usefulness of libraries in general. It's true that you can make several variants - depending on certain requirements like speed, compactness or features - but that doesn't mean you have to reinvent the wheel each and every time. I learned quite a few things from Chuck, but here I do absolutely not agree. And I've found no circumstances in which I had to change my mind in that regard. Most often than not - if it happened, I merely added another library to the arsenal.
> >
> > Like C, it is hard to distinguish the extensions to the language from the language itself. My own C-libraries need an inclusion of the prototypes and are linked in a similar fashion. Forth is the same thing. Every Forth compiler has at least some "extra" words attached to it. When talking about the "core" words, I don't think you've seen much development in C during that period as well. Even more, I think - even when comparing just the years '70-'90 - Forth has seen much more development - CELLS, CHAR+, ?DO, CASE..ENDCASE, just to name a few. Add [: and ;] for good measure.
> >
> > And then: the rebels. The ones that do *NOT* adhere (completely) to the standard. I could name a few offhand like oForth, StrongForth, 8th and even Factor. It's not *TOO* hard so add at least some Factor features to ordinary Forth. 4tH has proven that in the recent release of v3.64.0. All of these variants carried some concepts that are compatible with Forth; or - like 8th. oForth or Factor - a complete reimagining of Forth.
> >
> > I do agree that some of these variants have not been maintained for long, but that doesn't mean they're incomplete - and hence unusable. Excuse me if I'm making errors here (I apologize beforehand), but often there has been little or no activity - for reasons unknown. It could be that the writers consider their tools "rounded" and "ready for use" and are still using it for their own development. We don't know.
> >
> > Lots of people here maintain their own compilers. I can't speak for them, of course. If they still use it for their own development, let them speak up. I can only speak for myself. I developed 4tH almost 30 years ago - and development is still ongoing. My last commit was a week ago. In the meanwhile I'm also maintaining 500+ libraries, quietly doing "drop in replacements" when need be. Since I've developed 4tH, I've hardly used C - except for maintaining the compiler itself.
> >
> > Speaking of that compiler, it doesn't follow the Forth architecture - at all. The support for tables is unique, as is its I/O system. It has a preprocessor, which allows for a unique OOP model called FOOS. It has abstracted the STRING wordset, since it uses ASCIIZ strings internally. It has a complete set of string words - the entire preprocessor was built in 4tH - what more proof do you need? You can write Jason, LateX, HTML, XLS and even RTF. It features libraries to read CSV and XML. So yes, I wrote and write "real world" applications in 4tH - both personally and professionally. A lot of them are still used every day. And I'm not alone. I know for sure my highly regarded confrere Aaron who wrote 8th can sing a similar song.
> >
> > I suppose you can only see what you want to see - but IMHO there are and have been numerous developments in Forth. And yes, people are still developing in Forth. I just wish we would see more useful stuff presented here - and if people do, they would help to improve these instead of playing the "standard Nazis", taking away all the fun in publishing stuff here in the first place. And another big tip: if you don't like locals, prove you can write a better one without these pesky things instead of starting to whine. People do that all the time in Rosetta Code.
> >
> With all due respect, I really don't see how the development of numerous new,
> but among themselves incompatible, dialects can contribute to modernizing
> Forth. Of course exploring new concepts is the way to go for Occam's razor test,
> but incompatible and thus unsharable libraries are a dead end IMO.
>
> BTW I use Forth locals a lot... ;-)

With all due respect, I think that attitude is EXACTLY the problem here. First of all, it's all whining why there are "no new Forth concepts being developed" and then when numerous new concpts are presented the ugly head of the "Standards Nazi" pops up again (used as ametaphor - nothing personal).

New concepts are by definition "non-standard" - because they are NEW. They are here to be explored. As I did when I added two Factor like libraries to 4tH. And you know what? As I had handcoded some primitives, some Factor definitions could be added verbatim. And stuff started to look more and more like Factor.

Exploring takes effort. It doesn't come for free. And may be you don't really like it. I didn't find wrapping my head around nested quotations easier than vanilla Forth - agreed. It didn't make me embrace Factor in any way, although I still think the concept has merit. But at least I didn't discard it with the cheap excuse that it is "non-standard".

If we, as a community keep denying that there are new concepts being developed - while there most certainly are - then we won't have no new conepts. None are published, none are posted - why should one even try - and none are explored and none are discussed. We as a community will cease to exist due to our own conservatism.

And there is plenty to do. We need a complete string wordset. We need to replace some ugly C-isms like the FILE wordset. We could set the first step towards an OO wordset. We could explore alternatives to locals (another horrible C-ism). AND THERE ARE!

All that as alternative to our endless and rather fruitless complaining. At least it confirms to me why I do not do any effort anymore.

Hans Bezemer

On 31/12/2021 11:00, Hans Bezemer wrote:
> ...
> All that as alternative to our endless and rather fruitless complaining. At least it
> confirms to me why I do not do any effort anymore.

Forth and rhetoric about what it should be go together like dogs and fleas.
A little flea powder is all one needs.

On Friday, December 31, 2021 at 1:00:49 AM UTC+1, the.bee...@gmail.com wrote:
[..]
> And there is plenty to do. We need a complete string wordset.
> We need to replace some ugly C-isms like the FILE wordset.
> We could set the first step towards an OO wordset. We could
> explore alternatives to locals (another horrible C-ism).
> AND THERE ARE!

Actually, I don't understand the need. Is there a program
we can't express in Forth? If there is, "we need" to do
something indeed.

Although we can express all possible programs in Forth,
some may 1. want to express them *differently,* or 2. add
additional *programmer* requirements, e.g. introspection,
debugging, garbage collecting, etc.. In Forth we can do 1
by extending the language *and still call it Forth*,
something which all interpreted languages can do (but
AFAIK, not as efficiently as Forth).

It is possible to start with Forth and implement 1 and 2
by taking shortcuts, resulting in the numerous more or
less useful Forth mongrels. To be able to still officially
call these Forth, inconsistencies and bottlenecks in the
basic language specification must be tracked down
and fixed. This is what IMO the various standardization
efforts are about.

Of course people will argue that a 'Fixed Forth' is not
the real thing anymore. It is 'Standard Forth,' though.

In what I quoted above there is nothing problematic as
long as the laundry list is implemented in Standard
Forth. IMHO it is just a complaint that some
programmer has to do himself what he thinks
(FFL and FSL?) noone has already done for him.

-marcel

Marcel Hendrix <mhx@iae.nl> writes:
> Although we can express all possible programs in Forth,

If you mean all possible computations (the Turing completeness fallacy)
then sure. For some other things the language facilities actually
matter. The following is afaict impossible in Forth, C, Python etc.,;
difficult but possible in C++ or Java, a little bit clumsy in Haskell,
and probably quite easy in Agda or Idris. It requires making use of a
static type system, so languages without static types don't meet the
entry requirement. I've only done it in Haskell:

http://blog.tmorris.net/posts/understanding-practical-api-design-static-typing-and-functional-programming/

On Friday, December 31, 2021 at 10:51:20 AM UTC+1, Paul Rubin wrote:
> Marcel Hendrix <m...@iae.nl> writes:
> > Although we can express all possible programs in Forth,
> If you mean all possible computations (the Turing completeness fallacy)
> then sure. For some other things the language facilities actually
> matter. The following is afaict impossible in Forth, C, Python etc.,;
> difficult but possible in C++ or Java, a little bit clumsy in Haskell,
> and probably quite easy in Agda or Idris. It requires making use of a
> static type system, so languages without static types don't meet the
> entry requirement. I've only done it in Haskell:
>
> http://blog.tmorris.net/posts/understanding-practical-api-design-static-typing-and-functional-programming/

It is necessary to be precise ...

Are you saying that it is impossible to implement "what static
typing does" (focusing here on your concrete statement) for a fully
specified program (like that Tic-Tac-Toe API example)? I think that
we have to be extra precise here because an API allows to write
quite a lot of unknown programs. I would prefer to take *one
specific* program produced with the API and see if it could be
written in Forth (in order to prevent moving the goal posts at
infinitum).

If you state that "static typing is necessary" I would be
interested to know how you are going to test if static
typing actually works as intended for a concrete
example that can not be reproduced with a Forth
program taking the aforementioned input for the test :--)

-marcel

On Friday, December 31, 2021 at 9:51:26 AM UTC+1, Marcel Hendrix wrote:
> On Friday, December 31, 2021 at 1:00:49 AM UTC+1, the.bee...@gmail.com wrote:
> [..]
> > And there is plenty to do. We need a complete string wordset.
> > We need to replace some ugly C-isms like the FILE wordset.
> > We could set the first step towards an OO wordset. We could
> > explore alternatives to locals (another horrible C-ism).
> > AND THERE ARE!
> Actually, I don't understand the need. Is there a program
> we can't express in Forth? If there is, "we need" to do
> something indeed.
>
> Although we can express all possible programs in Forth,
> some may 1. want to express them *differently,* or 2. add
> additional *programmer* requirements, e.g. introspection,
> debugging, garbage collecting, etc.. In Forth we can do 1
> by extending the language *and still call it Forth*,
> something which all interpreted languages can do (but
> AFAIK, not as efficiently as Forth).
>
> It is possible to start with Forth and implement 1 and 2
> by taking shortcuts, resulting in the numerous more or
> less useful Forth mongrels. To be able to still officially
> call these Forth, inconsistencies and bottlenecks in the
> basic language specification must be tracked down
> and fixed. This is what IMO the various standardization
> efforts are about.
>
> Of course people will argue that a 'Fixed Forth' is not
> the real thing anymore. It is 'Standard Forth,' though.
>
> In what I quoted above there is nothing problematic as
> long as the laundry list is implemented in Standard
> Forth. IMHO it is just a complaint that some
> programmer has to do himself what he thinks
> (FFL and FSL?) noone has already done for him.
>
> -marcel
Try implementing 4tH's IO scheme in standard Forth. Good luck. Implementing Forths FILE wordset in 4tH is trivial, however. Just a bunch of oneliners.

Hans Bezemer

Paul Rubin <no.email@nospam.invalid> writes:
>http://blog.tmorris.net/posts/understanding-practical-api-design-static-typing-and-functional-programming/

He does not show his solution, but given that even tic-tac-toe is too
complex to make a complete manual static expansion practical, I expect
that his move and take-move-back words return one of the following
subtypes of a board-state type:

board-finished
board-empty
board-next-x
board-next-o

And then he uses enforced run-time guarding to guarantee that control
flow never reaches the words unless the type is correct. I.e.,

empty-board (board-empty) 1 1 x-move ( board ) 0 0 o-move

would result in a type error at the second move, because move just
returns the board supertype, but not one of the types that MOVE
accepts. You would have to do something along the lines of

empty-board (board-empty) 1 1 x-move ( board )
dup is-board-next-o if
0 0 o-move then

instead. That did not come out clear in this posting (I only figured
it out afterwards, and I guess those who have not come into contact
with type guards do not figure it out at all), and he did not give a
convincing (to me) reason why a programmer would want to comply with
his rules.

Anyway, about doing that in Forth: One could put the words in separate
wordlists (with each wordlist representing a type), and then have
words that do the type-guarding and wordlist lookup. Something like
having o-move in the board-next-o wordlist, and having a guarding
word, used like this:

( board ) 0 0 rot guard-board-next-o o-move 2drop

If you write

( board) 0 0 rot guard-board-next-o x-move 2drop

you get a "undefined word" error because x-move is not in the
board-next-o wordlist. The definition of guard-board-next-o could
look like this:

: guard-board-next-o ( compilation: "word" "word" -- ;
run-time: ... board -- ... )
]] dup is-board-next-o if [[
parse-name board-next-o find-name-in dup 0= -13 and throw
name>compile execute
]] else drop [[
parse-name find-name dup 0= -13 and throw name>compile execute
]] then [[ ; immediate

Admittedly, if you really want to go there, it's better to have the
type system from the ground up rather than tacked on like shown above,
but I don't really want to go there, and this proof-of-concept is good
enough to show that it can be done in Forth (the "from-the-ground-up"
can also be done in Forth, but would require much more effort.

- 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 2021: https://euro.theforth.net/2021

> New concepts are by definition "non-standard" - because they are NEW. They are here to be explored. As I did when I added two Factor like libraries to 4tH.
> And you know what? As I had handcoded some primitives, some Factor definitions could be added verbatim. And stuff started to look more and more like Factor.
New concepts are not appears just because of dreams or wishes to 'promote' language.

> Exploring takes effort. It doesn't come for free. And may be you don't really like it. I didn't find wrapping my head around nested quotations easier than vanilla Forth - agreed.
> It didn't make me embrace Factor in any way, although I still think the concept has merit. But at least I didn't discard it with the cheap excuse that it is "non-standard".

Having no practice means having no specific goals. Adding features and converting Forth to extended Forth, Factor, C, Lisp etc etc is an empty work.
> If we, as a community keep denying that there are new concepts being developed - while there most certainly are - then we won't have no new conepts.
> None are published, none are posted - why should one even try - and none are explored and none are discussed. We as a community will cease to exist due to our own conservatism.

This is not pure comservatism. This is an attempt to ride on the 'Forth' brand. Selected persons are allowed to do this and they are stopping not initiatives, but attempts to
rebuild 'hierarchy', as they understand it.
> And there is plenty to do. We need a complete string wordset. We need to replace some ugly C-isms like the FILE wordset. We could set the first step towards an OO wordset. We could explore alternatives to locals (another horrible C-ism). AND THERE ARE!
>
> All that as alternative to our endless and rather fruitless complaining. At least it confirms to me why I do not do any effort anymore.

The is no complaining indeed. Looking at 'forth' in a web resource name, people may wait a place to discuss Forth. Not to listen how wrong they are
and how many 'proposals' they need to send before they will be allowed to become a part of a 'hierarchy'. This is a kind of cult.

Marcel Hendrix <mhx@iae.nl> writes:
> If you state that "static typing is necessary" I would be interested
> to know how you are going to test if static typing actually works as
> intended for a concrete example that can not be reproduced with a
> Forth program taking the aforementioned input for the test :--)

The specification doesn't only say what is supposed to happen when you
execute a correct program. Of course you can implement any such
specification in Forth if you can implement it in some other language.

For this problem, the specification says what is supposed to happen when
you compile the program, not just what happens when you execute it. It
says when you compile a program that tries to make an illegal move, the
compiler is supposed to signal a type error AT COMPILE TIME, not at run
time. The concept of a compile time type error is intrinsically one of
static types.

It is perfectly valid for a program specification to say things about
its meta-properties like that, and not just its runtime behaviour. For
example, a program specification might say the program is supposed to be
written in Forth, that every word is supposed to have a stack comment,
that its documentation is supposed to be written in Dutch, etc. You
can't satisfy those requirements with a Haskell program documented in
English.

This particular specification says to use static types in a certain way,
and gives a reasonable explanation of why you might want to do that.
Obviously, since the specification says "you must use static types", you
can't do it without static types. I can post my Haskell solution to
that problem if you want to see it, but here is one (not by me) that I
like even better:

https://www.reddit.com/r/haskell/comments/ti5il/redblack_trees_in_haskell_using_gadts_existential/

anton@mips.complang.tuwien.ac.at (Anton Ertl) writes:
> I expect that his move and take-move-back words return one of the
> following subtypes of a board-state type:
>
> board-finished
> board-empty ...

Yes, my solution ended up looking like that.

> Anyway, about doing that in Forth: One could put the words in separate
> wordlists (with each wordlist representing a type), and then have
> words that do the type-guarding and wordlist lookup.

Oh, this is interesting, and very clever. Maybe it is in some sense
doable after all. I'll try to look at it more closely.