Modern Forth

[minf...@arcor.de]

My impression is that there are basically three different Forth worlds:
1) few commercially supported development toolchains with a battle-proven
vendor-specific Forth core
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

Ad 1) Vendors are customer-driven, they fulfill contracts. Generic language
development has no priority.

Ad 2) and 3) There seems a tendency towards permanently reinventing
or retuning old wheels. Hence no progress there as well.

It is a dilemma. Where are Forth's main application niches today?
What is lacking in Forth that prevents it from filling these niches?

[Nickolay Kolchin]

On Tuesday, December 21, 2021 at 8:05:06 PM UTC+3, minf...@arcor.de wrote:
> My impression is that there are basically three different Forth worlds:
> 1) few commercially supported development toolchains with a battle-proven
> vendor-specific Forth core
> 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
>

Add embedded as 4-th choice. Mecrisp, Amforth, FlashForth are actually
used for some embedded development.

[Kerr-Mudd, John]

As an outsider (almost perpetually looking in) I think anyone with an interest in Forth quickly sees how simple it is to implement, and then disappears down a rabbit-hole of Doing their own Thing. I had hopes of a variety called Brief (as, to me, the main innovation of Forth is Concatativeness [word?]) but, again, it was mostly just a man one show.


It also doesn't help that under
https://en.wikipedia.org/wiki/Forth

it's listed under [other]

i.e. it's difficult to search for.

--
Bah, and indeed Humbug.

[minf...@arcor.de]

Correct. AFAIK prominent embedded application domain is control of small devices.
Multitasking with or without interrupts is very often required here.

[Marcel Hendrix]

I should hope there is a fourth world where people are using
Forth for their own extremely domain-specific problems.
These people fully control their copy or version of Forth
and have no desire to further develop the basis of an
arbitrarily extensible language. The only thing they
are missing (I guess) in the current time segment
is the Forth Dimensions/FORML/JFAR type of
papers of the past era.
(https://www.forth.com/forth-books/jfar-archives/).

-marcel

[minf...@arcor.de]

One man shows have become _very_ rare ....

I imagine IOT applications could be well served by Forth, but then even the Standard
treats a Forth system as an isolated entity. Although there have been past attempts:
https://www.taygeta.com/networking/forthnet.html

[Marcel Hendrix]

On Tuesday, December 21, 2021 at 8:08:44 PM UTC+1, minf...@arcor.de wrote:
[..]

> One man shows have become _very_ rare ....

You observe that human beings have fundamentally
changed over the past 40 years?

-marcel

[dxforth]

You haven't defined "progress". For me, it's the ability to write
applications without my feeling the tools I'm using are lacking. For
the targets and applications that interest me, I'm comfortable with
what I have. Others with objectives similar to mine who have tried it
appear to agree e.g.

"Highly recommend dx forth which has a lot of nice features for CP/M.
For example very easy to build a standalone .COM program using the
turnkey word."

I set out to please myself. Had my aim been to please others - or I
tried to bite off more than I could chew - I suspect I'd be here saying
there had been no progress :)

[Ilya Tarasov]

> It is a dilemma. Where are Forth's main application niches today?
> What is lacking in Forth that prevents it from filling these niches?

1. Glueware for desktop applications.
2. Embedded, especially FPGA-based configurable CPUs.

[Marcel Hendrix]

On Tuesday, December 21, 2021 at 8:08:44 PM UTC+1, minf...@arcor.de wrote:

Bernd Paysan: https://github.com/forthy42/net2o

-marcel

[Nickolay Kolchin]

On Wednesday, December 22, 2021 at 2:39:56 AM UTC+3, Ilya Tarasov wrote:
> > It is a dilemma. Where are Forth's main application niches today?
> > What is lacking in Forth that prevents it from filling these niches?
> 1. Glueware for desktop applications.

Doesn't Factor fills that niche?

[minf...@arcor.de]

As for glueware, Python or Lua seem much better equipped.
Is there any _significant_ market for such CPUs? I thought they are more
for prototyping or very samll series.

[minf...@arcor.de]

With 'progress' I imagine things like more complex data structures, parallelism,
ready-to-use libraries for important application domains etc.

What you described is sort of "Forth is my Swiss army knife in my one-man show.
It is good enough as it is". But okay if this what it means to you.

[dxforth]

That would be reinventing the wheel - no? Who will care that Forth may one day
duplicate what's already been achieved elsewhere. ISTM it's not the language
clients care about, rather the programmer with ability to do what average
programmers and their ready-to-use libraries weren't capable of doing.

>
> What you described is sort of "Forth is my Swiss army knife in my one-man show.
> It is good enough as it is". But okay if this what it means to you.

According to Moore it's only the latter where Forth will survive:

"A mainstay of our economy is the employment of programmers. [...] To keep those
programmers busy requires clumsy languages and bugs to chase. [...] There are
niches in which you can be creative, productive, inspired. Not everyone can be
so lucky."

[Krishna Myneni]

The perennial hand wringing about Forth's dim prospects for being a
mainstream language, even for niche applications, continues. It is a bit
amusing, but also a bit tiresome.

If one views Forth as a general framework for building and using
programs for domain-specific problems, then Forth appears in a much
better light. This can be for significant large projects involving a
group of people, which occurs more often in the vendor sphere, or for
"one-man" shows, for which a particular and specific need IS the only
necessary rationale.

