On Friday, July 10, 2020 at 7:28:13 AM UTC-5 Bruno Marchal wrote:
> On 8 Jul 2020, at 13:57, Philip Thrift <cloud...@gmail.com> 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 everything-list+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/everything-list/7bc60b1c-f4b9-4696-b7fd-1f57665de911n%40googlegroups.com.
