--- Day changed Sat Mar 04 2017
rlyHas anyone ever written a production program in Agda/Coq/... of some non-trivial size? 04/03 18:07
{AS}rly: Have you seen CompCert?04/03 19:04
{AS}rly: In fact anything from https://deepspec.org/main04/03 19:05
rly{AS}: yes, but it's not complete. Also, it's written by the guy who wrote the tooling, so that's a bit unlikely to expect from a normal user.04/03 19:05
rly{AS}: deepspec is an academic thing, isn't it?04/03 19:05
{AS}rly: It's also used by industri/government as far as I understand04/03 19:06
rly{AS}: I see that now.04/03 19:06
{AS}rly: I mean https://deepspec.org/page/Industry/04/03 19:06
rly{AS}: yes, that sort of counts, but there is still heavy academic influence; it's not just some random startup who decided to use such tooling and build something.04/03 19:07
{AS}Sure, it's not your ordinary business solution04/03 19:07
rly{AS}: (which is not what I initially asked, I know).04/03 19:07
rly{AS}: but looking at what industry produces, perhaps it's not such an outrageous idea anymore.04/03 19:08
{AS}rly: Yeah, so really unfortunately that it's not something any off-the-shelf programmer can grab and program in04/03 19:08
{AS}really unfortunate* 04/03 19:08
rly{AS}: how much easier does Homotopy type theory make using a proof assistant for such developments?04/03 19:09
rly{AS}: I am convinced it's "the future", but not so much how much work it is to work without it and what it would mean for compatibility.04/03 19:09
{AS}rly: honestly, this is more an educational problem than a technological one04/03 19:09
{AS}I think the DeepSpec, Agda, Idris, etc. people are realizing that04/03 19:10
{AS}and they are in progress of improving it04/03 19:10
rly{AS}: would you say that Homotopy type theory is irrelevant to someone who wants to prove e.g. a file system to be correct today?04/03 19:11
{AS}rly: So someone did prove something about query equivalence in HoTT04/03 19:11
rly{AS}: i.e., the existence of an interpreter which would have native homotopy type theory support would not improve proof performance by more than a factor of 1.5.04/03 19:12
{AS}rly: I would not say it's irrelevant04/03 19:12
{AS}It makes many proofs easier04/03 19:12
{AS}(also many _mathematical_ proofs possible)04/03 19:12
{AS}rly: https://homotopytypetheory.org/2016/09/26/hottsql-proving-query-rewrites-with-univalent-sql-semantics/ <- is a good example for a programming use of HoTT04/03 19:13
{AS}performance is kind of an orthogonal issue04/03 19:14
{AS}As far as I understand even the computational model of all of HoTT is not properly understood yet04/03 19:14
rly{AS}: Cubical Type Theory seems to solve it.04/03 19:14
{AS}rly: It solves the univalence part04/03 19:14
rly{AS}: what part is missing?04/03 19:15
{AS}there is still some issues with HITs04/03 19:15
{AS}and propositional truncation etc.04/03 19:15
{AS}I am not an expert04/03 19:15
rly{AS}: ah, right.04/03 19:15
rly{AS}: I would say it's the first theory which sort of makes my head hurt.04/03 19:15
{AS}rly: have you seen Licatas ICFP 2016 presentation?04/03 19:16
{AS}it's really good04/03 19:16
rly{AS}: yes04/03 19:16
{AS}but yeah, it's too complicated even for me04/03 19:17
rly{AS}: I am a bit less enthusiastic by nature, but I would say it's the best presentation on the topic (there are not that many) and quite well done. 04/03 19:17
rly{AS}: Thorsten (or something like that) also did one, but he mixed up all kinds of symbols and didn't introduce notation in his lecture.04/03 19:17
{AS}rly: I am only familiar with Licata's presentation04/03 19:18
rly{AS}: "thanks for correcting me" is something I don't want to hear in a lecture by a *professor*.04/03 19:18
{AS}but I would guess that the other presentation was more for type theorists audience04/03 19:18
{AS}rly: That is what I want to hear from a professor04/03 19:18
{AS}it's better than pretending there is no issue04/03 19:18
rly{AS}: I don't mind that, but the point is that it shouldn't be needed in the first place.04/03 19:19
{AS}rly: people make mistakes, even professors :)04/03 19:19
rly{AS}: now, I also understand that it's not reasonable to blame him personally.04/03 19:19
{AS}it's not a big deal04/03 19:19
rly{AS}: it could be his governments funding program, or whatever.04/03 19:20
{AS}rly: really, it's OK to be wrong04/03 19:20
{AS}it's bad if you insist on being wrong04/03 19:20
{AS}but just being wrong is OK04/03 19:20
rly{AS}: what culture is that? ;)04/03 19:21
{AS}rly: it's not related to any culture04/03 19:22
{AS}but it's hard to expect people being perfect04/03 19:22
{AS}I am just saying that making a small mistake somewhere should not outweigh all the other good things04/03 19:23
rly{AS}: sure, I agree on that.04/03 19:23
rly{AS}: I actually think systems should be designed to cope with human imperfections.04/03 19:24
rly{AS}: thanks for the link.04/03 19:28
{AS}np04/03 19:28

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!