Yes, there are likely hundreds of non-commercial Forths which have been
developed to various degrees. A few of them are well documented and have
sufficient features for general purpose programming or for niche uses.
Many are simple experiments, and have been abandoned after their authors
lost interest. I fail to understand why is this a negative. If anything,
it is a plus -- those who attempt to write a Forth system and carry it
to some usable level will likely be well-suited for solving a problem
with a conventional, more complete Forth system.

Cheers,
Krishna

[minf...@arcor.de]

If it stays with whining and hand wringing, you are right. Period. Nobody
needs that, waste of time.

But the question was more constructive: what is missing? where are the
bottle necks?

F.ex. those different TCP stacks mentioned. With some Google-fu one
might be able to pick one half-baked solution. With more time and effort
understand, debug, and adapt it. Would you do that?

[Nickolay Kolchin]

But 40 years ago people build complex systems in Forth. For example:

http://dl.forth.com/jfar/vol3/no2/article4.pdf

What has changed?

[Krishna Myneni]

My guess is the availability of other, better standardized programming
languages and tools which don't depart in convention as much from
traditional procedural programming is what has changed.

Krishna

[Krishna Myneni]

Good. It's always better to point out a specific example of a need such
as a full-fledged TCP stack. My understanding is that the TCP stacks do
exist from the commercial Forth vendors for specific embedded
processors. Examples of client-server Forth demos are provided in some
of the free Forth systems as well -- e.g. the http and sockets layer in
Gforth, and the sockets layer in kForth. Are these half-baked? Depends
on what you need.

Krishna

[Nickolay Kolchin]

Can you elaborate what do you mean by "better standardized programming
languages"?

[minf...@arcor.de]

Having spent the last 40 years with distributed control systems for various
industries, I can tell you that complexity and number of signals has increased
by magnitudes. Come modern complex standards for fire&safety systems,
networking, cyber security and so so and so on.

Today nobody with a sane mind would automate an airport in Forth.

[Nickolay Kolchin]

From safety point of view Forth is no different from C/C++. I.e. both work
with raw memory. Both have no builtin protection from overflow/underflow.
Forth code with proper testing and coverage will be as safe as C.

So, whats the problem? Language reputation, poor tools or lack of
programmers?

[Paul Rubin]

Nickolay Kolchin <nbko...@gmail.com> writes:
>> Today nobody with a sane mind would automate an airport in Forth.
> From safety point of view Forth is no different from C/C++.

Nobody with a sane mind would automate an airport in C today either.

> Forth code with proper testing and coverage will be as safe as C.

That's not saying much! And even assuming equivalence of the end
product, which one gets there with less total effort? Which is easier
to maintain and extend?

> So, whats the problem? Language reputation, poor tools or lack of
> programmers?

You mentioned Frama-C for validating C code: is there something like it
for Forth? What about for C++?

I'm not that advanced a C++ programmer but I use it in preference to C
these days and it really does help my productivity a lot, even if the
end product is not any safer. Productivity still counts.

[john]

> In article <87mtksw...@nightsong.com>, no.e...@nospam.invalid says...

> That's not saying much! And even assuming equivalence of the end
> product, which one gets there with less total effort? Which is easier
> to maintain and extend?
>

Delphi ?
Funny how RAD dissapeard almost overnight. I wonder why.

> > So, whats the problem? Language reputation, poor tools or lack of
> > programmers?
>

All of the above?

> You mentioned Frama-C for validating C code: is there something like it
> for Forth? What about for C++?
>

Not a validator but you can see what "tools" are - and these are very old now.:
https://en.freedownloadmanager.org/Windows-PC/Crystal-REVS-for-C.html

My deja vu has deja vu...

Seasons greetings to all.
Have a good one.


john

[Andy Valencia]

Nickolay Kolchin <nbko...@gmail.com> writes:
> But 40 years ago people build complex systems in Forth. For example:
> http://dl.forth.com/jfar/vol3/no2/article4.pdf
> What has changed?

I brought up a C-based microkernel VSTa about 20 years ago; pushing bytes out
the UART to see where the kernel crashed as it clawed its way to life. It
was pretty torturous, but as the only option, I went with it.

I did some huge changes to exceptions and interrupts on ForthOS a few years
ago. It was under qemu (and bochs for "single step the microcode" type
debugging of my mistakes), and had to be like 100x more productive.

Would I go back? No. I did it, and I know how to do it. But I will decline
to do it for now and into the future.

I've done pretty big apps in Forth. Now I do them mostly in Python. Things
don't corrupt, you can ^C out, you skip all the memory allocation hassles.
Modules and classes and all the "batteries included" amenities. I know how
to do it the old way, but I will decline to do it on into the future.

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

[Nickolay Kolchin]

Have you tried Factor?

[Nickolay Kolchin]

On Wednesday, December 22, 2021 at 11:24:48 PM UTC+3, Paul Rubin wrote:
> Nickolay Kolchin <nbko...@gmail.com> writes:
> >> Today nobody with a sane mind would automate an airport in Forth.
> > From safety point of view Forth is no different from C/C++.
> Nobody with a sane mind would automate an airport in C today either.

No. C is still number one for embedded. And in regulated areas like aviation
for example, only two languages exist -- C and Ada. There are two reasons
for that:

1. Tools.
2. General conservatism in the industry. DERs know what to expect and what
to check in C projects. And nobody wants to take responsibility when shiny
new thing suddenly explodes.

So parts of code may be written in C.

> > Forth code with proper testing and coverage will be as safe as C.
> That's not saying much! And even assuming equivalence of the end
> product, which one gets there with less total effort? Which is easier
> to maintain and extend?

In theory, with proper tools, Forth should be more simple to test.

