On Friday, July 10, 2020 at 7:28:13 AM UTC-5 Bruno Marchal wrote:
> On 8 Jul 2020, at 13:57, Philip Thrift <[email protected]> wrote: > > > *Scientific proof-oriented programming (S-pop)* > > https://codicalist.wordpress.com/2020/07/06/scientific-proof-oriented-programming-s-pop/ > > > > Don’t hesitate to sum up your point. Forcing is just a powerful technic to > build weird model of set theory. Forcing is a particular S4-like modal > logic. The relation between Smullyan-Fitting “quantisation in S4” and the > material mode of the self-referential machine is a bit an open problem for > me. I might say more on this in some future. > > Bruno > > > As outlined there: Repurpose a *proof-oriented programming system* (Coq, Lean, Agda) with forcing, e.g. *forcing in Lean:* https://github.com/jesse-michael-han/flypitch to do physics, e.g. *categorical quantum mechanics* - https://www.cs.ox.ac.uk/teaching/courses/2019-2020/cqm/ and implement *set-theoretical forcing in quantum mechanics *- https://arxiv.org/abs/quant-ph/0303089 @philipthrift -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/everything-list/7bc60b1c-f4b9-4696-b7fd-1f57665de911n%40googlegroups.com.
