[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [Axiom-developer] Proving Axiom Correct

From: Raymond Rogers
Subject: Re: [Axiom-developer] Proving Axiom Correct
Date: Sat, 01 Aug 2015 12:45:44 -0400
User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.8.0

Great!  Actually this list makes a great dictionary for me :)

Might I suggest opening an axiom-developer forum where discussions about different categories, proofs, and typos can be addressed individually? And perhaps a prefered format for the signatures along the ideas of input-process-output as blocks together with a "lint" and cross reference program. Even with the correct semantic,s syntax/form can still make things unmaintainable; I know I have done it. Written perfectly correct code/mathematical solutions that totally mystified me later.


On 07/31/2015 07:22 PM, address@hidden wrote:
I've collected all of the functions that are implemented at the
category level. For each function I've prepended the signature.  These
chunks are automatically extracted during build and collected into a
file in the obj/sys/proofs subdirectory. The file has been uploaded to

The file consists of a single COQ Module named Jenks.
Each category and its asssociated functions are comments in the file.
The categories in the file are arranged so that more primitive
categories occur before categories that inherit from them.

The next stage is to begin proving these algorithms correct using COQ.
Each proven function will be uncommented, along with its associated proof.


Axiom-developer mailing list

reply via email to

[Prev in Thread] Current Thread [Next in Thread]