3 ms·

Is the web demo compiled from the lean?

• permute 4mo ago
  Yes, the webassembly is compiled from lean. The JS UI that calls the webassembly is not built from lean and not formally verified. So a human reviewer that does not trust the code, needs to review the formal spec and the UI code. But the geometry with rare special cases that we want to treat correctly happens in the verified core.
  • olaird25 4mo ago
    Nice. So is the js/lean interface using exact rationals?
    • permute 4mo ago
      Yes