Lessness (Jul 15 2022 at 15:41): Lessness (Jul 15 2022 at 15:41):I've decided to make a Patreon account. More for fun than for profit, please don't judge. :sweat_smile:
Ideas to do there:
1) To keep doing Euler Project problems (the first 100, of course) - verifying C code that solves them. It takes time and brain though, and I'm stuck with the 3rd exercise right now.
2) Slowly start/continue to read and work for my bachelor thesis (and talk about that etc. on Patreon). (See https://coq.zulipchat.com/#narrow/stream/237655-Miscellaneous/topic/Coq.20and.20statistics.20-.20any.20suggestions.20for.20bachelor.20thesis.3F)
3) Do model theory in Coq (I have wanted to do that for some long time), because it seems like an ignored topic. (Only thing I found is this: https://arxiv.org/abs/2104.14445)
4) Make formally verified algorithms in C, using VST and some textbook as guide. A variation of the 1).
Which one do you like the best? Any other suggestions?
P.S. 1) and 4) could be impossible/forbidden without acquiring a licence for that. Because on Patreon that becomes commercial use, I believe.
Karl Palmskog (Jul 15 2022 at 16:07):hmm, I thought the non-commercial part for CompCert+VST was mostly related to clightgen. It seems unlikely that taking an already-defined Clight syntax tree in Coq and expressing+proving properties in VST about it violates the CompCert license just because there is a "donate" button somewhere in the GitHub repo. But I didn't study the license in detail.
Paolo Giarrusso (Jul 15 2022 at 16:16):IANAL. Here’s what https://github.com/AbsInt/CompCert/blob/master/LICENSE says; I’m tempted to leave the interpretation to a lawyer:
Limitations on Use: The License is limited to noncommercial
use. Noncommercial use relates only to educational, research,
personal or evaluation purposes. Any other use is commercial use.
You may not use the Software in connection with any activities
which purpose is to procure a commercial gain to you or others.
Karl Palmskog (Jul 15 2022 at 16:19):I think this is more about the use of the actual compiler (which is not required for verification in VST). I think the VST license stuff is more informative: https://github.com/PrincetonUniversity/VST/blob/master/LICENSE
All parts of the VST opam distribution, (make target "vst"), (including msl, sepcomp, veric, floyd, concurrency) and the VST test suite (including progs, progs64, sha, hmacdrbg, hmacfcf, aes) are licensed by the BSD 2-clause license (below).
The github repo contains certain subdirectories, not distributed
in the opam package, that are licensed differently:
- The "compcert" subdirectory is Copyright (c) 2004-2013 by INRIA,
and licensed according to the terms in "compcert/LICENSE";
basically, those files are dual licensed with a proprietary license
and an open-source license.
- The "compcert_new" subdirectory is Copyright (c) 2004-2013 by INRIA,
and contains some files that are not dual-licensed; therefore you should
not use compcert_new unless you satisfy the terms of the CompCert license.
Karl Palmskog (Jul 15 2022 at 16:20):so it looks as though anyone who stays away from compcert_new is in the clear. Not sure which files/modules that actually translates to.
Paolo Giarrusso (Jul 15 2022 at 16:24):That sounds much nicer; but here's the help text from a recent platform (2022.04.0):
If you want to use VST with the provided VST examples only, you require only
parts of CompCert, which are dual licensed and open source. In case you want
to verify your own C code with VST, you need non open source parts of
CompCert, notably the clightgen program. CompCert does not support
installing only its open source parts, since evaluation usage is explicitly
allowed in the license (see link above).
if the textbook includes the ASTs, and there isn't a problem with _their_ license, it seems the rest is completely fine.
Karl Palmskog (Jul 15 2022 at 16:26):yes, note the distinction between "C code" and "Clight code". So the crux seemingly becomes to obtain/express the program as Clight inside Coq [without violating the license for clightgen]
Karl Palmskog (Jul 15 2022 at 16:28):but I guess the opam file also provides a sufficient condition to be in the clear: express the program you want to verify in the same way as the VST examples, without using clightgen or other stuff that is not dual licensed
Karl Palmskog (Jul 15 2022 at 16:32):I mean, if a VST program verification example in the VST repo is fully open source, then you should be able to use that as a template for new program verification. And if you replace code in your template without using CompCert code/tools in any way, I don't see how one can argue it's a license violation, regardless of whether commercial or not
Lessness (Jul 15 2022 at 17:19):I don't know... it seems quite hard to do C program verification (using VST) while avoiding any use of clightgen tool. :(
Karl Palmskog (Jul 15 2022 at 17:36):the pretty-printing of Clight into C-like syntax works quite well. That's how I would do it - write Clight manually and check that it makes sense using the Clight pretty printing inside Coq
Pedro Abreu (Jul 25 2022 at 15:16):Hey @Lessness , that sounds like a cool idea. Any news or plans on it? Maybe an interesting approach would be to offer twitch streams on a weekly basis so that patreons can see your progress and interact with how things are going? I could see value in that
Lessness (Jul 25 2022 at 17:01):Thank you for the kind suggestion. <3
My spoken English is quite bad, so I plan to stay exclusively in text mode, sadly. :\
I'm slowly learning and formalizing model theory, and this will be main thing for now. (Euler Project and its first 100 exercises are postponed for now.)
Also, I like the idea of weekly status updates very much, so I'm plan to do them (on patreon.com, publicly for all, probably each Sunday starting with this weekend).
Huỳnh Trần Khanh (Jul 26 2022 at 03:27):My spoken English is quite bad
I doubt it. Your English looks fine here. Just give talking a try, I assure you you're better at talking than you think!
Lessness (Jul 30 2022 at 20:40):https://www.patreon.com/posts/69805072 - there's the first post.
Feel free to ask questions or write suggestions! :)
Karl Palmskog (Jul 31 2022 at 21:21):some possibly useful links:
Logic/fol_prop.ml has compactness) Karl Palmskog (Jul 31 2022 at 21:23):in particular, I think the main difference from the MathComp Model-theory-in-Coq approach is that since this is HOL, there are no dependent types, hence no Language structure
Karl Palmskog (Jul 31 2022 at 21:26):so if I wanted to do FOL metatheory, I would probably emulate the OCaml here (code from Harrison's book): https://github.com/logic-tools/sml-handbook/blob/master/code/OCaml/fol.ml
Yannick Forster (Aug 03 2022 at 07:23):For FOL metatheory, I'd recommend to use the FOL library underlying the arxiv paper on model theory you mentioned. It's here: https://github.com/dominik-kirst/coq-library-undecidability/tree/fol-library Probably it will be released as a standalone library soon. There is a talk about it next week at the Coq workshop!
Last updated: Oct 08 2024 at 14:01 UTC