1.3 Foundational choices and their influence on design/coding choices

williamdemeo commented 2 years ago

(The 1.3 label in the title of this issue is a reference to point 3 from the 1st referee report.)

In the introduction (e.g. 3rd ¶) and §2.1, we claim to take great care with foundational aspects. Further explanation of the following would make clearer the relevance of our work:

(a) How does this attention to foundational details affect our coding choices?
(b) What's the difference from the foundational view-point between our code and work cited in sect.7?
(c) At start of §2.2, our claims about setoids seem a bit bold (or "gnomic"). We don't cite work on the so-called "setoid hell", and we miss the point of the bad reputation of setoids. Referee asserts: setoids do not make implementation tedious, but, in a sense, unnatural wrt informal mathematical practice, since any setoid-based reasoning depends on specific implementation details. Some parts of our code (omitted from the paper) suffer from these aspects of using setoids.

(wd: I made an first attempt to address point c in the latest PR)

JacquesCarette commented 2 years ago

Ack. that this is on my plate.

JacquesCarette commented 2 years ago

Hmm, I'm not quite sure where I should discuss this. Also "any setoid-based reasoning depends on specific implementation details" is not something I believe is true! I'm not going to address that bit at all, as I'd need an example. Lastly, I have no idea what work to cite wrt this.

williamdemeo commented 2 years ago

You are mildly alarmed or dismayed that this is on your plate? (I had to look up "Ack" :)

Fair enough. I think what you said in your second comment is reasonable. I suspect we could get away with saying something like that in our response to the referees in order to justify leaving the paper as is (with respect to this).

JacquesCarette commented 2 years ago

I keep forgetting your main education is all math, so some oft-used CS lingo (like Ack as a short-form for aknowledged, which comes from low-level network protocols) is mysterious.

I am neither dismayed nor alarmed that this is on my plate. Once I looked into it some more, I came up empty-handed as to where to actually address it! I'd be happy to only address in referee response.

williamdemeo commented 2 years ago

I was going to close this, but I'll leave it open, in case we want a reminder that JC's nice comments about this could go in Sec 7.

ualib / agda-algebras

1.3 Foundational choices and their influence on design/coding choices #190