Suppose I have a Python program that takes "angle" and "initial speed" as arguments and calculates where a ball shot from a cannon lands. The program could be described using the function
f(\theta, s) = d
where \theta is the angle, s is the speed, and d is the distance from the cannon where the ball lands. The function could be expressed using a variety of languages like Python, C, Lean, etc.
If f(\theta, s) = d is derived from the equations of motion (like https://derivationmap.net/review_derivation/201726/) and each step is verified using Lean (as described in this post), then we can use Lean to calculate d from \theta and s. The difference would be that there's more explanation of where the result came from. Rather than just "here the equation to use," including the derivation step and proof of each step makes the assumptions explicit and the implementation correct.
All software programs can be described as functions that take arguments and return results. That doesn't mean that all functions are derived. As an example of software that is a function but isn't derived, consider the A* routing algorithm. An algorithm outlines a sequence of steps for accomplishing a function.
While all programs could be written in Lean (because each program is a function), not all functions are derived mathematically. As a trivial example, printing "hello world" is not a derived function. In contrast, the first example in this post, the distance a projectile flies, is derived from the equations of motion. What distinguishes "hello world" and A* routing from the cannon ball trajectory?
The distinction is that the cannon ball example is a numerical simulation of a tangible scenario, whereas "hello world" is not describing physically-constrained reality.
For numerical simulations, Lean can formally verify the derivation and the formula used for analytical calculation. Keeping both aspects in Lean results in a clear chain of custody.
For algorithms (e.g., A* routing, "hello world"), the verification is to show that the implementation is consistent with the requirements. Here languages like Dafny and F* are relevant.
More on F*:
- https://en.wikipedia.org/wiki/F*_(programming_language)
- https://www.microsoft.com/en-us/research/project/the-f-project/
- https://github.com/FStarLang/FStar
- https://www.fstar-lang.org/
- https://fstarlang.github.io/
More on Dafny:
- https://en.wikipedia.org/wiki/Dafny
- https://www.microsoft.com/en-us/research/wp-content/uploads/2008/12/dafny_krml203.pdf
- https://homepage.cs.uiowa.edu/~tinelli/classes/181/Fall15/Papers/Lein13.pdf
- https://dafny.org/
No comments:
Post a Comment