Update README.md

formal-land · May 10, 2024 · 8beca03 · 8beca03
1 parent 147df86
commit 8beca03
Showing 1 changed file with 7 additions and 1 deletion.
diff --git a/README.md b/README.md
@@ -1,9 +1,15 @@
 # coq-of-python
 
-> Translate Python code to Coq code.
+> Translate Python code to Coq code
 
 ```python
 input = "🐍"
 
 print("🐓")
 ```
+
+## Status
+
+We focus on translating the Ethereum specification, which is written in Python: https://github.com/ethereum/execution-specs The output of the translation is in [CoqOfPython/ethereum](CoqOfPython/ethereum).
+
+The generated Coq code type checks, with some holes for expressions we do not handle yet. We are now working on adding a semantics to be able to specify at least one file.