Théo Zimmermann (Jun 24 2020 at 11:21): Théo Zimmermann (Jun 24 2020 at 11:21):This is the topic to ask questions on the talk "Experience Report: Smuggling a Little Bit of Coq Inside a CAD Development Context".
Emilio Jesús Gallego Arias (Jul 06 2020 at 11:21):Session 2 will start at 14:10 Paris time
Dimitur Krustev (Jul 06 2020 at 11:37):Do I need a different Zoom link for this session?
Karl Palmskog (Jul 06 2020 at 11:39):@Dimitur Krustev the organizers will promote you to panelist in Zoom via the regular login, you may want to write in Zoom chat or raise your hand
Dimitur Krustev (Jul 06 2020 at 11:40):Thanks!
Théo Zimmermann (Jul 06 2020 at 11:52):Feel free to join early to test your sound.
Emilio Jesús Gallego Arias (Jul 06 2020 at 12:09):Starting now!
Maxime Dénès (Jul 06 2020 at 12:21):Q: Why did you restrict yourself to tools / libraries coming with the standard Coq installation?
Enrico Tassi (Jul 06 2020 at 12:23):Q: How did you learn Coq? How do your colleagues learn it?
Emilio Jesús Gallego Arias (Jul 06 2020 at 12:23):Really cool stuff!
refs, needed for some more efficient algorithms. Do you have a need for those? Maxime Dénès (Jul 06 2020 at 12:24):Q: Is it hard to hire / find "competent" Coq users in your industrial field?
Yves Bertot (Jul 06 2020 at 12:27):Q: would you have a use case for extension of code production towards more imperative programming language (C, C++ fragments).
Yves Bertot (Jul 06 2020 at 12:28):Agreed for difficulties to work on windows. Coq platform is a big progress.
Emilio Jesús Gallego Arias (Jul 06 2020 at 12:30):Thanks for the answers and the talk @Dimitur Krustev !
Enrico Tassi (Jul 06 2020 at 12:31):Thanks, nice talk!
Hugo Herbelin (Jul 06 2020 at 12:31):Thanks for the talk!
Michael Soegtrop (Jul 06 2020 at 12:31):Thanks for the very nice talk!
Maxime Dénès (Jul 06 2020 at 12:31):Yes, thanks for the talk and the answers!
Dimitur Krustev (Jul 06 2020 at 12:32):Thanks for the nice questions, and also for all the good work on Coq that made it all possible!
Dimitur Krustev (Jul 06 2020 at 12:35):Yves Bertot said:
Q: would you have a use case for extension of code production towards more imperative programming language (C, C++ fragments).
It can be potentially useful in many situations. On the other hand, in my experience imperative code is usually much harder to formally verify. So I am not sure if we shall find - in our particular context - many cases, where it would be profitable.
Dimitur Krustev (Jul 06 2020 at 12:42):Emilio Jesús Gallego Arias said:
...
- q2: you seem to imply that a native F# extraction backend would not be a large gain for you, do you expect that to be the case would you make your approach more extensive?
The 2 things that mostly create problems for us in extracted code are modules and higher-kinded types. While a specialized Coq extractor to F# could help a bit with module restrictions, I am not sure if anything better can be done during extraction about higher-kinded types. The best would be to simply have higher-kinded types in F#. Unfortunately, while this has been on the wish-list for years, there are no signs yet it will happen.
Last updated: May 31 2023 at 04:01 UTC