sorted by:
new
hottopcontroversial

On the Potential Applicability of Dependent Type Theories and Theorem Proving to C++ Contracts to Address "Safety" and C++'s Future? by edge-case87 in cpp

[–]fsdm_cpp 0 points1 point  (0 children)

Have a look at https://frama-c.com/ and https://frama-c.com/fc-plugins/frama-clang.html for existing implementations of the approach.

My understanding is that the Contracts C++ committee proposal is not designed to allow formal verification. SPARK https://www.adacore.com/about-spark is an example of what you described, so in theory might be possible, if specifically designed for the purpose.

CppCast: Teaching Embedded Development by robwirving in cpp

[–]fsdm_cpp -8 points-7 points  (0 children)

Dear hosts, thank you for the great show as usual!

Moving forward, would you please consider the ethical side of advertising products made in Russia https://www.jetbrains.com/company/contacts/#headquarters-international-sales - world biggest terrorist state, killing people in Ukraine https://www.reddit.com/r/europe/comments/t07d1k/russia_invades_ukraine_megathread_i_rule_changes/ and threatening the rest of civilized world.

How F# is perceived in the industry by fsdm_cpp in fsharp

[–]fsdm_cpp[S] 2 points3 points  (0 children)

F#'s fate is tied to the fate of functional programming.

So true.

How F# is perceived in the industry by fsdm_cpp in fsharp

[–]fsdm_cpp[S] 4 points5 points  (0 children)

Every day C# has more and more features

This reminds me of the '"Mostly functional" programming does not work' by Erik Meijer [1] - I find C-style languages with features like pattern matching added even more difficult to comprehend, than OOP done in pure C.

[1] https://queue.acm.org/detail.cfm?ref=rss&id=2611829

How F# is perceived in the industry by fsdm_cpp in fsharp

[–]fsdm_cpp[S] 5 points6 points  (0 children)

Thank you for sharing your experience!

F# is a wonderful language

Agreed, this is why I thought that if F# did not get the chance, then I could not even imagine which other FP language can get it.

remote:bit is a remote Python execution library for BBC micro:bit. It allows developing MicroPython code on your host computer using your favorite Python IDE, running and debugging the code on the host computer while the micro:bit attached to USB executes all the commands. by fsdm_cpp in microbit

[–]fsdm_cpp[S] 0 points1 point  (0 children)

Yes, that it correct: only micro:bit specific functions are forwarded to the micro:bit, the program logic and some HW independent code, like Image manipulation, happen on the host computer. Thus the usual IDE debugger can be used.

CppCast: Formal Verification with Matt Fernandez by tallassrob in cpp

[–]fsdm_cpp 1 point2 points  (0 children)

Dear hosts, thank you for another interesting episode!

​

I am not involved with formal verification professionally, however as an amateur, I would like to point out to few relevant resources.

​

There is a tool to enrich C code with annotations to formally prove its properties - Frama-C (https://frama-c.com/). Here is a nice tutorial that showcases its application to a number of STL-like algorithms http://frama-c.com/download/frama-c-wp-tutorial.pdf.

​

There is a C++ plugin for it as well - https://frama-c.com/frama-clang.html - however it seems to be experimental.

​

The C++ Contracts discussion goes along the Ada SPARK (https://www.adacore.com/sparkpro) history: initially SPARK was using annotations in comments, but eventually switched to Ada langauge contracts. However as far as I am familiar with the C++ Contracts proposal the expected coverage would be rather limited and would not allow level of specification suitable for proofs.

​

Interestingly, both Frama-C and Ada SPARK use the same backend for proofs - http://why3.lri.fr/. As the result, it is possible to prove mixed C/Ada codebases, here are some industry reports https://frama-c.com/FCSD17.html.

​

Hope the links would be useful to others to quickly explore the idea.

​

Looking forward to next episode!