4 ms·
What I couldn't find was an answer to the question "why?" I could see this being an interesting basis for teaching Computer Science in high schools, where a te
by nmrm2 11y ago
What I couldn't find was an answer to the question "why?"
I could see this being an interesting basis for teaching Computer Science in high schools, where a text like this functions in a way similar to Euclid in high school Geometry courses. I'm pretty sure there aren't any non-exceptional examples of high school Computer Science courses (e.g., the AP CS course is better described as an Intro to Computer Programming course).
And in any case this is a nice exposition.
But aside from that, I'm not sure I see any new insights here about CS/verification, nor any suggestions for research directions that aren't already extensively explored. Perhaps I'm missing something, though.
(Edit: There's a list of suggested future work at the end of the paper. I guess I get it now; although all of these things have been done in verification/PL -- and even by non-type-theorists -- they almost always involve the development of a new logic, and aren't done in pure set theory. So certainly there's a lot of work to do if you want to do things in this style. But I'm still trying to see the benefit of this style, aside from pedagogic or philosophical benefits. Is my inexperience in this area blinding me from some obvious potential? I don't know much about non-high-school set theory.)
- AnimalMuppet 11y agoBuilding a unified framework for all of programming theory is useful, even if it provides no new insights. It provides a clearer basis for thinking about what we already know, and thereby makes the new insights easier. So even if the new insights aren't here yet, it makes it more likely that they eventually come.
- nmrm2 11y agoI guess my question is, why set theory, as opposed to building [new] logics on top of other semantic models (e.g. operational semantics or reachability relations)? (I don't doubt there are compelling reasons, I just don't know enough about set theory or programming theory to know what they are. Other than the clear benefit of this approach over others in "elementary" educational settings, e.g. US high schools)
- AnimalMuppet 11y agoLowest total cognitive load? That is: If I build my theory on a complicated foundation, then you have to learn the complicated foundation before you can even start to learn my theory. On the other hand, if I build it on a simple foundation, but that simple foundation means that the theory itself has to jump through a bunch of hoops because the foundation is too simple, that can also make the total (foundation + theory) harder to learn and understand. So the sweet spot is to use the simplest foundation that does not unduly complicate the theory. (And that may change, depending on target audience.) Is set theory the best answer? I have no idea, but all of programming in 28 pages, built on a foundation only of set theory, is very impressive.
- nmrm2 11y agoThanks for your responses. I think I'm expecting interesting and impactful results out of an exposition/proposal, which is probably unreasonable. > but all of programming in 28 pages, built on a foundation only of set theory, is very impressive Yes, it is :-)