Tim Daly
2021-05-05 05:36:00 UTC
It is interesting that programmer's eyes and expectations adapt
to the tools they use. For instance, I use emacs and expect to
work directly in files and multiple buffers. When I try to use one
of the many IDE tools I find they tend to "get in the way". I already
know or can quickly find whatever they try to tell me. If you use an
IDE you probably find emacs "too sparse" for programming.
Recently I've been working in a sparse programming environment.
I'm exploring the question of running a proof checker in an FPGA.
The FPGA development tools are painful at best and not intuitive
since you SEEM to be programming but you're actually describing
hardware gates, connections, and timing. This is an environment
where everything happens all-at-once and all-the-time (like the
circuits in your computer). It is the "assembly language of circuits".
Naturally, my eyes have adapted to this rather raw level.
That said, I'm normally doing literate programming all the time.
My typical file is a document which is a mixture of latex and lisp.
It is something of a shock to return to that world. It is clear why
people who program in Python find lisp to be a "sea of parens".
Yet as a lisp programmer, I don't even see the parens, just code.
It takes a few minutes in a literate document to adapt vision to
see the latex / lisp combination as natural. The latex markup,
like the lisp parens, eventually just disappears. What remains
is just lisp and natural language text.
This seems painful at first but eyes quickly adapt. The upside
is that there is always a "finished" document that describes the
state of the code. The overhead of writing a paragraph to
describe a new function or change a paragraph to describe the
changed function is very small.
Using a Makefile I latex the document to generate a current PDF
and then I extract, load, and execute the code. This loop catches
errors in both the latex and the source code. Keeping an open file in
my pdf viewer shows all of the changes in the document after every
run of make. That way I can edit the book as easily as the code.
Ultimately I find that writing the book while writing the code is
more productive. I don't have to remember why I wrote something
since the explanation is already there.
We all have our own way of programming and our own tools.
But I find literate programming to be a real advance over IDE
style programming and "raw code" programming.
Tim
to the tools they use. For instance, I use emacs and expect to
work directly in files and multiple buffers. When I try to use one
of the many IDE tools I find they tend to "get in the way". I already
know or can quickly find whatever they try to tell me. If you use an
IDE you probably find emacs "too sparse" for programming.
Recently I've been working in a sparse programming environment.
I'm exploring the question of running a proof checker in an FPGA.
The FPGA development tools are painful at best and not intuitive
since you SEEM to be programming but you're actually describing
hardware gates, connections, and timing. This is an environment
where everything happens all-at-once and all-the-time (like the
circuits in your computer). It is the "assembly language of circuits".
Naturally, my eyes have adapted to this rather raw level.
That said, I'm normally doing literate programming all the time.
My typical file is a document which is a mixture of latex and lisp.
It is something of a shock to return to that world. It is clear why
people who program in Python find lisp to be a "sea of parens".
Yet as a lisp programmer, I don't even see the parens, just code.
It takes a few minutes in a literate document to adapt vision to
see the latex / lisp combination as natural. The latex markup,
like the lisp parens, eventually just disappears. What remains
is just lisp and natural language text.
This seems painful at first but eyes quickly adapt. The upside
is that there is always a "finished" document that describes the
state of the code. The overhead of writing a paragraph to
describe a new function or change a paragraph to describe the
changed function is very small.
Using a Makefile I latex the document to generate a current PDF
and then I extract, load, and execute the code. This loop catches
errors in both the latex and the source code. Keeping an open file in
my pdf viewer shows all of the changes in the document after every
run of make. That way I can edit the book as easily as the code.
Ultimately I find that writing the book while writing the code is
more productive. I don't have to remember why I wrote something
since the explanation is already there.
We all have our own way of programming and our own tools.
But I find literate programming to be a real advance over IDE
style programming and "raw code" programming.
Tim
The systems I use have the interesting property of
"Living within the compiler".
Lisp, Forth, Emacs, and other systems that present themselves
through the Read-Eval-Print-Loop (REPL) allow the
ability to deeply interact with the system, shaping it to your need.
My current thread of study is software architecture. See
and https://www.georgefairbanks.com/videos/
My current thinking on SANE involves the ability to
dynamically define categories, representations, and functions
along with "composition functions" that permits choosing a
combination at the time of use.
You might want a domain for handling polynomials. There are
a lot of choices, depending on your use case. You might want
different representations. For example, you might want dense,
sparse, recursive, or "machine compatible fixnums" (e.g. to
interface with C code). If these don't exist it ought to be possible
to create them. Such "lego-like" building blocks require careful
thought about creating "fully factored" objects.
Given that goal, the traditional barrier of "compiler" vs "interpreter"
does not seem useful. It is better to "live within the compiler" which
gives the ability to define new things "on the fly".
Of course, the SANE compiler is going to want an associated
proof of the functions you create along with the other parts
such as its category hierarchy and representation properties.
There is no such thing as a simple job. :-)
Tim
"Living within the compiler".
Lisp, Forth, Emacs, and other systems that present themselves
through the Read-Eval-Print-Loop (REPL) allow the
ability to deeply interact with the system, shaping it to your need.
My current thread of study is software architecture. See
and https://www.georgefairbanks.com/videos/
My current thinking on SANE involves the ability to
dynamically define categories, representations, and functions
along with "composition functions" that permits choosing a
combination at the time of use.
You might want a domain for handling polynomials. There are
a lot of choices, depending on your use case. You might want
different representations. For example, you might want dense,
sparse, recursive, or "machine compatible fixnums" (e.g. to
interface with C code). If these don't exist it ought to be possible
to create them. Such "lego-like" building blocks require careful
thought about creating "fully factored" objects.
Given that goal, the traditional barrier of "compiler" vs "interpreter"
does not seem useful. It is better to "live within the compiler" which
gives the ability to define new things "on the fly".
Of course, the SANE compiler is going to want an associated
proof of the functions you create along with the other parts
such as its category hierarchy and representation properties.
There is no such thing as a simple job. :-)
Tim
The Axiom SANE compiler / interpreter has a few design points.
1) It needs to mix interpreted and compiled code in the same function.
SANE allows dynamic construction of code as well as dynamic type
construction at runtime. Both of these can occur in a runtime object.
So there is potentially a mixture of interpreted and compiled code.
2) It needs to perform type resolution at compile time without overhead
where possible. Since this is not always possible there needs to be
a "prefix thunk" that will perform the resolution. Trivially, for
example,
if we have a + function we need to type-resolve the arguments.
However, if we can prove at compile time that the types are both
bounded-NNI and the result is bounded-NNI (i.e. fixnum in lisp)
then we can inline a call to + at runtime. If not, we might have
+ applied to NNI and POLY(FLOAT), which requires a thunk to
resolve types. The thunk could even "specialize and compile"
the code before executing it.
It turns out that the Forth implementation of "threaded-interpreted"
languages model provides an efficient and effective way to do this.[0]
Type resolution can be "inserted" in intermediate thunks.
The model also supports dynamic overloading and tail recursion.
Combining high-level CLOS code with low-level threading gives an
easy to understand and robust design.
Tim
[0] Loeliger, R.G. "Threaded Interpretive Languages" (1981)
ISBN 0-07-038360-X
1) It needs to mix interpreted and compiled code in the same function.
SANE allows dynamic construction of code as well as dynamic type
construction at runtime. Both of these can occur in a runtime object.
So there is potentially a mixture of interpreted and compiled code.
2) It needs to perform type resolution at compile time without overhead
where possible. Since this is not always possible there needs to be
a "prefix thunk" that will perform the resolution. Trivially, for
example,
if we have a + function we need to type-resolve the arguments.
However, if we can prove at compile time that the types are both
bounded-NNI and the result is bounded-NNI (i.e. fixnum in lisp)
then we can inline a call to + at runtime. If not, we might have
+ applied to NNI and POLY(FLOAT), which requires a thunk to
resolve types. The thunk could even "specialize and compile"
the code before executing it.
It turns out that the Forth implementation of "threaded-interpreted"
languages model provides an efficient and effective way to do this.[0]
Type resolution can be "inserted" in intermediate thunks.
The model also supports dynamic overloading and tail recursion.
Combining high-level CLOS code with low-level threading gives an
easy to understand and robust design.
Tim
[0] Loeliger, R.G. "Threaded Interpretive Languages" (1981)
ISBN 0-07-038360-X
I've worked hard to make Axiom depend on almost no other
tools so that it would not get caught by "code rot" of libraries.
However, I'm also trying to make the new SANE version much
easier to understand and debug.To that end I've been experimenting
with some ideas.
It should be possible to view source code, of course. But the source
code is not the only, nor possibly the best, representation of the
ideas.
In particular, source code gets compiled into data structures. In Axiom
these data structures really are a graph of related structures.
For example, looking at the gcd function from NNI, there is the
representation of the gcd function itself. But there is also a structure
that is the REP (and, in the new system, is separate from the domain).
Further, there are associated specification and proof structures. Even
further, the domain inherits the category structures, and from those it
inherits logical axioms and definitions through the proof structure.
Clearly the gcd function is a node in a much larger graph structure.
When trying to decide why code won't compile it would be useful to
be able to see and walk these structures. I've thought about using the
browser but browsers are too weak. Either everything has to be "in a
single tab to show the graph" or "the nodes of the graph are in
different
tabs". Plus, constructing dynamic graphs that change as the software
changes (e.g. by loading a new spad file or creating a new function)
represents the huge problem of keeping the browser "in sync with the
Axiom workspace". So something more dynamic and embedded is needed.
Axiom source gets compiled into CLOS data structures. Each of these
new SANE structures has an associated surface representation, so they
can be presented in user-friendly form.
Also, since Axiom is literate software, it should be possible to look at
the code in its literate form with the surrounding explanation.
Essentially we'd like to have the ability to "deep dive" into the Axiom
workspace, not only for debugging, but also for understanding what
functions are used, where they come from, what they inherit, and
how they are used in a computation.
To that end I'm looking at using McClim, a lisp windowing system.
Since the McClim windows would be part of the lisp image, they have
access to display (and modify) the Axiom workspace at all times.
The only hesitation is that McClim uses quicklisp and drags in a lot
of other subsystems. It's all lisp, of course.
These ideas aren't new. They were available on Symbolics machines,
a truly productive platform and one I sorely miss.
Tim
tools so that it would not get caught by "code rot" of libraries.
However, I'm also trying to make the new SANE version much
easier to understand and debug.To that end I've been experimenting
with some ideas.
It should be possible to view source code, of course. But the source
code is not the only, nor possibly the best, representation of the
ideas.
In particular, source code gets compiled into data structures. In Axiom
these data structures really are a graph of related structures.
For example, looking at the gcd function from NNI, there is the
representation of the gcd function itself. But there is also a structure
that is the REP (and, in the new system, is separate from the domain).
Further, there are associated specification and proof structures. Even
further, the domain inherits the category structures, and from those it
inherits logical axioms and definitions through the proof structure.
Clearly the gcd function is a node in a much larger graph structure.
When trying to decide why code won't compile it would be useful to
be able to see and walk these structures. I've thought about using the
browser but browsers are too weak. Either everything has to be "in a
single tab to show the graph" or "the nodes of the graph are in
different
tabs". Plus, constructing dynamic graphs that change as the software
changes (e.g. by loading a new spad file or creating a new function)
represents the huge problem of keeping the browser "in sync with the
Axiom workspace". So something more dynamic and embedded is needed.
Axiom source gets compiled into CLOS data structures. Each of these
new SANE structures has an associated surface representation, so they
can be presented in user-friendly form.
Also, since Axiom is literate software, it should be possible to look at
the code in its literate form with the surrounding explanation.
Essentially we'd like to have the ability to "deep dive" into the Axiom
workspace, not only for debugging, but also for understanding what
functions are used, where they come from, what they inherit, and
how they are used in a computation.
To that end I'm looking at using McClim, a lisp windowing system.
Since the McClim windows would be part of the lisp image, they have
access to display (and modify) the Axiom workspace at all times.
The only hesitation is that McClim uses quicklisp and drags in a lot
of other subsystems. It's all lisp, of course.
These ideas aren't new. They were available on Symbolics machines,
a truly productive platform and one I sorely miss.
Tim
Also of interest is the talk
"The Unreasonable Effectiveness of Dynamic Typing for Practical
Programs"
https://vimeo.com/74354480
which questions whether static typing really has any benefit.
Tim
"The Unreasonable Effectiveness of Dynamic Typing for Practical
Programs"
https://vimeo.com/74354480
which questions whether static typing really has any benefit.
Tim
http://pages.cs.wisc.edu/~remzi/Naur.pdf
In particular, it mirrors my notion that Axiom needs
to embrace literate programming so that the "theory
of the problem" is presented as well as the "theory
This article is, to my mind, the most accurate account
of what goes on in designing and coding a program.
I refer to it regularly when discussing how much
documentation to create, how to pass along tacit
knowledge, and the value of the XP's metaphor-setting
exercise. It also provides a way to examine a methodolgy's
economic structure.
In the article, which follows, note that the quality of the
designing programmer's work is related to the quality of
the match between his theory of the problem and his theory
of the solution. Note that the quality of a later programmer's
work is related to the match between his theories and the
previous programmer's theories.
Using Naur's ideas, the designer's job is not to pass along
"the design" but to pass along "the theories" driving the design.
The latter goal is more useful and more appropriate. It also
highlights that knowledge of the theory is tacit in the owning, and
so passing along the thoery requires passing along both explicit
and tacit knowledge.
Tim
In particular, it mirrors my notion that Axiom needs
to embrace literate programming so that the "theory
of the problem" is presented as well as the "theory
This article is, to my mind, the most accurate account
of what goes on in designing and coding a program.
I refer to it regularly when discussing how much
documentation to create, how to pass along tacit
knowledge, and the value of the XP's metaphor-setting
exercise. It also provides a way to examine a methodolgy's
economic structure.
In the article, which follows, note that the quality of the
designing programmer's work is related to the quality of
the match between his theory of the problem and his theory
of the solution. Note that the quality of a later programmer's
work is related to the match between his theories and the
previous programmer's theories.
Using Naur's ideas, the designer's job is not to pass along
"the design" but to pass along "the theories" driving the design.
The latter goal is more useful and more appropriate. It also
highlights that knowledge of the theory is tacit in the owning, and
so passing along the thoery requires passing along both explicit
and tacit knowledge.
Tim