Skip to content

Comment on C*: Unifying Programming and Verification in C (2025)parent

Comments

Security Standards/Frameworks like "TCB" (https://en.wikipedia.org/wiki/Trusted_computing_base), "Common Criteria" (https://en.wikipedia.org/wiki/Common_Criteria) etc. are not what i am talking about here. I am pointing to the fact that there is a large piece of industrial-strength C code (i.e. BEAM/ERTS) whose architecture/complexity/techniques are manifested as the "features" of another higher-level language (i.e. Erlang). People seem to appreciate the latter while not comprehending the former. The underlying C-based infrastructure is so good that there are now multiple different-paradigm languages targeting the BEAM.

Incidentally, the C implementation of BEAM/ERTS is not formally verified; only some parts of the upper-layer intermediate representation and bytecode have been verified (academic). Also an Erlang distributed cluster was designed to operate only within an already secure network (i.e. telephone network) and not on today's public Internet. So if you want to run Erlang securely you would need to know overall system security architectures and follow advice given by the "Erlang Ecosystem Foundation Security Working Group" - https://security.erlef.org/

AboutSource Built by g1lg1l

Hackerly is an independent reader for Hacker News, built on the public HN API. Not affiliated with Y Combinator.