> > So, whats the problem? Language reputation, poor tools or lack of
> > programmers?
> You mentioned Frama-C for validating C code: is there something like it
> for Forth? What about for C++?
>

Forth has nothing like that, except few academical projects. Frama-C
have some C++ support, but is in early stages.

> I'm not that advanced a C++ programmer but I use it in preference to C
> these days and it really does help my productivity a lot, even if the
> end product is not any safer. Productivity still counts.

And something like Go will make you even more productive (that depends
on target application of course). Smaller compile time, easier external
libraries integration, etc.

[Krishna Myneni]

Upon re-reading my statement, I realize it is ambiguous with respect to
"better". I meant that implementations and standards for conventional
procedural programming had improved over the original non-Forth
counterparts, e.g. better standardization amongst C compilers (although
that may have taken a while). There were also a plethora of new
languages with paradigms such as OOP, e.g. C++ and Java, which retained
familiarity with past languages. But, perhaps the most important reason
that Forth was quickly overtaken was that the large software/hardware
companies of the early 1990s, such as Microsoft, Borland, Sun
Microsystems, threw their weight behind the conventional language
descendants. This meant, for example, they could develop large libraries
of ready to use components. Small Forth companies could not compete in
the general programming space within that environment. The above
observations are mostly relevant to the development of applications for
commercial use.

Forth continues to evolve, as well as to fragment into variants. This
may be intrinsic to the nature of the language, and not altogether a bad
thing, unless one is only evaluating it through the lens of commercial use.

Krishna

[Nickolay Kolchin]

Your points are valid for desktop development. But how Forth lost
embedded?

>
> Forth continues to evolve, as well as to fragment into variants. This
> may be intrinsic to the nature of the language, and not altogether a bad
> thing, unless one is only evaluating it through the lens of commercial use.
>

Can you name Forth major evolution points since ANS?

[Paul Rubin]

Nickolay Kolchin <nbko...@gmail.com> writes:
>> Nobody with a sane mind would automate an airport in C today either.
>
> No. C is still number one for embedded. And in regulated areas like
> aviation for example, only two languages exist -- C and Ada. There are
> two reasons for that:

The airport project was not aviation (airports stay on the ground) and
only a few parts of it were embedded. It was programmed in Forth, for
heavens' sake ;-). These days, the embedded parts (sensor nodes) would
be clients to some fairly straightforward server app.

C for embedded may be fading, as embedded processors get powerful
enoough to run full featured OS's and more convenient languages.

> In theory, with proper tools, Forth should be more simple to test.

I don't know about this. Maybe it is possible.

> And something like Go will make you even more productive [than C++]

Yeah maybe sometimes, though the execution speed is considerably slower,
and for that program it mattered. I used Go some years ago though I
didn't become expert at it. The new versions may be better. I also
want to try Rust.

Ada is kind of daunting. I've played with it and read a book about it
("Ada Distilled"), understood most of the stuff in the book, but then
find I can't really follow newsgroup discussions about it because they
are about issues that the book doesn't discuss.

I have another Ada book sitting near my bed for the past year or so that
I've barely looked at. It does look good. Someday...

[Nickolay Kolchin]

On Thursday, December 23, 2021 at 8:25:24 AM UTC+3, Paul Rubin wrote:
> Nickolay Kolchin <nbko...@gmail.com> writes:
> >> Nobody with a sane mind would automate an airport in C today either.
> >
> > No. C is still number one for embedded. And in regulated areas like
> > aviation for example, only two languages exist -- C and Ada. There are
> > two reasons for that:
> The airport project was not aviation (airports stay on the ground) and
> only a few parts of it were embedded. It was programmed in Forth, for
> heavens' sake ;-). These days, the embedded parts (sensor nodes) would
> be clients to some fairly straightforward server app.

I know that land systems have different regulation. Aviation was used
to demonstrate that C is not going away anytime soon.

>
> Ada is kind of daunting. I've played with it and read a book about it
> ("Ada Distilled"), understood most of the stuff in the book, but then
> find I can't really follow newsgroup discussions about it because they
> are about issues that the book doesn't discuss.
>
> I have another Ada book sitting near my bed for the past year or so that
> I've barely looked at. It does look good. Someday...

Ada found a niche in Safety Critical Development and stays strong there.
Read about SPARK: https://www.adacore.com/about-spark

They first made formal verification tools part of language standard.

P.S. I really like your quotation style. You should write a tutorial on that.

[Paul Rubin]

Nickolay Kolchin <nbko...@gmail.com> writes:
> I know that land systems have different regulation. Aviation was used
> to demonstrate that C is not going away anytime soon.

I'm terrified if anyone is crazy enough to program avionics in C. I
know that SpaceX uses C++ which is also terrifying, but not quite in the
same way. Ada really is the best for this from what I can tell.

I believe a lot of aerospace Ada code is generated from Matlab models,
fwiw. I have no idea how Ada's safety features interact with that.

> Ada found a niche in Safety Critical Development and stays strong there.
> Read about SPARK: https://www.adacore.com/about-spark

Yes I tried to build it from source some years ago and got bogged down
in dependency issues, but I will try again sometime.

[Nickolay Kolchin]

On Thursday, December 23, 2021 at 9:06:32 AM UTC+3, Paul Rubin wrote:

(I accidentally removed this from original reply)

>
> C for embedded may be fading, as embedded processors get powerful
> enoough to run full featured OS's and more convenient languages.

full featured OS are unable to handle modern realtime requirements. I.e.
microsecond precision (It was fun to read about IPS "realtime" at 50hz in
a recent thread here).

