On 04/11/17 16:18, Tim Daly wrote:
You're correct. My primary focus is on Spad code.
Tim,
Thanks for the explanation, interesting stuff, I'll be keen to read any
progress reports if you get time to write them.
Thanks, Martin B
___
You're correct. My primary focus is on Spad code.
In a logic setting there are things called Typeclasses which are roughly
equivalent to Axiom Categories. Typeclasses have 3 parts:
signatures-- just like Axiom
carriers-- Axiom's Domain representation
propositions -- formal
On 04/11/17 00:42, Tim Daly wrote:
On the other hand, my current effort involves proving Axiom correct. That
should (in theory) eliminate whole classes of errors. This is at the expense
of proving new code correct which tends to get a negative reaction from
developers.
Tim,
I know little
