Stephen Nuchia
Jun 12, 2013, 2:49:46 PM6/12/13
to sage-s...@googlegroups.com
Apparently the answer to my last question is "yes". Since I originally studied the Sage tutorials a couple of years ago "var" has been extended to attache a domain to variables. Still reading up on it, it's connected to the assumptions mechanism and simplify method. I used all of the above in Mathematica but it's structured very differently in Sage and I haven't absorbed it yet. And it isn't immediately clear whether it will do anything with non-scalar domains. But it's a great start!
Stephen Nuchia
Jun 14, 2013, 10:05:41 AM6/14/13
to sage-s...@googlegroups.com
Continuing to answer my own questions ... I went back to Isabelle and found that it has been evolving very nicely, and that very large scale proofs about programs have been accomplished using it. One still has to know what one is doing but it is no longer a matter of juggling chainsaws.
The Isabelle community has a subculture (at least two sub-subcultures, actually) beavering away at building a complete formalization of all of mathematics, with formal verification of formulas with free variables being the focus of the effort. The Sage community, meanwhile, is beavering away at building a complete formalization of all of mathematics with a focus on computational evaluation of formulas without free variables.
Why can't we all just get along?
On the plus side, Isabelle's notebook-equivalent technology exposes an open API and it should be feasible to bring it into Sage's big tent. Gaining access to the library of definitions and theorems as well as their user-guided simplification system would be a huge win. An ambitions project and maybe not as much fun as building a crippled theorem prover from sticks and string but unifying the computational and foundational libraries would be a huge win.
I guess I should move this little monologue over to the developers' forum.
The Isabelle community has a subculture (at least two sub-subcultures, actually) beavering away at building a complete formalization of all of mathematics, with formal verification of formulas with free variables being the focus of the effort. The Sage community, meanwhile, is beavering away at building a complete formalization of all of mathematics with a focus on computational evaluation of formulas without free variables.
Why can't we all just get along?
On the plus side, Isabelle's notebook-equivalent technology exposes an open API and it should be feasible to bring it into Sage's big tent. Gaining access to the library of definitions and theorems as well as their user-guided simplification system would be a huge win. An ambitions project and maybe not as much fun as building a crippled theorem prover from sticks and string but unifying the computational and foundational libraries would be a huge win.
I guess I should move this little monologue over to the developers' forum.
Reply all
Reply to author
Forward
0 new messages