Content deleted Content added
Line 15:
=== Trusted computing base ===
The implementation of the underlying ML compiler adds to the [[trusted computing base]]. Work on CakeML<ref name="cakeml">{{cite web |title=CakeML |url=https://cakeml.org/ |access-date=2 November 2019}}</ref> resulted in a formally verified ML compiler, alleviating some of these concerns.
=== Efficiency and complexity of proof procedures ===
| |||