Most boards we made in recent years have two controllers: one for realtime
processing, one for everything else. And realtime one is programmed
baremetal in C.

> > I know that land systems have different regulation. Aviation was used
> > to demonstrate that C is not going away anytime soon.
> I'm terrified if anyone is crazy enough to program avionics in C. I
> know that SpaceX uses C++ which is also terrifying, but not quite in the
> same way. Ada really is the best for this from what I can tell.
>

To supply avionics software you must have DO-178 certification. And
it has extremely strict requirements. For example, on Level-A you must
provide complete MC/DC coverage. You also can't write tests "just for
coverage". You must provide complete trace from high-level requirements
to assembler code. Avionic software is most tested in the world. Until
recent Boeing accident, there were no human casualties in aviation caused
by software malfunction since DO-178 become mandatory.

The development tools must be qualified for usage in Avionics. For C we
have a lot of instruments that help us satisfy regulation requirements: LDRA,
VectorCast, etc.

So, don't worry about C. It is safe there.

SpaceX doesn't follow any serious regulations. That just need to get
acceptance from NASA. Their approach won't work in aviation. Actually,
Tesla approach won't work in aviation too. Just imagine, that you board
Airbus and pilot shouts -- "Lady and Gentleman, we are happy to see you
on our airliner. We are currently updating board systems to latest beta
software. God save us all". Koopman writes a lot on this topic.

> I believe a lot of aerospace Ada code is generated from Matlab models,
> fwiw. I have no idea how Ada's safety features interact with that.

Matlab can generate C code. That approach is commonly used to save costs.
But generated code tend to be large and ineffective compared to handwritten.
This may change in future.

> > Ada found a niche in Safety Critical Development and stays strong there.
> > Read about SPARK: https://www.adacore.com/about-spark
> Yes I tried to build it from source some years ago and got bogged down
> in dependency issues, but I will try again sometime.

I've just downloaded prebuild software.

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

[dxforth]

On 23/12/2021 17:37, Nickolay Kolchin wrote:
>
> P.S. But we kinda moved away from Forth again.

Here was I thinking you and Paul were done giving reasons why
Forth was no longer suited to anything. There's more? :)

[Nickolay Kolchin]

I thought he was giving reasons why C is obsolete.

Imagine, if Forth has tools like LDRA and Frama-C. Will it become
acceptable for modern development?

[minf...@arcor.de]

AFAIU Frama-C builds its own abstract syntax tree from C sources.
Given that Forth is practically grammar-free, that won't work well.
BTW Frama-C itself is written in OCAML.

[Nickolay Kolchin]

We can perform analyse on compiled bytecode. Forth can be treated as
kind of assembler language. So, no real problem here. Also, due to simpler
language -- less things need to be checked.

[minf...@arcor.de]

Are you really saying that assembly language is no real problem for certification??

Even on higher Forth level, analyse:
: TEST
POSTPONE IF ] R> ?DUP DROP ; IMMEDIATE
It compiles hassle-free in gforth ...

[Marcel Hendrix]

How do these tools get past Goedel's second theorem?

-marcel

[Andy Valencia]

Nickolay Kolchin <nbko...@gmail.com> writes:
> Have you tried Factor?

Years ago, and I thought it was the most promising attempt to bring Forth
forward that I had ever seen.

I tried it more recently, and the build/install had become quite bloated.
The build failed in some non-obvious way, I spent a couple hours slogging
through a maze of code trying to figure out why, and then had to move on.

[Nickolay Kolchin]

Well, this is pure theory, but:

1. We can define precondition and postcondition for each word here.
2. We are not really interested in `immediate` words verification. We are
interested in final code. But i don't see immediately how "specification"
can be written for such words. This may be an interesting challenge.
3. SPARK originally have no support for recursion and many other Ada
features. Frama-C also worked on C subset. There can be defined a
"safe" Forth wordset as a starting point.

[Nickolay Kolchin]

Hoare logic?

[Anton Ertl]

Marcel Hendrix <m...@iae.nl> writes:
>How do these tools get past Goedel's second theorem?

Do they? Do they need to? I don't think so. The typical way with
correctness proofs is that the programmer needs to write the program
in a way that is accepted by the prover.

- 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

[Ilya Tarasov]

среда, 22 декабря 2021 г. в 11:14:33 UTC+3, Nickolay Kolchin:

> On Wednesday, December 22, 2021 at 2:39:56 AM UTC+3, Ilya Tarasov wrote:
> > > It is a dilemma. Where are Forth's main application niches today?
> > > What is lacking in Forth that prevents it from filling these niches?

> > 1. Glueware for desktop applications.
> Doesn't Factor fills that niche?

No idea. I have no time to check every programming language in the world. For me,
Forth is a kind of programming technology and I use my own Forth translators. Factor
may be good for it's users.

[Krishna Myneni]

Someone from an electronics engineering background may be better suited
to answer that. I have done some embedded programming on a couple of
microcontrollers, for which Forth was not available at the time. I think
C was universally available on microcontrollers at that time (mid to
late 90s). I suspect the availability of Forth on microcontrollers was
pretty limited at that time. Although engineers are usually conservative
in their implementations, I think the loss of Forth on desktop
development impacts development on embedded systems as well.

>>
>> Forth continues to evolve, as well as to fragment into variants. This
>> may be intrinsic to the nature of the language, and not altogether a bad
>> thing, unless one is only evaluating it through the lens of commercial use.
>>
>
> Can you name Forth major evolution points since ANS?
>

