Zulip Chat Archive

Hi, I work exclusively on embedded systems and am therefore looking for tools that can be used for verification and have code generation for C/C++.
Looking at what is out there, the question I have at this point is what can be better to use for code verification of C/C++-based code for embedded systems: Coq or Lean? The answer is probably both, but I am somewhat encouraged by the syntax of Lean as opposed to the syntax of Coq.

Huỳnh Trần Khanh (Dec 24 2021 at 00:22):

coq has more mature tooling for what you're trying to do, see https://softwarefoundations.cis.upenn.edu/vc-current/index.html

Johan Commelin (Dec 24 2021 at 10:15):

@Anton Hristozov Lean 3 does not have code generation to C. But Lean 4 does. There is a lot going on with Lean 4 right now, and I don't think it's ready for production (there's no official release yet). But it shouldn't be long and then Lean 4 will also be a good system for this.

Joe Hendrix (Dec 24 2021 at 19:02):

@Anton Hristozov I worked on a proof of concept where we ported a robotic car controller from C to Lean 4, and got it running on a Rasberry Pi. The writeup with a link to the source is avalable here.

Joe Hendrix (Dec 24 2021 at 19:04):

If you want to verify or look for bugs in existing C/C++ code, then in addition to the Coq work, you may want to take a look at CBMC, Galois's Software Analysis Workbench, Facebook Infer, and/or FramaC among others.

Anton Hristozov (Dec 24 2021 at 19:53):

Thank you @Johan Commelin
I installed and ran lean 3.4.2 on my Linux box, but Lean 4 had issues after following the build instructions. Looks like it is still work in progress.

Alex J. Best (Dec 24 2021 at 19:54):

Lean 3 is now maintained by the community and has come many versions since 3.4.2 check out #install for the latest instructions for community lean 3

Anton Hristozov (Dec 24 2021 at 19:57):

Thank you @Joe Hendrix
I saw the robotic car controller on the web you mention.
I am also interested in the opposite direction of defining higher-level logic in Lean and generating C/C++ code that implements that logic. I am not sure if Lean is meant to be used that way. Possibly this would require some extensions to the language, but it appears that this is supported.

Arthur Paulino (Dec 24 2021 at 20:02):

@Anton Hristozov I think this is related: https://github.com/tydeu/lean4-alloy
@Mac is the one developing it

Arthur Paulino (Dec 24 2021 at 20:04):

I'm not sure if he intends to support the entire C syntax in Lean, but he's got a nice chunk of it already in.

Arthur Paulino (Dec 24 2021 at 20:06):

@Tomas Skrivan and I are also working on something similar. Our current code can turn this into this.

Arthur Paulino (Dec 24 2021 at 20:08):

One thing I like about Lean 4 is that it really feels like a programming language that can be used for all sorts of generic applications. For example, reading and writing files feels satisfactorily smooth.

Anton Hristozov (Dec 24 2021 at 20:25):

@Arthur Paulino All these projects on Github are great directions. Nice to see them.
I agree with the syntax of Lean being readable and the feel of a language.

Mac (Dec 24 2021 at 20:34):

Arthur Paulino said:

I'm not sure if he intends to support the entire C syntax in Lean

I do. In fact, It should already be there (and if its not that is a bug). The two caveats are that preprocessor macros don't actually define usable syntax within the DSL (i.e., you can't #define BRACE { and then use BRACE in place of { like you could in C) and that type names need to be manually added to the syntax for disambiguation (see Typdefs.lean for examples).

Arthur Paulino (Dec 24 2021 at 20:41):

Anton Hristozov said:

I agree with the syntax of Lean being readable and the feel of a language.

Oh sorry. I meant more in the sense of reading text files as strings or writing strings to text files. But yeah, Lean code is nicely readable once you get more used to it

Joe Hendrix (Dec 24 2021 at 21:55):

@Anton Hristozov Maybe I misunderstand, but the robotics control code was written in Lean (see here) and compiled to C. You currently do still need some C to write the bindings, but maybe Alloy could replace that as well.

Anton Hristozov (Dec 25 2021 at 13:23):

@Joe Hendrix I looked at the code and see that you have the controller code in Lean and the additional C code to make everything work. This is a great example.
So if we want to make this work for certain aspects of an existing autopilot system, such as PX4, Ardupilot, or ROS, we can use Lean and generate C code to integrate with the rest of the system. I had trouble making Lean 4 run on my Ubuntu 20.04, though, where 3.4.2 worked right out of the box.
Is there an official release date for Lean 4?

Karl Palmskog (Dec 25 2021 at 16:43):

C++ semantics and verification in Coq: https://github.com/bedrocksystems/BRiCk
C semantics and verification in Coq: https://github.com/absint/compcert https://github.com/PrincetonUniversity/VST
C code generation focused on cryptography in Coq: https://github.com/mit-plv/fiat-crypto

Karl Palmskog (Dec 25 2021 at 18:47):

Andrew Appel's recent overview of program verification tooling in Coq has more C+Coq references: https://www.cs.princeton.edu/~appel/papers/ecosystem.pdf

Joe Hendrix (Dec 25 2021 at 19:30):

@Anton Hristozov I'm glad you are able to get it installed. I'd recommend trying out the Lake build system also if you haven't already. It makes it a lot easier to build both C and Lean in the same project.

Anton Hristozov (Dec 25 2021 at 20:06):

Well, I was able to run the lean binary, but lake and leanc had a runtime error after following the installation instructions for Linux.
Most tools I install on Linux just work. I am going to look at other avenues first and then see if it is worth spending the time with this tool.

Huỳnh Trần Khanh (Dec 26 2021 at 01:03):

head over to #lean4 if you have trouble installing

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib