Conway's Law[0] basically says that software structure reflects
organizational structure.
In the youtube video[1] the argument is made that, despite evolving
organizational
changes, the old structure of software remains basically unchanged.
So it appears with Axiom. The Meta language was early
I know you all have better things to do with your life but ...
As I've mentioned too many times I'm trying to merge LEAN
proof technology with computer algebra (the SANE project in Axiom).
That involves proving algorithms.
LEAN currently seems more focused on straight math rather than
is good.
Tim
On Mon, Apr 3, 2023 at 6:32 AM Johann 'Myrkraverk' Oskarsson <
joh...@myrkraverk.com> wrote:
> Dear Tim,
>
> On Sun, Apr 2, 2023 at 5:35 PM Tim Daly wrote:
> >
> > > Moving forward with Axiom is going to be hard, and will probably have
>
Apr 2, 2023 at 2:49 AM Johann 'Myrkraverk' Oskarsson <
joh...@myrkraverk.com> wrote:
> Dear Tim,
>
> On Sat, Apr 1, 2023 at 10:22 AM Tim Daly wrote:
> [...]
> > I had hoped that Axiom could have been reborn as a literate program.
> > The idea was to "make it l
ay, there is The Long Now Foundation. They encourage long term
> thinking and preservation work. Maybe they can finance this project ?
> https://longnow.org/contact/
>
>
>
>
>
>
> So, why exactly it is not going to happen ?
>
>
> Best regards,
> Svjatoslav
&g
I just received the 4th edition copy of Physically Based Rendering[0].
Donald Knuth wrote "This book has deservedly won an Academy Award.
I believe it should also be nominated for a Pulitzer Prize."
It is a 1200 page literate program. It not only contains the actual
source code, it contains
t;working in public" is not helpful.
Axiom is still free and open source. The source will be
available at every release.
Tim
On Mon, Mar 6, 2023 at 6:08 PM Svjatoslav Agejenko
wrote:
> Hello !
>
> On Mon, 2023-02-13 at 14:42 -0500, Tim Daly wrote:
> > You'll notice that I'v
I want to synthesize and organize prior discussions into a research
statement.
Scratchpad was born as a research platform. Axiom is the commercial
version that was forcibly birthed due to IBM's business decisions. Axiom
has never been, and was not intended to be, a "commercial competitor
to
was not the problem.
The canonical place for Axiom's source code is github.
Thanks for your offer.
Tim
On Wed, Feb 15, 2023 at 12:34 AM Svjatoslav Agejenko <
svjatos...@svjatoslav.eu> wrote:
> Hello !
>
> On Tue, 2023-02-14 at 20:09 -0500, Tim Daly wrote:
> > Microsoft has made git
Camm,
The "next generation" of Axiom has a few goals that is significantly
reshaping the whole project. I call the effort SANE (a synonym of
rational, judicious, sound, rational). I gave a talk about it at Notre
Dame a few years ago (pre-covid).
There are two streams of mathematical development
David Stoutemyer published an article (p178) in BYTE magazine
in August 1979. He discussed Scratchpad. At the time I was still
at Unimation doing robot research. I published a robot article in
the February 1979 issue (p84).
d even a spiffy new cover!
Oh, and someone can actually read your explanation of your code.
Make Knuth happy! Win a Pulitzer prize!
Tim
On Sat, Dec 3, 2022 at 8:20 AM Tim Daly wrote:
> Java code has the pseudo-ability to re-generate the original source
> through decompilation. Unfort
r anticipated. I wonder what your colleagues will
> come up with.
>
> Thanks.
>
> -- Terence
>
>
> On Fri, 2 Dec 2022, Tim Daly wrote:
>
> > ...
> >
> > The above considerations leads me to the conclusion that the PDF is the
> > thing that generates code rather than the code generating the PDF.
>
rather than the code generating the PDF.
Tim Daly
http://axiom-developer.org/~daly
On Thu, Dec 1, 2022 at 10:00 PM Terence Kelly
wrote:
>
>
> Hi Tim,
>
> Thanks for your feedback, and for pointing me to Axiom.
>
> One "literacy" aspect of literate executabl
' is
(slightly) missing the fundamental point of literate software.
It is true that it keeps the code in sync with the executable and
keeps the code available for any given version. However, it
misses the fundamental literate point of 'Explanation'.
Tim Daly
http://daly.axiom-developer.org/~daly
[0] Axiom
Perhaps I wasn't clear.
I've sent a note to the Schmidt Futures project requesting Axiom support.
They have not yet replied. There is no agreement in place.
Tim
On Tue, Jul 19, 2022 at 4:35 PM Svjatoslav Agejenko <
svjatos...@svjatoslav.eu> wrote:
>
> Hello !
>
> > Financing isn't the real
m
On Mon, Jul 18, 2022 at 11:15 PM Svjatoslav Agejenko <
svjatos...@svjatoslav.eu> wrote:
> Hello !
>
> On Mon, 2022-07-18 at 11:56 -0400, Tim Daly wrote:
> > One early Axiom project question was how to keep Axiom
> > alive after the project lead dies (aka me). Almost all pro
Clifford,
My research is on self-reproducing systems (SRP). Specifically I am trying
to build
a robot / 3D printer combination that can (a) make two copies of itself and
then
(b) forage for materials that can be used by those copies to make two
copies.
The idea is that this leads to exponential
As most of you know, I'm deeply involved in not
only Axiom research, but also self-reproducing robots.
One early Axiom project question was how to keep Axiom
alive after the project lead dies (aka me). Almost all projects
die once the lead developer stops developing. Since Axiom
is so complex it
An interesting idea is what I'd call "proof specificity".
The motivation is to prove that certain classes of bugs
cannot occur. Or, more generally, that certain classes of
behavior cannot occur.
At a very low level there could be a proof that the stack
size is bounded.
A slightly higher level
Even cubical type theory might not
> be foundational?
>
> Do you think that dynamic types and/or the sort of self modifying
> programs you are suggesting are necessary to model all of mathematics?
>
> These videos are 4 years old, do you know if this research has come to
> any conclus
Well, SANE is certainly turning into a journey.
When we look at the idea of first-class dependent types
as implemented in languages like Agda and Idris we find
what I call "peano types". For example, Fin is a type
of "finite numbers", usually defined as
data Fin : Nat -> Type where
FZ : Fin (S
I've been living with Axiom's code now since the 1980s,
a portion of which I've authored or, at least, rewritten.
The code was written by some truly clever people (and
I'm not one of them). The parser, written by Bill Burge,
uses a "zipper" technique. It is quite clever and absolutely
opaque.
beginning to think that the key flaw in Godel's 2 theorems
is that they don't take self-reference and self-modification into
account. At this point it's just not clear to me how to express
self-reference and self-modification in Godel numbering.
... [snip] ...
Tim
On Wed, Apr 27, 2022 at 9:22 A
... [snip] ...
I guess that's where we differ. Axiom is a piece of research software.
Axiom was never intended to be a product. IBM gave us two choices. Either
find someone to market it (NAG) or throw it away. FOSS software did
not exist at that time and we were not allowed to work on it in any
I tried to push some changes to github and failed.
It appears I'm unable to update Axiom.
Leave it to Microsoft to screw up something that
worked for over a decade.
Sigh.
Tim
beit in a tactic language.
For example, a "reduce" tactic would apply a function to a
set of numbers (symbolically), with the proof condition that
the set is finite and the generated index decreases so we
can know that "reduce" terminates. That would then be
equivalent to the Lisp
to the success of the OpenAI Codex more
> than anything else, but the results are impressive.
>
> Bartosz Piotrowski, a PhD student and author of one of the papers you
> cited, will be visiting Carnegie Mellon for a few months this spring.
>
> Best wishes,
>
> Jeremy
>
&
This is an interesting paper (especially given that it
is work under Gilbert Strang):
A Neural Network Solves and Generates Mathematics
Problems by Progam Synthesis: Calculus, Differential
Equations, Linear Algebra, and More.
https://arxiv.org/pdf/2112.15594.pdf
"This work shows that a neural
A Neural Network Solves and Generates Mathematics
Problems by Progam Synthesis: Calculus, Differential
Equations, Linear Algebra, and More.
https://arxiv.org/pdf/2112.15594.pdf
Axiom allows the user to dynamically create dependent types.
For example, matrix(3,3) is a 3x3 matrix. This may
seem trivial but it is not.
Consider that to construct the "domain" (as it is called
in Axiom) of 3x3 matrices you need to evaluate the
arguments. Again, in this case it is trivial but,
age to their problem.
A simple paper on the subject is "Metaobject Protocols"
https://users.cs.duke.edu/~vahdat/ps/mop.pdf
Tim
On Mon, Oct 25, 2021 at 7:42 PM Tim Daly wrote:
> I have a separate thread of research on Self-Replicating Systems
> (ref: Kinematics
intermediate steps.
Having the intermediate steps also allows proofs to be
inserted in a step-by-step fashion. This aids the effort to
have proofs run in parallel with computation at the hardware
level.
Tim
On Thu, Oct 21, 2021 at 9:50 AM Tim Daly wrote:
> So the current struggle involves
ot;
applies to the resulting object. Proofs depend on their
assumptions which might be different for different
constructions. As yet I have no clue how to "index"
proofs based on their assumptions, nor how to
connect these assumptions to the groupoid structure.
My brain hurts.
Tim
O
e problem is no longer "the tools".
*I* am the problem constraining the solution.
Birthing this "new thing" is slow, difficult, and
uncertain at best.
Tim
[0] Alexander, Christopher "Notes on the Synthesis
of Form" Harvard University Press 1964
ISBN 0-674-62751-2
On Sun, O
tioned in any recent bibliography.
https://mitpress.mit.edu/books/parallel-distributed-processing-volume-1
On 9/27/21, Tim Daly wrote:
> Greg Wilson asked "How Reliable is Scientific Software?"
> https://neverworkintheory.org/2021/09/25/how-reliable-is-scientific-software.ht
t is nonrandom" (i.e., the
authors of different packages make similar mistakes).
On 9/26/21, Tim Daly wrote:
> I should note that the lastest board I've just unboxed
> (a PYNQ-Z2) is a Zynq Z-7020 chip from Xilinx (AMD).
>
> What makes it interesting is that it contains 2 hard
> cor
combined in a single chip.
That means that my effort to run a proof checker on
the FPGA and the algorithm on the CPU just got to
the point where coordination is much easier.
Now all I have to do is figure out how to program this
beast.
There is no such thing as a simple job.
Tim
On 9/26/21, Tim Daly
ivial, out of date, and incomplete.
I'm clearly not smart enough to prove the Risch
algorithm and its associated machinery but the needed
definitions and theorems will be available to someone
who wants to try.
[0] https://github.com/daly/PDFS/blob/master/bookvolbib.pdf
On 8/19/21, Tim D
OWS) make a PowerShell desktop
https://superuser.com/questions/886951/run-powershell-script-when-you-open-powershell
Tim
On 8/13/21, Tim Daly wrote:
> A great deal of thought is directed toward making the SANE version
> of Axiom as flexible as possible, decoupling mechanism from theory.
>
ut duplication.
Tim
[0], Smith, Brian Cantwell "Reflection and Semantics in LISP"
POPL '84: Proceedings of the 11th ACM SIGACT-SIGPLAN
ymposium on Principles of programming languagesJanuary 1
984 Pages 23–35https://doi.org/10.1145/800017.800513
On 6/29/21, Tim Daly wrote:
> Having spent tim
could just be another
service node. In fact, any "foreign function" could transparently
cooperate in a distributed Axiom.
Another key feature is that proofs can be "by node".
Tim
On 6/5/21, Tim Daly wrote:
> Axiom is based on first-class dependent types. Deciding when
> two
odel for generated code.
I think Bob Harper had a NuPRL-like effort at some point. I vaguely
remember mention of an effort at code generation. That was long
ago so my memory is likely faulty and I don't remember the name
of his effort.
Anyway, LEAN code generation is an important step in the
Axiom SANE r
26/21, Jeremy Avigad wrote:
> Thanks for pointing this out to me -- I had heard about it. The Scholze
> post was huge for us.
>
> Best wishes,
>
> Jeremy
>
>
> On Sat, Jun 26, 2021 at 5:47 PM Tim Daly wrote:
>
>> Andrej Bauer gave an extraordinarilly clear talk
>
ow much effort it takes to get my current
research working I can safely estimate that self-modifying
FPGAs are at least a few weeks in the future :-)
Tim
On 6/17/21, Tim Daly wrote:
> Camm,
>
> Greetings, as you say...
>
> That would save me a lot of effort. At the moment I've been
&
ion pertains to the same platform as
> Debian's 'riscv64'. There are virtual machine images which can be run
> in emulation, but I have been waiting for a porterbox to become
> available to port gcl. I anticipate the linker will just take a few
> days.
>
> Take care,
>
> T
the detailed explanation, Tim. That's very helpful.
> -Jeff
>
> --
> Jeff Scheel (he/him/his)
> Linux Foundation, RISC-V Technical Program Manager
>
>
> On Thu, Jun 10, 2021 at 7:25 PM Tim Daly wrote:
>
>> I'm the lead developer on Axiom, a computer alg
types has to export a function to decide if a
given type is "equivalent" to itself.
The notion of "equivalence" might involve category ideas
of natural transformation and univalence. Sigh.
That's an interesting design point.
Tim
On 5/5/21, Tim Daly wrote:
> It is i
Tim,
I just watched your Symbiflow video.
https://www.youtube.com/watch?v=-xyAauPa__s
My first question is: I saw you had an Axiom t-shirt.
What does it refer to? Clearly not the Axiom project :-)
I'm Tim Daly, project lead on Axiom, an open source
computer algebra project:
https
I'm working on circuit construction and found the tool nMigen
https://m-labs.hk/gateware/nmigen/
nMigen is a Python toolbox for building complex digital hardware.
nMigen offers Bounded Model Checking and formal
verification tool checkers for circuits.
You can, for example, guarantee that a
ng to be a real advance over IDE
style programming and "raw code" programming.
Tim
On 2/27/21, Tim Daly wrote:
> The systems I use have the interesting property of
> "Living within the compiler".
>
> Lisp, Forth, Emacs, and other systems that present themselve
representation properties.
There is no such thing as a simple job. :-)
Tim
On 2/18/21, Tim Daly wrote:
> 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 cod
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
On 2/5/21, Tim Daly wrote:
ll 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
On 1/19/21, Tim Daly wrote:
> Also of i
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
On 1/19/21, Tim Daly wrote:
> Peter Naur wrote an article of interest:
> http://p
Peter Naur wrote an article of interest:
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
of the solution". I quote the introduction:
This
stance objects that exist both at compile time
and at run time (since types, including new categories,
can be constucted at run time).
Tim
On 1/1/21, Tim Daly wrote:
> One of the struggles of working with first-class dependent types
> is that they can be created "on the fly".
al Evaluation, which used the type information
to collapse and specialize a function.
Jones, Gomard, and Sestoft "Partial Evaluation and Automatic
Program Generation" (1993) Prentice Hall
On 12/31/20, Tim Daly wrote:
> It's been a long, slow effort to "get up to spee
It's been a long, slow effort to "get up to speed" (or more
accurately "a slow crawl") on the various subjects one needs
to know to work on "computational mathematics" aka SANE.
A reading knowledge of a lot of areas is needed, including
things like
abstract algebra (to understand Axiom's
of Lean's Type
Theory, deriving functors that fulfill all the definitions
using things like Axiom's group theory structure, and
inventing the verification language V rich enough
for both needs.
It's gonna be a long winter :-)
Tim
.
On 12/18/20, Tim Daly wrote:
> Quoting Dijkstra (1988, EWD10
are
asked to provide an algorithm and an associated proof.
Will you get hired?
Dijkstra saw this in 1988 and it's taken me decades to
hear and understand.
Tim
On 12/18/20, Tim Daly wrote:
> I occasionally get grief because Axiom is implemented
> in Common Lisp. People don't seem to like that f
I occasionally get grief because Axiom is implemented
in Common Lisp. People don't seem to like that for some
odd reason. Lisp, one of the easiest languages to learn,
seems to be difficult to accept.
I'm working with John Harrison's book "Practical Logic
and Automated Reasoning" from 2009. It
ion of Axiom.
Progress, albeit glacial, is being made.
Tim
On 12/3/20, Tim Daly wrote:
> HILL CLIMBING
>
> I really encourage you to read the slides:
> Vladimir Voevodsky. Univalent foundations, March 2014. Presentation at
> IAS,http://www.math.ias.edu/~vladimir/S
do better.
We must. And as a consequence we elevate "computer algebra" to
"computational mathematics", surely a worthwhile research goal.
Tim
On 12/3/20, Tim Daly wrote:
> I just ran across an interesting example about the difference
> between testing and proving (not t
this out.
Tim
On 11/29/20, Tim Daly wrote:
> Axiom, as it was released to me long ago, is being
> overtaken by current technology.
>
> I'm taking an MIT course on "Underactuated Robots" [0]
> (I spent a large portion of my life doing robotics).
>
> The instru
ld
be a great help if, for instance, you wanted a Groebner
basis solution and Axiom could provide an "answer". It would
be SO much better if the computer algebra algorithm
came back with the associated proof.
We seem to be working toward a common goal, that
of "computational mathematics". Hopefully we will
"meet in the middle".
Please, please, please video your courses.
Stay healthy. Keep up the good fight.
Tim Daly
eads to the dustbin of history.
Tim
[0]
https://www.youtube.com/watch?v=GPvw92IKO44=UUhfUOAhz7ynELF-s_1LPpWg=28
On 11/27/20, Tim Daly wrote:
> The current mental struggle involves properly re-constructing
> Axiom so Category Theory (e.g. objects, morphisms, identity,
> and compos
otocol [2].
[0] https://www.youtube.com/user/youdsp/playlists
[1] https://github.com/digama0/lean-type-theory/releases/download/v1.0/main.pdf
[2] https://mitpress.mit.edu/books/art-metaobject-protocol
Tim
On 11/10/20, Tim Daly wrote:
> Another area that is taking a great deal of time a
and a
specification language syntax is not yet decided.
Tim
On 10/9/20, Tim Daly wrote:
> A great deal of thought has gone into the representation
> of functions in the SANE version.
>
> It is important that a function lives within an environment.
> There are no "stand alo
A great deal of thought has gone into the representation
of functions in the SANE version.
It is important that a function lives within an environment.
There are no "stand alone" functions. Given a function
its environment contains the representation which itself
is a function type with accessor
I'm writing a book on the history of Axiom. As part of
that effort I'm reviewing all of the emails posted to the
mailing list. I came across this posting by Scott Morrison,
the author of the interpreter:
Date: Thu, 3 Nov 2005 08:34:55 -0800
From: Scott Morrison
To: list
Subject: Re: BAD tim
I did a git clone git://git.sv.gnu.org/gcl.git
cd gcl/gcl
./configure
make
... and it failed on Ubuntu 1404 and 2020.04
The failing console is attached.
Tim
FAILED
Description: Binary data
Hill Climbing
Almost every possible step along the path to creating
the SANE version of Axiom involves a LOT of hill
climbing, by that I mean a LOT to learn to get started.
Axiom was built with a scaffold of group theory which
makes it easier to reason about and understand. Going
forward we
My apologies. I reacted poorly to what I
interpreted as a criticism of the developers of
Scratchpad. I consider them among the most
clever and intelligent people I've ever met. I was
lucky to work with them.
Tim
(https://groups.google.com/g/fricas-devel/c/lF4w9MduSVg)
-- There is quality called "cohesion" or "conceptual
-- integrity" meaning that parts of system follow common
-- design and compose into coherent whole. I could list
-- rather long list of design choices made in Axiom time
-- that I am not
fic
> computation system. Or is it?
>
> William
>
> William Sit
> Professor Emeritus
> Department of Mathematics
> The City College of The City University of New York
> New York, NY 10031
> homepage: wsit.ccny.cuny.edu
>
> __
Today's Headline:
Axiom finalizing agreements for private astronaut mission to space station
https://spaceflightnow.com/2020/09/23/axiom-finalizing-agreements-for-private-astronaut-mission-to-space-station/
Wow. I HAVE been busy :-)
Tim
On 9/24/20, Tim Daly wrote:
> Ricardo,
>
>
th axiom, so maybe
> connecting through it serves like a bridge.
>
> On Thu 24 Sep 2020 at 0:06 Tim Daly wrote:
>
>> The new Axiom version needs to have a better user interface.
>>
>>
>>
>> I'm experimenting with a browser front end that has an Axiom
>
is already in hyperlinked PDF
files it will be possible to jump directly to related sections
in the various books.
Tim
On 9/23/20, Tim Daly wrote:
> Rich Hickey gave a keynote:
> https://www.youtube.com/watch?v=oyLBGkS5ICk
> which, like all of Hickey's talks, is worth watching.
>
>
sion 1.2.3)
is meaningless.
I realized this years ago and changed Axiom to use
the date of the release. It provides the same sort of
"non-information" but it is easy to find in the changelog.
Tim
On 9/5/20, Tim Daly wrote:
> Geometric algebra also affects another "in-process"
metric Algebra means that some of the
errors, such as roundoff, cannot occur in the symbolic form.
This has the potential to make Axiom's BLAS and LAPACK
computations faster and more accurate.
Tim
On 9/5/20, Tim Daly wrote:
> I'm in the process of re-architecting Axiom, of course.
>
> T
speaking, of leading to completely different
> conclusions than those that are obtained from theorems
> which have been deduced from the accepted axioms.
> The longer and fancier is the chain of deductions
> ("proofs"), the less reliable is the final result.
>
> https://w
and fancier is the chain of deductions
("proofs"), the less reliable is the final result.
https://www.uni-muenster.de/Physik.TP/~munsteg/arnold.html
On 8/8/20, Tim Daly wrote:
> Mark,
>
> You're right, of course. The problem is too large.
> So what. is the plan to ach
Mark,
You're right, of course. The problem is too large.
So what. is the plan to achieve a research result?
There are 3 major restrictions on the effort (so far).
First, the focus is on the GCD in NonNegativeInteger.
Volume 13 is basically a collection of published thoughts
by various authors
I did a survey of a couple hundred papers from the computer
algebra and proof camps. The only person mentioned in both
bibliographies on a regular basis seems to be James Davenport.
All attempts at combining the systems seems to be either a
simple cover (e.g. a simple front-end on Mathematica) or
I'm Tim Daly, lead developer on Axiom, a computer algebra
system developed by IBM, which is now open source.
http://axiom-developer.org
https://en.wikipedia.org/wiki/Axiom_(computer_algebra_system)
http://daly.axiom-developer.org
I read your paper and watched your video with great interest
red equal (unless there is a
> problem with computing the LCM of denominators of the coefficients).
>
> William
>
> William Sit
> Professor Emeritus
> Department of Mathematics
> The City College of The City University of New York
> New York, NY 10031
> home
of a program and you can regenerate the
program from the proof, are the proof and program equal?
Presumably the chap behind the SANE effort will be
able to handle both kinds of equality (as well as giving
universes for types).
But I suspect he's not that clever.
On 7/21/20, Tim Daly wrote:
>&g
these days? After all, nearly three decades have
> passed.
>
> William
>
> William Sit
> Professor Emeritus
> Department of Mathematics
> The City College of The City University of New York
> New York, NY 10031
> homepage: wsit.ccny.cuny.edu
>
> _
ps solved. In that case, please ignore
> them and just tell me so.
>
> William
>
> William Sit
> Professor Emeritus
> Department of Mathematics
> The City College of The City University of New York
> New York, NY 10031
> homepage: wsit.ccny.cuny.edu
>
> ___
William
>
> William Sit
> Professor Emeritus
> Department of Mathematics
> The City College of The City University of New York
> New York, NY 10031
> homepage: wsit.ccny.cuny.edu
>
>
> From: Axiom-developer
> on behalf of
> Tim D
r documentation,
are all "nice to have" but, as Hamming would say,
they are not "the most important problem".
Tim
On 7/2/20, Tim Daly wrote:
> Time for another update.
>
> The latest Intel processors, available only to data centers
> so far, have a built-in FPG
; I seem to remember that you had something to do with "AXIOM" ;-)
>
> The AXIOM algebra source could be one component of the prospective project.
> Did you see the "Foundations" post?
>
> What times are good for calls?
>
> Cheers, Gene
>
>
> On 6
of it succeed, it changes computational mathematics.
Tim
"A person's reach should exceed their grasp,
or what's a computer for?" (misquoting Robert Browning)
(https://www.quotetab.com/quote/by-robert-browning/ah-but-a-mans-reach-should-exceed-his-grasp-or-whats-a-heaven-for)
On 6
sophisticated techniques that, even today, are
beyond the capabilities of the compiler.
On 3/24/20, Tim Daly wrote:
> I've spent entirely too much time studing the legal issues
> of free and open source software. There are copyright,
> trademark, and intellectual property laws. I have read
> s
Wittgenstein’s famous thought experiment, the
open source ‘beetle in a box’ can represent different
things to different people, bearing interesting fruit for
philosophers and software creators alike.
http://itc.conversationsnetwork.org/audio/download/itconversations-1502.mp3
On 3/7/20, Tim
to us
mortals) have built-in FPGAs so it would be possible to
"side-load" a proof of a program to be checked while the
program is run. I have the FPGA and am doing a gate-level
special instruction design for such a proof checker.
On 2/7/20, Tim Daly wrote:
> As a mathematician, it
puters, just not in my lifetime. That's ok. When I
started programming there was no computer science degree.
Somebody has to be the first lemming over the cliff.
Tim
On 1/9/20, Tim Daly wrote:
> When Axiom Sane is paired with a proof checker (e.g. with Lean)
> there is a certain amount
/20, Tim Daly wrote:
> Provisos that is, 'formula SUCH pre/post-conditions'
>
> A computer algebra system ought to know and ought to provide
> information about the domain and range of a resulting formula.
> I've been pushing this effort since the 1980s (hence the
&g
.
Trust "down to the metal".
Tim
On 12/15/19, Tim Daly wrote:
> Progress in happening on the new Sane Axiom compiler.
>
> Recently I've been musing about methods to insert axioms
> into categories so they could be inherited like signatures.
> At the moment I've been thi
1 - 100 of 491 matches
Mail list logo