In my opinion, Forth 2012 was the next significant evolution point. It
cleaned up and added some missing floating point functionality (and also
standardized the separate fp stack), added standardized data structures,
standardized numeric input in different bases, added the concept of
"name token" along with a so-called higher order function which allowed
deeper introspection into the system, provided optional support for
recognizing extended characters for all words which deal with character
input and output, added a low-level parsing word which was needed, added
support for non-printable characters in strings, improved deferred word
support, and some other features.

I can't speak on the developments in the embedded world, although Forth
systems which support ARM architectures seem to be a significant
development.

Krishna

[minf...@arcor.de]

Andy Valencia schrieb am Donnerstag, 23. Dezember 2021 um 17:16:22 UTC+1:
> Nickolay Kolchin <nbko...@gmail.com> writes:
> > Have you tried Factor?
>
> Years ago, and I thought it was the most promising attempt to bring Forth
> forward that I had ever seen.
>

IMO Factor's important contribution was moving away from Forth's CPU-centricity
towards a more data-oriented design. And it 'comes' with many libraries.

[dxforth]

On 24/12/2021 10:09, Krishna Myneni wrote:
> On 12/22/21 22:30, Nickolay Kolchin wrote:

>> ...

>> Can you name Forth major evolution points since ANS?
>>
> In my opinion, Forth 2012 was the next significant evolution point. It
> cleaned up and added some missing floating point functionality (and also
> standardized the separate fp stack), added standardized data structures,
> standardized numeric input in different bases, added the concept of
> "name token" along with a so-called higher order function which allowed
> deeper introspection into the system, provided optional support for
> recognizing extended characters for all words which deal with character
> input and output, added a low-level parsing word which was needed, added
> support for non-printable characters in strings, improved deferred word
> support, and some other features.

More consolidation of power than evolutionary as most of those pre-existed
in one form or another. The majors got their way and the independents
went theirs.

[minf...@arcor.de]

It is not helpful to belittle those steps and the amount of work that went into
making the steps. A "giant leap for mankind" does not make more followers
automatically, but probably more sceptics I guess.

Nevertheless it speaks volumes to mention 'standardized data structures'
(ie BEGIN-STRUCTURE .. +FIELD .. END-STRUCTURE) as improvement in
Forth2012. This is at grass roots level, it can't get any lower. No lists, arrays,
dynamic strings etc that are elementary data types practically anywhere else.
OO with methods and classes? Google your favourite package or better
roll your own private Idaho...

[dxforth]

On 24/12/2021 14:26, minf...@arcor.de wrote:
> dxforth schrieb am Freitag, 24. Dezember 2021 um 01:22:11 UTC+1:
>> On 24/12/2021 10:09, Krishna Myneni wrote:
>> > On 12/22/21 22:30, Nickolay Kolchin wrote:
>> >> ...
>> >> Can you name Forth major evolution points since ANS?
>> >>
>> > In my opinion, Forth 2012 was the next significant evolution point. It
>> > cleaned up and added some missing floating point functionality (and also
>> > standardized the separate fp stack), added standardized data structures,
>> > standardized numeric input in different bases, added the concept of
>> > "name token" along with a so-called higher order function which allowed
>> > deeper introspection into the system, provided optional support for
>> > recognizing extended characters for all words which deal with character
>> > input and output, added a low-level parsing word which was needed, added
>> > support for non-printable characters in strings, improved deferred word
>> > support, and some other features.
>> More consolidation of power than evolutionary as most of those pre-existed
>> in one form or another. The majors got their way and the independents
>> went theirs.
>
> It is not helpful to belittle those steps and the amount of work that went into
> making the steps.

Self-interest is hardly work.

> A "giant leap for mankind" does not make more followers
> automatically, but probably more sceptics I guess.

You say Forth lacks ready-to-use libraries. If they've not materialized
with what's been added thus far, then what, when and who?

> Nevertheless it speaks volumes to mention 'standardized data structures'
> (ie BEGIN-STRUCTURE .. +FIELD .. END-STRUCTURE) as improvement in
> Forth2012. This is at grass roots level, it can't get any lower.

You can define them yourself - if you really needed them. They mimic methods
found in other languages, despite Forth offering other possibilities which
are arguably more forth-like. Forth today smacks of 'cultural cringe'. You
could put it in the Standard and nobody would even notice :)

> No lists, arrays,
> dynamic strings etc that are elementary data types practically anywhere else.
> OO with methods and classes? Google your favourite package or better
> roll your own private Idaho...

QED

[Marcel Hendrix]

On Thursday, December 23, 2021 at 6:36:58 PM UTC+1, Anton Ertl wrote:
> Marcel Hendrix <m...@iae.nl> writes:
> >How do these tools get past Goedel's second theorem?
> Do they? Do they need to? I don't think so. The typical way with
> correctness proofs is that the programmer needs to write the program
> in a way that is accepted by the prover.

IOW, axiom one: the prover is correct?

-marcel

[Paul Rubin]

Marcel Hendrix <m...@iae.nl> writes:
> IOW, axiom one: the prover is correct?

No, come on. That type of issue can't be avoided in theory, but is
rarely an issue in practice. See:

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.106.364&rep=rep1&type=pdf

[Marcel Hendrix]

On Friday, December 24, 2021 at 9:15:21 AM UTC+1, Paul Rubin wrote:
> Marcel Hendrix <m...@iae.nl> writes:
> > IOW, axiom one: the prover is correct?
> No, come on. That type of issue can't be avoided in theory, but is
> rarely an issue in practice.

Ok, can we at least ask that the prover processes its own source code
with positive results?

One could bypass the problem by requiring that software for
purpose 'X' passes checks implemented by prover 'Y.'

