search

utensil / ginac-lean

A work-in-progress Lean 4 binding to GiNaC
MIT License
5 stars 1 forks source link

Inspiration: Verifying CAS algorithms modulo lower levels #3

Open utensil opened 6 months ago

utensil commented 6 months ago

References:

Combining this with the ideas in SampCert, cedar-spec, and SSA, we should be able to do 4 things for low level functionalities in one go:

  1. call CAS for the results
  2. have a theorem/axiom for expected property, via opaque/implemented_by maybe fit into a type class
  3. generated the corresponding tests testing the property, with a test subject sampler
  4. use verified codegen or MLIR techniques to generate production code for target language, which could be relying on CAS results.

P.S. An alternative to GiNaC for this idea is gTybalt which is also based on GiNaC (noticed because of AN EXAMPLE OF CLIFFORD ALGEBRAS CALCULATIONS WITH GiNaC).

utensil commented 6 months ago

A smaller scale of experiment is to rewrite kingdon's symbolic capabilities in GiNaC, to check if it could be a drop-in replacement.