The project is in ideation phase. DRAFT.md
is where I dump my thoughts.
Consig empathizes very much with a project whose name suggests a rewrite of SciPy. We share the vision that Lean programs can be a better abstraction in scientific computing. However, SciLean project as it is defined today jumps perhaps a bit rashly on the Lean train. Workshop-paper level signals simulation (the problem domain of Consig) practically revolves around Python, Matlab and Octave today. To our knowledge, there has been no momentum strong enough in recent years for a shift in this landscape. Scientists and engineers have generally used the tools they prefer, and Consig in philosophy doesn't want to change that.
Given enough time, hypothetically, Lean overtakes Python as the most popular language for scientific computing, thanks to SciLean. Consig's ideal future, on the other hand, is when reviewers sometimes ask authors of simulation papers of proofs of parts they are not convinced of.
Literate programming for Coq and Lean4.