-marcel

[Marcel Hendrix]

On Friday, December 24, 2021 at 9:15:21 AM UTC+1, Paul Rubin wrote:

[..]
> http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.106.364&rep=rep1&type=pdf

A pity, one of those pdfs can not be copy/pasted from. Quite ironical, considering the
stament 1) that I wanted to highlight but can't :--)

-marcel

1) The paper's last paragraph.

[Nickolay Kolchin]

"Five decades ago, at the beginning of electronic computing, we chose (B).
If it is the case, as seems likely, that we can have languages of type (A) which
accomodate all the programs we need to write, bar a few special situations, it
may be time to reconsider this decision."

This?

[Paul Rubin]

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

I think we are not talking about the same thing. These provers are
usually not completely automatic. They are proof checkers with some
partial automation and some manual assistance.

Say your program has a variable N, and at a certain place in the
program, you require that N < 15. You can see where N is initialized,
and where it is incremented by 1 over here and by either 1 or 2 over
there, etc. Adding those up, you see N is at most 14, satisfying the
requirement. But just in case, you put in an "assert(N < 15)" , that
checks at runtime that N < 15. The idea is that N>=15 is definitely
a program bug.

Now you have a code review: the reviewer asks how you know that N < 15.
In principle your answer could rely on horrendous math, but in practice
it is usually straightforward, like above. So you can give a reasonable
explanation to the reviewer. That is similar to what a verifier like
SPARK does. It sees the assert statement and tries to prove that the
assert never fails. It can often figure out the proof by itself, though
sometimes you have to help it. Once the assertion is proved, the
compiler can eliminate the runtime check and you can be sure that the
program won't crash.

I believe SPARK proofs are all in quite simple arithmetic, level 1 of
the arithmetic hierarchy if you're familiar with that. The proof
automation is done with SAT solvers which don't always succeed, thus the
occasional need for manual help.

Obviously at the bottom of all this, there are some assumptions like
"Peano arithmetic is consistent". There is no way around that in
regular mathematics either.

The issues are somewhat different for fancier proof systems intended
more for math theorems than for program checking, so I'll skip that.

[Nickolay Kolchin]

On Friday, December 24, 2021 at 2:36:27 PM UTC+3, Paul Rubin wrote:

>
> I believe SPARK proofs are all in quite simple arithmetic, level 1 of
> the arithmetic hierarchy if you're familiar with that. The proof
> automation is done with SAT solvers which don't always succeed, thus the
> occasional need for manual help.
>

AdaCore uses why3 which is the frontend to various provers. Most common
are Z3, Alt-Ergo and CVC4.

[minf...@arcor.de]

"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.

[Krishna Myneni]

On 12/24/21 01:10, dxforth wrote:
> On 24/12/2021 14:26, minf...@arcor.de wrote:

...

>> Nevertheless it speaks volumes to mention 'standardized data structures'
>> (ie BEGIN-STRUCTURE .. +FIELD .. END-STRUCTURE) as improvement in
>> Forth2012. This is at grass roots level, it can't get any lower.
>
> You can define them yourself - if you really needed them.  They mimic
> methods
> found in other languages, despite Forth offering other possibilities which
> are arguably more forth-like.  Forth today smacks of 'cultural cringe'.
> You
> could put it in the Standard and nobody would even notice :)
>

And you can still define structures yourself, despite standardized
versions being present in Forth systems. In fact, revisions to my own
legacy code uses a mix of an older non-standard structures package
(struct.4th) with the standardized structures from Forth 2012. A notable
exception is my version of the FSL which has been updated to use
standardized structures. All new code which I write uses the Forth 2012
standardized structures.

The case for standardized structures is simple. It means I can use the
work of others, and others can use mine, with little effort. If you only
work in isolation, without need for or interest in the work of others,
or in making your shared source easily usable by others, then you can
certainly ignore standardized structures, whether they are present or not.

Krishna

[Marcel Hendrix]

Thanks!

Further comment is superfluous.

-marcel

[Marcel Hendrix]

On Friday, December 24, 2021 at 12:36:27 PM UTC+1, Paul Rubin wrote:
> Marcel Hendrix <m...@iae.nl> writes:

[..]

> Say your program has a variable N, and at a certain place in the
> program, you require that N < 15. You can see where N is initialized,
> and where it is incremented by 1 over here and by either 1 or 2 over
> there, etc. Adding those up, you see N is at most 14, satisfying the
> requirement. But just in case, you put in an "assert(N < 15)" , that
> checks at runtime that N < 15. The idea is that N>=15 is definitely
> a program bug.

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?
At compile-time? At run-time? Once? Always?

-marcel

[Paul Rubin]

Marcel Hendrix <m...@iae.nl> writes:
> How would one use SPARK to usefully catch such a problem?
> At compile-time? At run-time? Once? Always?

You would write a contract with that spec, i.e.

POST => IF y /= 0 THEN r = x - y*q;

or something like that. POST means it is a postcondition for the
function. SPARK is a static verifier so you would run it at compile
time, or possibly as a separate (pre-compilation) phase or your build
process. Floating point being messy, I don't know what the proof would
look like. In the event that SPARK couldn't prove the postcondition, it
would give you an example of values of x and y where the condition
failed.

Here is a simple SPARK example:

https://learn.adacore.com/courses/intro-to-spark/chapters/01_Overview.html#a-trivial-example

There are more complicated examples in that document as well.

[Brian Fox]

Could the Hayes tester be used to write such "contracts" for a Forth project?
It might appear to be self-referential but if the entire system and the application
were tested as they compiled it would be pretty solid wouldn't it?

