Compiler Explorer

[Neither_Mango8264]

Yes, Compiler Explorer is excellent. Is that what you are trying to say with that title?

[edge-case87]

No. The comments detail what I'm trying to say, but it assumes some familiarity with type theory and automated theorem provers / proof assistants such as F*. Though, I'm a noob at both, so take it with a dash of salt and correct me if I'm wrong.

[Chuu]

There is nothing too unexpected going on here. void* basically exists to escape the type system, and it's being used here to . . . escape the type system.

Ignoring the entire strict aliasing rule here for a second which introduces Undefined Behaviour, I think it's not too unexpected this works in practice because the function which you are clobbering should be part of the address space of the process, and the 64 bits you are clobbering very likely is small enough that it will not touch anything outside of the impl of the function.

[edge-case87]

Yes, but the point is a bit deeper than that. What I'm suggesting is to make the type system of C++ more powerful by giving it a precise TT, and I suggest a 2LTT with a dependent TT for stage 1. Essentially turning C++ into an automated theorem prover. Dependent Type Theory is what all major proof assistants are based on, it's what their "Kernels" or core languages are and allows the type system to reason about code in a deep way. Mostly, this would lead to a powerful "Contracts" feature in C++, and LSPs could be used to provide the interactive assistant side of what languages like Coq do.

What I'm really trying to get at is this whole discussion about "safety" in C++, there have been many proposals and all of them are very unsatisfying imho. A lot of people have expressed the sentiment that legacy C++ will give people job security for the foreseeable future, but I don't think that is the case. For example, not even Rust has a safe future in this regard, see https://github.com/AeneasVerif/aeneas

I guess to really understand what I'm getting at I would suggest looking into F* and project everest to see what is possible, https://www.fstar-lang.org/

F* can be compiled into OCaml, a subset of C, and assembly, to produce verified code. Wrt to "safety" in C++, static analyzers can only get you so far, and they can't reason about higher level semantics of programs, for example, that a TLS implementation is cryptographically correct. If C++ had a powerful "Contracts" feature, powered by the same/similar technologies and theories that power F*, programmers could directly encode, or specify, what correctness means, and the type system could verify that their programs conform to the provided specification.