On Mon, 26 May 2014, Jasmin Christian Blanchette wrote:
Am 26.05.2014 um 12:34 schrieb Lawrence Paulson <l...@cam.ac.uk>:
What new users see when they look at the actual definition of lists is
not that important. There are many, many situations where the actual
definition of something is much more complicated than the idealised
version that one would use for teaching.
Indeed, this is an old observation that has been repeated over and over
throughout the history of computing. The definitions of most library
functionality in various programming languages looks obfuscated. Take
for example "stdio.h" in C. On my "user-friendly Mac", it looks like
this:
__BEGIN_DECLS
void clearerr(FILE *);
int fclose(FILE *);
...
int fgetpos(FILE * __restrict, fpos_t *);
char *fgets(char * __restrict, int, FILE *);
#if defined(_DARWIN_UNLIMITED_STREAMS) || defined(_DARWIN_C_SOURCE)
FILE *fopen(const char * __restrict, const char * __restrict)
__DARWIN_ALIAS_STARTING(__MAC_10_6, __IPHONE_3_2, __DARWIN_EXTSN(fopen));
#else /* !_DARWIN_UNLIMITED_STREAMS && !_DARWIN_C_SOURCE */
FILE *fopen(const char * __restrict, const char * __restrict)
__DARWIN_ALIAS_STARTING(__MAC_10_6, __IPHONE_2_0, __DARWIN_ALIAS(fopen));
#endif /* (DARWIN_UNLIMITED_STREAMS || _DARWIN_C_SOURCE) */
int fprintf(FILE * __restrict, const char * __restrict, ...)
__printflike(2, 3);
One could blame the C language for being obsolete and requiring all this
extra rubbish, but even Scala can compete here. Scala libraries are easy
to use, but only a few elect experts know how there are implemented.
See again
http://stackoverflow.com/questions/1722726/is-the-scala-2-8-collections-library-a-case-of-the-longest-suicide-note-in-hist
I've implemented collections myself until Scala 2.7, but starting with
Scala 2.8 I am flying blind, and merely hope to get my own little add-ons
over continued changes by the experts, e.g. see 86f9c6912965.
For HOL we have our own history of complexity in the bootstrap process.
Everything below theory Main might be somehow obscure. Often it is
possible to do some peephole optimizations to reduce the obscurity to a
reasonable level.
The same for Pure. The new @{here} antiquotation at least gives the
formal declaration point of type "fun", but without any clue how it is
really done.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