[Marcel Hendrix]

Cool stuff -- I could change, execute, and check the examples on-line.

It let me add 1.0e-422 to X without problem. That is of course not
necessarily wrong.

-marcel

[Paul Rubin]

Brian Fox <bria...@brianfox.ca> writes:
> Could the Hayes tester be used to write such "contracts" for a Forth
> project?

Contracts checked at runtime (they amount to assert statements) are a
standard technique that sometimes catches errors. However, the usual
warning about testing is that sometimes the errors live in weird edge
cases that escape the tests.

Haskell has a test framework called QuickCheck that other languages have
grown versions of. QuickCheck examines the type signature of a function
and uses it to generate random values of the relevant type, basically
fuzz-testing the function. I guess that could be done for Forth too,
though the types and test vectors would need more manual setup since
Forth doesn't have static types.

For a while, static verification tools like Coverity were popular for
C. I've been told that in recent years, they have been somewhat
displaced by fuzzing systems, which are also quite effective in practice
(at least for C). I don't know whether that also applies to Frama-C,
which appears to be somewhat like SPARK.

[Hugh Aguilar]

LOL
Forth 2012 was worthless, and Forth-200x continues to be worthless.

The only "evolution point" since ANS-Forth was my rquotations.
This is roughly comparable to the "evolution point" in human development
when we began using tools, distinguishing ourselves from the beasts.
Note that ANSI-C programmers continue to lack anything comparable to
my rquotations --- GCC does have nested functions, but that is non-standard
in the ANSI-C world just as my rquotations are non-standard in Forth-200x.
The rquotations, by themselves, are more valuable than anything that the
entire Forth-200x committee has come up with --- Forth can do without
the Forth-200x committee, but needs rquotations in order to support
general-purpose data-structures which are necessary to have a future.

Also, I think that my STRING-STACK.4TH qualifies as an "evolution point."
There have been multiple weak attempts at a string-stack in Forth, starting with
Wil Baden's, but all of them move entire strings in memory when doing string-stack
juggling and all of them have severe limitations on how many strings are
supported and how big the strings can be. Only my STRING-STACK.4TH has
COW (copy-on-write) that allows pointers to be moved most of the time when
stack juggling, and has no limitation on how many strings can be on the stack
or how big they can be.

[minf...@arcor.de]

You are progressing. I didn't think you could be so self-humourous. :o)

[dxforth]

Who needs structures?

1) Turbo Pascal target

153 constant 'TNAME \ terminal name
1A0 constant 'TDCM \ terminal delays
1BA constant 'TDCLS \
1CE constant 'TDEOL \

\ copy terminal data to target
: TNAME ( -- ) 'tname 0 set.s ; \ terminal name
: TINIT ( -- ) 16B 16 set.s ; \ term init
: TEXIT ( -- ) 17B 26 set.s ; \ term exit
: TCM ( -- ) 18B 36 set.s ; \ cursor motion template
: TBIN ( -- ) 19B 46 set.b ; \ binary mode
: TPOS ( -- ) 19E 47 set.w ; \ col row pos
: TOFFS ( -- ) 19C 49 set.w ; \ col row offset
: TDCM ( -- ) 'tdcm 4B set.w ; \ cm delay
: TCLS ( -- ) 1A2 4D set.s ; \ clear screen
: THOM ( -- ) 1A8 53 set.s ; \ home cursor
: TDCLS ( -- ) 'tdcls 59 set.w ; \ cls delay
: THIL ( -- ) 1C2 5B set.s ; \ hilight video
: TNOR ( -- ) 1C8 61 set.s ; \ normal video
: TDEOL ( -- ) 'tdeol 67 set.w ; \ eol delay
: TEOL ( -- ) 1BC 69 set.s ; \ clear to end-of-line
: TINS ( -- ) 1AE 6F set.s ; \ insert line
: TDEL ( -- ) 1B4 75 set.s ; \ delete line
: TCR ( -- ) 168 7B set.w ; \ # cols rows


2) Turbo Modula-2 target

352 constant 'TNAME \ terminal name
3A0 constant 'TDCM \ terminal delays
3BE constant 'TDCLS \
3D6 constant 'TDEOL \

\ copy terminal data to target
: TNAME ( -- ) 'tname 0 set.s ; \ terminal name
: TINIT ( -- ) 36A 16 set.s ; \ term init
: TEXIT ( -- ) 37A 26 set.s ; \ term exit
: TCM ( -- ) 38A 36 set.s ; \ cursor motion template
: TBIN ( -- ) 39A 46 set.b ; \ binary mode
: TPOS ( -- ) 39E 47 set.w ; \ col row pos
: TOFFS ( -- ) 39C 49 set.w ; \ col row offset
: TDCM ( -- ) 'tdcm 4B set.w ; \ cm delay
: TCLS ( -- ) 3A2 4D set.s ; \ clear screen
: THOM ( -- ) 3A8 53 set.s ; \ home cursor
: TDCLS ( -- ) 'tdcls 59 set.w ; \ cls delay
: THIL ( -- ) 3CE 5B set.s ; \ hilight video
: TNOR ( -- ) 3C6 61 set.s ; \ normal video
: TDEOL ( -- ) 'tdeol 67 set.w ; \ eol delay
: TEOL ( -- ) 3C0 69 set.s ; \ clear to end-of-line
: TINS ( -- ) 3AE 6F set.s ; \ insert line
: TDEL ( -- ) 3B8 75 set.s ; \ delete line
: TCR ( -- ) 368 7B set.w ; \ # cols rows

