--- Day changed Sun Jan 28 2018
srpxIs agda’s codebase modular? Would it be feasible to separate the core language, make my own ascii syntax and ship it with the typechecker on a project?28/01 14:27
pgiarrussosrpx: I’ve often read type theorists note that Agda does not have a real kernel28/01 15:24
pgiarrussoand that its codebase is much bigger than, say, Idris28/01 15:24
pgiarrussoI’m not familiar enough to know what it means28/01 15:24
srpxoh :(28/01 15:24
srpxOk hmm28/01 15:25
pgiarrussoI heard 300 KLoC vs 10-20 KLoC, but please verify28/01 15:25
pgiarrussoI’ve read similar comments by Conor McBride28/01 15:25
srpxIf someone could link me to an human explanation on how I could implement a core language with inductive types I’d be thankful. I understand there is no simple thing like that, but whatever is the simplest, then...28/01 15:25
pgiarrusso*also*, people keep saying that *Coq* has a small kernel and passes the deBruijn criterion28/01 15:25
srpxdeBruijn criterion?28/01 15:26
pgiarrussoyou have proof certificates that can be checked by a small kernel28/01 15:26
pgiarrussoso you don’t have to trust the rest of the codebase28/01 15:26
pgiarrussosay, Coq’s tactics can have bugs, but they’ll be caught!28/01 15:27
pgiarrussobecause they produce terms that are checked by the kernel28/01 15:27
srpxI see28/01 15:29
pgiarrussosrpx: also, what was the problem with Cedille? Just that you haven’t found a tutorial implementation?28/01 15:29
srpxSo perhaps my best bet is to use coqs kernel with my own little syntax layer without all the tactics and whatever else28/01 15:29
pgiarrussoeither that or Idris28/01 15:30
srpxPgiarusso mostly that I didn’t have time to look it deeper as I’m jumping through so many options, so yes, if you’re sure it is the right way to go I could try28/01 15:30
pgiarrussosure? not28/01 15:31
pgiarrussoalso, it’s researchier28/01 15:31
srpxIdris has some issues, its compiler is way too slow for the kind of thing I have in mind, its syntax has too many things for me to build an editor for, etc... but it is an option too, I’m just not sure28/01 15:31
pgiarrussonot sure how many of those are with the kernel though28/01 15:32
pgiarrussoalso^2, not sure if you need dependent types or just a theorem prover28/01 15:32
pgiarrussothe first interactive theorem provers come from decades ago, and they were probably simpler28/01 15:33
pgiarrussoregarding tutorials, one is https://www.andres-loeh.de/LambdaPi/LambdaPi.pdf (not sure if it has inductive types)28/01 15:33
pgiarrussothere’s also http://math.andrej.com/2012/11/08/how-to-implement-dependent-type-theory-i/ and the two follow-ups28/01 15:34
srpxI need to be able to download proofs about programs my users access on the browser. Downloading types like “for all sequence of transactions this contract state never violates zero sum of balances” is the way I know how to do it. How else?28/01 15:34
srpxSorry for grammar, I’m on my phone /\28/01 15:34
srpxThanks for the links!28/01 15:34
pgiarrussoOK, so you indeed need proof certificates28/01 15:34
pgiarrussobecause (it sounds like) you want to implement proof-carrying code28/01 15:35
pgiarrusso(which I linked you to earlier)28/01 15:35
pgiarrussoback then, Appel used a subset of LF to minimize the trusted kernel, but LF has proof-theoretic limitations and I don’t know if it can state/prove the properties you care for28/01 15:36
srpxPgiarusso if I remember well that first tutorial doesn’t explain how to implement user-defined inductive types, no? It just extends the core itself with nats and vectors28/01 15:37
pgiarrussosrpx: “jumping through too many options” also sounds plausible28/01 15:38
pgiarrussosrpx: I don’t know, might be28/01 15:38
srpxHmm28/01 15:38
pgiarrussoand I understand from Cedille that’s because inductive types are hard28/01 15:38
srpxHmmm yea28/01 15:39
pgiarrussosrpx: if you want to use dependent types (which is reasonable), I’d try using Idris or Coq.js28/01 15:39
pgiarrussoif both are too big28/01 15:40
pgiarrussoyou should maybe then practice on that tutorial and then try going to Cedille28/01 15:40
pgiarrussosrpx: did I link you to https://github.com/Toxaris/pts/ ? That can typecheck programs in various PTSs (without inductive types)28/01 15:41
srpxOf all the options, if you had to implement a browser except that instead of JS, its native app language had types which could be downloaded to prove properties about its programs, what would you personally do? Write your own core based on cedille or similar, use full Idris/Agda/coq or what?28/01 15:41
srpxPgiarusso not yet, let me see28/01 15:42
pgiarrussosrpx: proof-carrying code sounds closest28/01 15:42
pgiarrussohonestly, if I wanted to do that and didn’t have a PhD, I’d try to start one under a suitable advisor28/01 15:43
srpxAbout that last link, no read me? Am I missing something?28/01 15:43
pgiarrussosrpx: you mean there’s missing info in the README? It’s right there28/01 15:43
srpxOh turns out I can’t use this phone sorry28/01 15:43
srpxYep28/01 15:43
pgiarrussoor at least, I’d try doing it as a master thesis, again under the right advisor28/01 15:44
pgiarrussoand ask them to figure out if the project size is feasible28/01 15:44
pgiarrussobut you should ask somebody who’s qualified because they wrote such a kernel, or close enough28/01 15:45
srpxThat is what I have though, right? Problem is adding inductive families to that28/01 15:45
pgiarrussonot just somebody (me) who has free time and knows quite a few pointers :-)28/01 15:45
srpxMakes sense, perhaps I should look for people who wrote those and mail them28/01 15:45
srpxgreat pointers by the way, thanks (:28/01 15:46
pgiarrussocstheory or cs .sx might be more appropriate28/01 15:47
pgiarrussoor the thesis route28/01 15:47

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