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.
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.
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.
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.
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.
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.
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
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
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
I don't know... it seems quite hard to do C program verification (using VST) while avoiding any use of
clightgen tool. :(
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
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
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).
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!
https://www.patreon.com/posts/69805072 - there's the first post.
Feel free to ask questions or write suggestions! :)
some possibly useful links:
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
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
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: Dec 01 2023 at 04:01 UTC