Skip to content
/ consig Public

Lean lib for signals simulations. Easy FFI with Python & Octave to keep our formality in check.

License

Notifications You must be signed in to change notification settings

tbmreza/consig

Repository files navigation

Untitled-2025-05-05-0555

Contributing

The project is in ideation phase. DRAFT.md is where I dump my thoughts.

See also

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.

About

Lean lib for signals simulations. Easy FFI with Python & Octave to keep our formality in check.

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Contributors 2

  •  
  •  

Languages