On 3/12/2022 9:51 AM, Anton Ertl wrote:
> Ivan Godard <ivan@millcomputing.com> writes:
>> On 3/9/2022 10:00 AM, Anton Ertl wrote:
>>> Ivan Godard <ivan@millcomputing.com> writes:
>>>> On 3/7/2022 12:19 AM, Anton Ertl wrote:
>>>>> I think that type systems are an area where formal descriptions are
>>>>> relatively close to being good enough to being used. The main problem
>>>>> is that every programming language has its own type system with its
>>>>> own twists, that results in its own notation. There is no unifying
>>>>> notation like (E)BNF or stack effect notation that is usable for
>>>>> describing many languages.
> ...
>>> But we have no successful formal notation for type systems.
>>
>> Depends on what "successful" means :-) If "does the job" then we have
>> some.
>
> In the present context it means R>1; i.e., other language designers
> get infected with the notation and use it for their language,
> eventually resulting in a significant portion of programming languages
> using this notation. We have no such notation for type systems.

Ah! You mean commercially/politically successful, not technically
successful. Sorry, I misunderstood.

Tim Rentsch <tr.17687@z991.linuxsc.com> writes:
>anton@mips.complang.tuwien.ac.at (Anton Ertl) writes:
>
>> Ivan Godard <ivan@millcomputing.com> writes:
>>
>>> On 3/7/2022 12:19 AM, Anton Ertl wrote:
>>>
>>>> I think that type systems are an area where formal descriptions are
>>>> relatively close to being good enough to being used. The main problem
>>>> is that every programming language has its own type system with its
>>>> own twists, that results in its own notation. There is no unifying
>>>> notation like (E)BNF or stack effect notation that is usable for
>>>> describing many languages.
>
>There is a good theoretical reason for that. BNF (and also EBNF)
>corresponds to a particular formal model of computation, one
>level of the Chomsky hierarchy. There are only four levels in
>the Chomsky hierarchy, and the two with more expressive power
>than context-free languages are a LOT more expressive. AFAIAA
>there is no formal model of computation known between push-down
>automata (aka context-free languages) and LBAs (aka linear
>bounded automata, aka context-sensitive languages). So if you
>want a formal description in a system that has more expressive
>power than syntax, which is pretty much a requirement for a type
>system, then you're going to end up with something equivalent to
>a context-sensitive language (or a general rewrite grammar, which
>is Turing equivalent).

I don't think that's a good theoretical reason. Just because Chomsky
came up with a hierarchy of language description formalisms does not
mean that such a formalism is needed for describing type systems.
Plus, we have a practical language formalism beyond context-free
grammars: VWG. And according to Ivan Godard, that's powerful enough
for type systems. So the reason why people have not described their
type systems as VWGs is probably that it's not a good notation for
what they want to express (even if it's powerful enough).

>In practice people want their type systems to be decidable both
>for programs that are type correct and for programs that are not
>type correct, and neither CSLs nor GRGs satisfy that property.

But even if that was not a problem, I doubt that people would try to
describe their type systems with these formalisms. What I have seen
in this area is not close to these formalisms. That's no surprise,
because Chomsky designed his formalisms to describe natural languages,
not type systems.

>The reason why is explained above. As type systems become more
>ambitious, there is a need for more expressive power in the
>formal model, which ultimately leads to newer formal models that
>are more expressive than the existing ones.

But somehow this has not happened to BNF (apart from the extension to
EBNF/RRPG).

- anton
--
'Anyone trying for "industrial quality" ISA should avoid undefined behavior.'
Mitch Alsup, <c17fcd89-f024-40e7-a594-88a85ac10d20o@googlegroups.com>

On 3/12/2022 9:55 AM, Anton Ertl wrote:
> Tim Rentsch <tr.17687@z991.linuxsc.com> writes:
>> anton@mips.complang.tuwien.ac.at (Anton Ertl) writes:
>>
>>> Ivan Godard <ivan@millcomputing.com> writes:
>>>
>>>> On 3/7/2022 12:19 AM, Anton Ertl wrote:
>>>>
>>>>> I think that type systems are an area where formal descriptions are
>>>>> relatively close to being good enough to being used. The main problem
>>>>> is that every programming language has its own type system with its
>>>>> own twists, that results in its own notation. There is no unifying
>>>>> notation like (E)BNF or stack effect notation that is usable for
>>>>> describing many languages.
>>
>> There is a good theoretical reason for that. BNF (and also EBNF)
>> corresponds to a particular formal model of computation, one
>> level of the Chomsky hierarchy. There are only four levels in
>> the Chomsky hierarchy, and the two with more expressive power
>> than context-free languages are a LOT more expressive. AFAIAA
>> there is no formal model of computation known between push-down
>> automata (aka context-free languages) and LBAs (aka linear
>> bounded automata, aka context-sensitive languages). So if you
>> want a formal description in a system that has more expressive
>> power than syntax, which is pretty much a requirement for a type
>> system, then you're going to end up with something equivalent to
>> a context-sensitive language (or a general rewrite grammar, which
>> is Turing equivalent).
>
> I don't think that's a good theoretical reason. Just because Chomsky
> came up with a hierarchy of language description formalisms does not
> mean that such a formalism is needed for describing type systems.
> Plus, we have a practical language formalism beyond context-free
> grammars: VWG. And according to Ivan Godard, that's powerful enough
> for type systems. So the reason why people have not described their
> type systems as VWGs is probably that it's not a good notation for
> what they want to express (even if it's powerful enough).
>
>> In practice people want their type systems to be decidable both
>> for programs that are type correct and for programs that are not
>> type correct, and neither CSLs nor GRGs satisfy that property.
>
> But even if that was not a problem, I doubt that people would try to
> describe their type systems with these formalisms. What I have seen
> in this area is not close to these formalisms. That's no surprise,
> because Chomsky designed his formalisms to describe natural languages,
> not type systems.
>
>> The reason why is explained above. As type systems become more
>> ambitious, there is a need for more expressive power in the
>> formal model, which ultimately leads to newer formal models that
>> are more expressive than the existing ones.
>
> But somehow this has not happened to BNF (apart from the extension to
> EBNF/RRPG).

BNF is a good formal notation for syntax for the grammar kinds commonly
used in programming languages; a parser can be mechanically generated
from the grammar. BNF is insufficiently powerful to define some
languages or language components: C preprocessor, m4 and other macro
languages, Mary1 declarable syntax, impure Prolog, some Smalltalks, and
indeed any other second-order language.

A formal type system, to deserve the name, should be able to
mechanically generate a type checker for the language, something that
can take in: "int a[5]; int b = a[2][4];" and complain. Note that the
expression is syntactically correct as defined by the BNF.

According to Ivan Godard <ivan@millcomputing.com>:
> For that matter, Scandinavia has always hit way above its
>population in the language design field: ...

>In contrast, very little from the US. That the most widespread languages
>of today derive primarily from the US reflects money and politics, not
>technical advances.

First, we gave the world Fortran, Cobol, and RPG, and then retired to
spend more time with our families.

I am not a big fan of Java or Javascript but they seem to get the job
done in a lot of applications. Java showed us that bytecodes and
loadtime or JIT translation were practical. Javascript has a good enough
sandbox that people are willing to run large amounts of it from random
places in their phones. Those aren't exactly langage design advances,
but it's not just politics either.

--
Regards,
John Levine, johnl@taugh.com, Primary Perpetrator of "The Internet for Dummies",
Please consider the environment before reading this e-mail. https://jl.ly

On Saturday, March 12, 2022 at 9:59:01 PM UTC+2, John Levine wrote:
> According to Ivan Godard <iv...@millcomputing.com>:
> > For that matter, Scandinavia has always hit way above its
> >population in the language design field: ...
> >In contrast, very little from the US. That the most widespread languages
> >of today derive primarily from the US reflects money and politics, not
> >technical advances.
> First, we gave the world Fortran, Cobol, and RPG, and then retired to
> spend more time with our families.
>

My possibly wrong impression is that while ALGOL, which is a source of majority of grammar
used by majority of procedural and object-oriented languages that people write programs in today,
was defined by the group of scientists, majority of whom were German, the leading force behind the
work actually being done was Alan Perlis of USA.

> I am not a big fan of Java or Javascript but they seem to get the job
> done in a lot of applications. Java showed us that bytecodes and
> loadtime or JIT translation were practical. Javascript has a good enough
> sandbox that people are willing to run large amounts of it from random
> places in their phones. Those aren't exactly langage design advances,
> but it's not just politics either.
> --
> Regards,
> John Levine, jo...@taugh.com, Primary Perpetrator of "The Internet for Dummies",
> Please consider the environment before reading this e-mail. https://jl.ly

John Levine <johnl@taugh.com> schrieb:
> According to Ivan Godard <ivan@millcomputing.com>:
>> For that matter, Scandinavia has always hit way above its
>>population in the language design field: ...
>
>>In contrast, very little from the US. That the most widespread languages
>>of today derive primarily from the US reflects money and politics, not
>>technical advances.
>
> First, we gave the world Fortran, Cobol, and RPG, and then retired to
> spend more time with our families.

Then there was C. Soustrup is Danish, but he was working for Bell Labs
while developing C++, so...

On 3/12/2022 12:43 PM, Michael S wrote:
> On Saturday, March 12, 2022 at 9:59:01 PM UTC+2, John Levine wrote:
>> According to Ivan Godard <iv...@millcomputing.com>:
>>> For that matter, Scandinavia has always hit way above its
>>> population in the language design field: ...
>>> In contrast, very little from the US. That the most widespread languages
>>> of today derive primarily from the US reflects money and politics, not
>>> technical advances.
>> First, we gave the world Fortran, Cobol, and RPG, and then retired to
>> spend more time with our families.
>>
>
> My possibly wrong impression is that while ALGOL, which is a source of majority of grammar
> used by majority of procedural and object-oriented languages that people write programs in today,
> was defined by the group of scientists, majority of whom were German, the leading force behind the
> work actually being done was Alan Perlis of USA.

If we assume that brilliance in computer science and language design is
evenly distributed across populations, then citizens of Norway and
Netherlands (and to a lesser extent UK and German-speaking countries)
have been vastly over-represented, while the US has been the reverse.

FWIW, the opposite pattern has been true for work in databases and
operating systems, where the US has been dominant.

Anton Ertl <anton@mips.complang.tuwien.ac.at> wrote:
> Theo <theom+news@chiark.greenend.org.uk> writes:
>> EricP <ThatWouldBeTelling@thevillage.com> wrote:
>>> Yes, that makes sense.
>>> Even for a mid-80's TTL DRAM controller I would be
>>> surprised if it didn't have same-row detection.
>>> Its a few latches and xors.
>>>
>>> So you are saying that because LDM/STM do a single instruction fetch,
>>> then a sequence of data addresses, it allows same-row detection
>>> and just a column address strobe CAS will do.
>>> For a sequence of individual LD or ST, the instruction addresses
>>> would most likely be to a different row than their data addresses
>>> so same-row detect doesn't kick in, and requires full RAS and CAS.
>>
>> Yes. So a traditional LD/ST (even if to contiguous addresses) gives you:
>>
>> row(instr. fetch); col(IF); row(data0); col(data0);
>> row(instr. fetch); col(IF); row(data1); col(data1);
>> ...
>> row(instr. fetch); col(IF); row(data15); col(data15);
>>
>> whereas STM/LDM has:
>>
>> row(IF); col(IF); row(data0); col(data0);
>> col(data1);
>> ...
>> col(data15);
>>
>> I'm not very familiar with 1980s DRAMs but I don't think they had multiple
>> banks so you could have several rows open at once.
>
> Yes, I don't think they had multiple banks.
>
> I recently revisited memory copying on a 6502: It took ~15
> cycles/byte (i.e., 66kB/s on a C64).
>
> The first ARM could use 12 registers for copying (1 PC, 1 source, 1
> destination, 1 limit), so copying 48 bytes took 15+15+1+2 cycles (1
> for subtract/compare, 2 for the branch; ARM experts will correct me if
> that does not work out), i.e., 0.69 cycles/byte (a little less with
> unrolling), about 22 times faster than the 6502 at the same clock rate
> (and the clock rate was faster). Not bad.
>
> - anton

But how fast was the 65816?
Which is a better match age wise for ARM than the 6502.

Brett <ggtgp@yahoo.com> writes:
>Anton Ertl <anton@mips.complang.tuwien.ac.at> wrote:
>> I recently revisited memory copying on a 6502: It took ~15
>> cycles/byte (i.e., 66kB/s on a C64).
>>
>> The first ARM could use 12 registers for copying (1 PC, 1 source, 1
>> destination, 1 limit), so copying 48 bytes took 15+15+1+2 cycles (1
>> for subtract/compare, 2 for the branch; ARM experts will correct me if
>> that does not work out), i.e., 0.69 cycles/byte (a little less with
>> unrolling), about 22 times faster than the 6502 at the same clock rate
>> (and the clock rate was faster). Not bad.
>>
>> - anton
>
>But how fast was the 65816?

The 65816 has dedicated instructions for copying memory blocks (MVN
and MVP). They take 7 cycles/byte, i.e., about 10 times slower than
the ARM at the same clock rate.

- anton
--
'Anyone trying for "industrial quality" ISA should avoid undefined behavior.'
Mitch Alsup, <c17fcd89-f024-40e7-a594-88a85ac10d20o@googlegroups.com>

Ivan Godard wrote:
> On 3/12/2022 12:43 PM, Michael S wrote:
>> On Saturday, March 12, 2022 at 9:59:01 PM UTC+2, John Levine wrote:
>>> According to Ivan Godard <iv...@millcomputing.com>:
>>>> For that matter, Scandinavia has always hit way above its
>>>> population in the language design field: ...
>>>> In contrast, very little from the US. That the most widespread
>>>> languages
>>>> of today derive primarily from the US reflects money and politics, not
>>>> technical advances.
>>> First, we gave the world Fortran, Cobol, and RPG, and then retired to
>>> spend more time with our families.
>>>
>>
>> My possibly wrong impression is that while ALGOL, which is a source of
>> majority of grammar
>> used by majority of procedural and object-oriented languages that
>> people write programs in today,
>> was defined by the group of scientists, majority of whom were German,
>> the leading force behind the
>> work actually being done was Alan Perlis of USA.
>
> If we assume that brilliance in computer science and language design is
> evenly distributed across populations, then citizens of Norway and
> Netherlands (and to a lesser extent UK and German-speaking countries)
> have been vastly over-represented, while the US has been the reverse.
>
> FWIW, the opposite pattern has been true for work in databases and
> operating systems, where the US has been dominant.
This is what I call the "law of small numbers", a law which I just
invented. :-)

The population of Norway is so low that as soon as we get one or two
brilliant outliers interested in a particular field, like Ole-Johan Dahl
and Kristen Nygaard, the Simula object-oriented programming inventors,
or Magnus Carlsen in chess, we suddenly become wildly successful when
measured per capita.

Last summer we had the winner of the Olympic Triathlon, a sport where we
had effectly zero active competitors 10 years ago. Now we are like the
international triathlon hothouse with Kristian Blummenfelt leading a
very small but strong group that train together.

Terje
PS. This "law" is most visible in winter olympics where the most
successful nation since it started is Liechtenstein: They have a single
medal over almost 100 years, but their total population is just 38K.

--
- <Terje.Mathisen at tmsw.no>
"almost all programming can be viewed as an exercise in caching"

anton@mips.complang.tuwien.ac.at (Anton Ertl) writes:

> Tim Rentsch <tr.17687@z991.linuxsc.com> writes:
>
>> anton@mips.complang.tuwien.ac.at (Anton Ertl) writes:
>>
>>> Ivan Godard <ivan@millcomputing.com> writes:
>>>
>>>> On 3/7/2022 12:19 AM, Anton Ertl wrote:
>>>>
>>>>> I think that type systems are an area where formal descriptions are
>>>>> relatively close to being good enough to being used. The main problem
>>>>> is that every programming language has its own type system with its
>>>>> own twists, that results in its own notation. There is no unifying
>>>>> notation like (E)BNF or stack effect notation that is usable for
>>>>> describing many languages.
>>
>> There is a good theoretical reason for that. BNF (and also EBNF)
>> corresponds to a particular formal model of computation, one
>> level of the Chomsky hierarchy. There are only four levels in
>> the Chomsky hierarchy, and the two with more expressive power
>> than context-free languages are a LOT more expressive. AFAIAA
>> there is no formal model of computation known between push-down
>> automata (aka context-free languages) and LBAs (aka linear
>> bounded automata, aka context-sensitive languages). So if you
>> want a formal description in a system that has more expressive
>> power than syntax, which is pretty much a requirement for a type
>> system, then you're going to end up with something equivalent to
>> a context-sensitive language (or a general rewrite grammar, which
>> is Turing equivalent).
>
> I don't think that's a good theoretical reason. Just because Chomsky
> came up with a hierarchy of language description formalisms does not
> mean that such a formalism is needed for describing type systems.
> Plus, we have a practical language formalism beyond context-free
> grammars: VWG. And according to Ivan Godard, that's powerful enough
> for type systems. So the reason why people have not described their
> type systems as VWGs is probably that it's not a good notation for
> what they want to express (even if it's powerful enough).
>
>> In practice people want their type systems to be decidable both
>> for programs that are type correct and for programs that are not
>> type correct, and neither CSLs nor GRGs satisfy that property.
>
> But even if that was not a problem, I doubt that people would try to
> describe their type systems with these formalisms. What I have seen
> in this area is not close to these formalisms. That's no surprise,
> because Chomsky designed his formalisms to describe natural languages,
> not type systems.
>
>> The reason why is explained above. As type systems become more
>> ambitious, there is a need for more expressive power in the
>> formal model, which ultimately leads to newer formal models that
>> are more expressive than the existing ones.
>
> But somehow this has not happened to BNF (apart from the extension to
> EBNF/RRPG).

BNF is well suited to expressing language syntax partly because
the notation is convenient but more importantly because it has
about the right amount of expressive power.

VWG is not well suited to expressing rules for type systems
partly because the notation is not easy to understand but more
importantly because it seems overmatched to the job: it is
Turing equivalent.

My focus here is not what specific notation is used but how much
expressive power the formal model has. Whether we use a Type 3
grammar or a regular expression or a finite state machine doesn't
change the key aspect of having too limited expressive power.
Similarly whether we use the lambda calculus or a Turing machine
or VWG or a general programming language doesn't change the key
aspect of the sense that there is too much expressive power. The
problem is to find a formal model that is powerful enough to
express the rules for as-yet-unthought-of type systems, but not
so powerful that it is intractable, which basically rules out any
scheme that is Turing equivalent or even in the same category as
linear bounded automata. Judging by the lack of results, it's
hard to do that. Notation is secondary to finding a system with
the right amount of expressive power.

> VWG is not well suited to expressing rules for type systems
> partly because the notation is not easy to understand but more
> importantly because it seems overmatched to the job: it is
> Turing equivalent.

Hmm... while there is a serious problem of non-standardized notation in
the world of type systems, AFAIK virtually all existing formal
definitions of type systems (the vast majority of them are purely
academic) are expressed as logical inference rules, i.e. a formalism
that's not just Turing complete but that is even happy to describe
things we don't know how to compute (more specifically: we know how to
verify a witness but we may need an oracle to give it to us).

So, Turing completeness doesn't seem to be an obstacle in this respect.

Stefan

Terje Mathisen <terje.mathisen@tmsw.no> writes:
>PS. This "law" is most visible in winter olympics where the most
>successful nation since it started is Liechtenstein: They have a single
>medal over almost 100 years, but their total population is just 38K.

Athletes starting for Liechtenstein won 10 medals through the 2018
winter olympics <https://en.wikipedia.org/wiki/Hanni_Wenzel>, two of
them gold <https://de.wikipedia.org/wiki/Hanni_Wenzel>.

- anton
--
'Anyone trying for "industrial quality" ISA should avoid undefined behavior.'
Mitch Alsup, <c17fcd89-f024-40e7-a594-88a85ac10d20o@googlegroups.com>

On Sunday, March 13, 2022 at 2:25:54 PM UTC+2, Terje Mathisen wrote:
> PS. This "law" is most visible in winter olympics where the most
> successful nation since it started is Liechtenstein: They have a single
> medal over almost 100 years, but their total population is just 38K.
> --
> - <Terje.Mathisen at tmsw.no>
> "almost all programming can be viewed as an exercise in caching"

They have far more than a single medal.
Hanni Wenzel alone got 2 golds, 1 silver and 1 bronze.
Her brother Andreas got silver and bronze.
Hanni's daughter Tina Weirather got bronze.
Another bronze medalist are Willi Frommelt, Paul Frommelt and Ursula Konzett.

Anton Ertl wrote:
> Terje Mathisen <terje.mathisen@tmsw.no> writes:
>> PS. This "law" is most visible in winter olympics where the most
>> successful nation since it started is Liechtenstein: They have a single
>> medal over almost 100 years, but their total population is just 38K.
>
> Athletes starting for Liechtenstein won 10 medals through the 2018
> winter olympics <https://en.wikipedia.org/wiki/Hanni_Wenzel>, two of
> them gold <https://de.wikipedia.org/wiki/Hanni_Wenzel>.

Oops! This means that my reference (or the way I read it) was badly
wrong, but it makes the example even better! :-)

Terje

--
- <Terje.Mathisen at tmsw.no>
"almost all programming can be viewed as an exercise in caching"