You are viewing a single comment's thread from:

RE: A brief analysis and discussion on formalist vs intuitionist programming factions in the crypto community.

in #crypto-news9 years ago (edited)

Tau itself is written/created in C++ because Tau is a compiler. All programming languages have compilers. All compilers must be created in an existing programming language. This would mean the Java virtual machine cannot be created in Java. This would mean the Rust compiler cannot be created in Rust. This would mean C cannot be created in C, because you have to program the compiler in a stand alone language to implement it.

As a result the first implementation of Tau will be the C++ implementation. The C++ implementation does not have to be the only implementation. A Turing complete programming language must be used to implement Tau because according to my understanding you cannot put the constraints there. The constraints have to come in after the logic is put in place which happens in the compile process itself not in the compiler executable. This means Tau has to be programmed perfectly, and Tau itself will have to use correct by construction, which is actually possible to do with CompCert the verified C compiler. I do not know if you can do it using a C++ compiler but I know C and C++ aren't so different so someone could implement a C version of Tau with the verified compiler as long as Ohad releases a formal specification. I think also there is EscherTech which offers formal verification for C++ so Ohad might be able to use these tools to make an exact C++ implementation correct by construction.

References

  1. http://compcert.inria.fr/
  2. http://www.eschertech.com/products/ecv.php
Sort:  

Ok, so writing the compiler in C++ doesn't necessarily make Tau unpredictable. Thanks!

It's not impossible to write reliable code in C++. It's just very difficult to do it and even when you do you have the problem where the more complex the code is the harder it is to audit. When you use correct by construction, and when your code is limited only to for example a compiler, then you can focus all community efforts on that. You have to trust fewer programmers and fewer auditors when you use correct by construction and build the compiler only in C++ and do the rest in Tau.