Marcel Hendrix <mhx@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

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

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.

On Friday, December 24, 2021 at 1:38:26 PM UTC+3, Marcel Hendrix wrote:
> 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.

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

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

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.

Nickolay Kolchin schrieb am Freitag, 24. Dezember 2021 um 13:09:04 UTC+1:
> 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.

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

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

On Friday, December 24, 2021 at 11:42:53 AM UTC+1, Nickolay Kolchin wrote:
> On Friday, December 24, 2021 at 1:38:26 PM UTC+3, Marcel Hendrix wrote:
> > 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.
> "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?

Thanks!

Further comment is superfluous.

-marcel

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

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

On Friday, December 24, 2021 at 2:23:57 PM UTC-5, Paul Rubin wrote:
> 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.

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?

On Friday, December 24, 2021 at 8:23:57 PM UTC+1, Paul Rubin wrote:
> 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.

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

Brian Fox <brian.fox@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.

On Thursday, December 23, 2021 at 4:09:16 PM UTC-7, 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.

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.

Hugh Aguilar schrieb am Sonntag, 26. Dezember 2021 um 00:00:46 UTC+1:
> On Thursday, December 23, 2021 at 4:09:16 PM UTC-7, 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.
> 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.

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

On 25/12/2021 00:50, Krishna Myneni wrote:
> 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.

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

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

Marcel Hendrix <mhx@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
--
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

Andy Valencia <vandys@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.

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

anton@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

Krishna Myneni <krishna.myneni@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
--
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

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

Marcel Hendrix <mhx@iae.nl> writes:
>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?

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