Our great sponsors
-
-
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
-
checkedc
Checked C is an extension to C that lets programmers write C code that is guaranteed by the compiler to be type-safe. The goal is to let people easily make their existing C code type-safe and eliminate entire classes of errors. Checked C does not address use-after-free errors. This repo has a wiki for Checked C, sample code, the specification, and test code.
-
>The files in question are, from a formal verification standpoint, the interface to CompCert. They are licensed under the non-commercial license (NCL) so that they can be used together with the rest of CompCert (the implementation of the compiler, so to speak), which is NCL-only.
>Additionally, the interface files in question are also licensed under the GPL so that they can be used in other, open-source projects such as VST (http://vst.cs.princeton.edu/) that connect with CompCert.
at https://github.com/AbsInt/CompCert/issues/140 (2016)
CakeML[0] is another formally verified compiler. Notably, unlike compcert, it is open source.
The language it implements (an sml dialect) is high-level and garbage collected, meaning that it is not usable in all of the same domains, but work is ongoing to reuse much of the compiler infrastructure for 'pancake', a low-level language.
0. https://github.com/CakeML/cakeml
I don't agree.
Consider WUFFS https://github.com/google/wuffs
WUFFS will give you a C library that can turn PNG data into raw image data and is definitely correct. It's not exactly idiomatic C, you'd assume if a person wrote this code it's probably wrong, but WUFFS promises it's correct. CompCert should turn that C library into executable code which is therefore also definitely correct.
Now, maybe you will screw up code that reads the PNG data from a disk file, or draws the image on a screen, or a million other things, but the WUFFS library components are definitely fine, not just "Bill wrote it and he's got 20 years experience" fine or "It passed the unit tests" fine but "Four Color Theorem" fine.
Related posts
- So you think you know C?
- Show HN: MicroTCP, a minimal TCP/IP stack
- Berry is a ultra-lightweight dynamically typed embedded scripting language
- Resources for beginners
- Recently I am having too much friction with the borrow checker... Would you recommend I rewrite the compiler in another language, or keep trying to implement it in rust?