Re: Build language with weak typing, then add scaffolding later to strengthen it?

[Georg Bauhaus <bauhaus@futureapps.invalid>]

On 25.05.15 21:54, jan.de.kruyf@gmail.com wrote:
> Oberon is very much a reduced instruction set language. Anything complex is either a library package or a code pattern. So formal proof, for those who need that, is relatively easy.

Why is formal proof any easier, then? If anything complex is either
a library package or a code pattern, then formal proof would have to
include these. Patterns are useful, of course, but they do not establish
proof by just being patterns?

> And for me production-wise it was a big bonus. When you are coding, your immediate working knowledge consists of exactly those 17 pages.

How is it that you know the libraries and the code patterns?
Can't be from the 17 pages of the report as it mentions none of them.

WRT the Ada LRM, this "works" for me:
*if* a text book or other introduction(*) or the rationale won't do:
employ the structure of the RM:

- The core language is text before Annex A. (Some 350 pages)
   (This would be the equivalent of the Oberon report.)
- In there, every section N has a few short paragraphs
   that introduce the section's topics formally, using definitions.
- Many subsections N.M start like the Oberon report, giving
   grammar; others focus on one subtopic. Note the recurring headings
   like _Syntax_ for a good guess at where you need to look.


> And you know them off by heart in no time, from doing them again and again.

Yet what is it that you know from 17 pages? It might feel good,
but that isn't good enough for a reference.

> And when you do your program design you dont get sidetracked by language complexities.

Can we get sidetracked by, say, improper choice of the code pattern?

__
(*) http://www.adaic.org/wp-content/uploads/2010/05/Ada-Distilled-24-January-2011-Ada-2005-Version.pdf