[Anton Ertl]

"minf...@arcor.de" <minf...@arcor.de> writes:
>Where are Forth's main application niches today?
>What is lacking in Forth that prevents it from filling these niches?

Today's niches are filled by today's Forths. But one may wonder what
potential niches for Forth exist, and if Forth is missing something
for that niche.

One niche that I see for Forth is low-level programming. C has been
used for that in the past, and still is, but there is a movement in
the C world that denies that C was ever meant to be used in that way,
so C is moving away from this niche.

What Forth needs for that is more performance and IMO better
guarantees (C moves away from the niche by telling low-level
programmers that they should not have relied on properties that the C
standard does not guarantee). I have sketched PAF, a dialect of Forth
for that, but have not yet found time to implement it.

[Anton Ertl]

Marcel Hendrix <m...@iae.nl> writes:
>The only thing they
>are missing (I guess) in the current time segment
>is the Forth Dimensions/FORML/JFAR type of
>papers of the past era.

There is EuroForth for publishing such papers, but people also need to
write them. It seems that since 2020 people have written fewer
papers; maybe the Covid situation consumed the time that people would
otherwise have spent on writing, or maybe they decided that videos are
good enough.

[Anton Ertl]

Andy Valencia <van...@vsta.org> writes:
>I've done pretty big apps in Forth. Now I do them mostly in Python. Things
>don't corrupt, you can ^C out

You can ^C out of Gforth and other Forth systems, with some
differences in functionality. E.g., for running the following line
from the Forth command line:

: foo begin again ; foo

and then pressing ^C:

Gforth 0.7.3:
: foo begin again ; foo
:1: User interrupt
: foo begin again ; >>>foo<<<
Backtrace:
$7F80C009C4C0 branch

and you are back in the Forth command line.

SwiftForth i386-Linux 3.11.0 23-Feb-2021
: foo begin again ; foo Segmentation fault

needs two ^C and you are than back in the shell (I remember it being
nicer in other cases).

VFX Forth 64 5.11 RC2 [build 0112] 2021-05-02 for Linux x64:

: foo begin again ; foo

You are back in the shell after one ^C.

[minf...@arcor.de]

Anton Ertl schrieb am Dienstag, 28. Dezember 2021 um 19:32:49 UTC+1:
> What Forth needs for that is more performance and IMO better
> guarantees (C moves away from the niche by telling low-level
> programmers that they should not have relied on properties that the C
> standard does not guarantee).

There are very few applications that need more processing speed in a single CPU.
Programmer time has become much more important.

This implies eg
- compiler performance for high semantical expressiveness
- catching as meany errors as possible in an early development stage
(most users/customers don't accept crashing as "bug detection facility")
- good integration with powerful development and maintenance tools

[Andy Valencia]

an...@mips.complang.tuwien.ac.at (Anton Ertl) writes:
> You can ^C out of Gforth and other Forth systems, with some
> differences in functionality.

And you and your folks have done great things with gforth!
And I find there's quite a bit of memory safety:

: a 1000000 0 do 0 i ! loop ; ok
a
:2: Invalid memory address
>>>a<<<
Backtrace:
$FFFFAE0E25D0 !
$0
$F4240

However, if things really go off the rails:

' flush-file ok
. 187650824918704 ok
: d 100000 0 do 0 i 187650824918704 + ! loop ; ok
d ok


Quit.
(No response at all, not ^C, took ^\ to abort out to the shell.)

It's a great environment (ForthOS has nothing to compare with its
memory safety, never mind the ^C support). What do you think about
the string processing question I posted?

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

[Anton Ertl]

Krishna Myneni <krishna...@ccreweb.org> writes:
>But, perhaps the most important reason
>that Forth was quickly overtaken was that the large software/hardware
>companies of the early 1990s, such as Microsoft, Borland, Sun
>Microsystems, threw their weight behind the conventional language
>descendants. This meant, for example, they could develop large libraries
>of ready to use components.

But, e.g., Python did not come from these companies and still became
popular.

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. I see
too little of that (and too much anti-library sentiment) in Forth.

[Anton Ertl]

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

http://www.forth200x.org/directories.html (withdrawn due to vigorous
resistance)

Possibly other pieces, but already this one was successfully resisted.

>when and who?

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.

[Anton Ertl]

Not IOW; that's a different issue.

My point was that the prover (even if correct) cannot just prove
arbitrary code you throw at it. You have to write your program in a
special way, so that the prover can do its magic.

[Anton Ertl]

Marcel Hendrix <m...@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 Ertl]

"minf...@arcor.de" <minf...@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.

[Andy Valencia]

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.

[Paul Rubin]

an...@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.

[minf...@arcor.de]

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.

[Paul Rubin]

"minf...@arcor.de" <minf...@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.

[Marcel Hendrix]

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

[dxforth]

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.

[Hugh Aguilar]

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.

[Nickolay Kolchin]

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

[Andy Valencia]

dxforth <dxf...@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.

[Paul Rubin]

Nickolay Kolchin <nbko...@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.

[Hans Bezemer]

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

[Anton Ertl]

Marcel Hendrix <m...@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

[minf...@arcor.de]

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... ;-)

[Hans Bezemer]

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

[dxforth]

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.

[Marcel Hendrix]

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

[Paul Rubin]

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/

[Marcel Hendrix]

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

[Hans Bezemer]

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

[Anton Ertl]

Paul Rubin <no.e...@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.

[Ilya Tarasov]

> 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.

[Paul Rubin]

Marcel Hendrix <m...@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/

[Paul Rubin]

an...@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.