Stream: Coq workshop 2020

Topic: [M4] Smuggling a Little Bit of Coq Inside a CAD...


view this post on Zulip 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".

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 11:21):

Session 2 will start at 14:10 Paris time

view this post on Zulip Dimitur Krustev (Jul 06 2020 at 11:37):

Do I need a different Zoom link for this session?

view this post on Zulip 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

view this post on Zulip Dimitur Krustev (Jul 06 2020 at 11:40):

Thanks!

view this post on Zulip Théo Zimmermann (Jul 06 2020 at 11:52):

Feel free to join early to test your sound.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 12:09):

Starting now!

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Jul 06 2020 at 12:23):

Q: How did you learn Coq? How do your colleagues learn it?

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 12:23):

Really cool stuff!

view this post on Zulip Maxime Dénès (Jul 06 2020 at 12:24):

Q: Is it hard to hire / find "competent" Coq users in your industrial field?

view this post on Zulip 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).

view this post on Zulip Yves Bertot (Jul 06 2020 at 12:28):

Agreed for difficulties to work on windows. Coq platform is a big progress.

view this post on Zulip Emilio Jesús Gallego Arias (Jul 06 2020 at 12:30):

Thanks for the answers and the talk @Dimitur Krustev !

view this post on Zulip Enrico Tassi (Jul 06 2020 at 12:31):

Thanks, nice talk!

view this post on Zulip Hugo Herbelin (Jul 06 2020 at 12:31):

Thanks for the talk!

view this post on Zulip Michael Soegtrop (Jul 06 2020 at 12:31):

Thanks for the very nice talk!

view this post on Zulip Maxime Dénès (Jul 06 2020 at 12:31):

Yes, thanks for the talk and the answers!

view this post on Zulip 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!

view this post on Zulip 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.

view this post on Zulip Dimitur Krustev (Jul 06 2020 at 12:42):

Emilio Jesús Gallego Arias said:

...

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: Feb 06 2023 at 06:29 UTC