Conversation

Imagine a world of programming and proving where we can float effortlessly between logical systems, harnessing the strengths of each of them as needed---much like we can in the natural world around us

Quote Tweet

Jacques Carette

@jjcarett2

· Jan 1

Replying to @jjcarett2 @TaliaRinger and @mietek

And yes, for sure, not hierarchies. Networks of logics, the same way there are naturally networks of theories.

I want it

Are you familiar with gtoolkit.com? It has some characteristics that allow you to “mold” the development concepts and environment. I don’t think proofs and formal verification methods are first class citizens but still might be worth checking out some of the ideas:

gtoolkit.com

Home

Glamorous Toolkit is the moldable development environment.

Replying to

and

I'm a big fan of Glamorous Toolkit, but I struggle to see the relevance here? It doesn't seem to have much to say when it comes to the trickier problems when it come between mixing formal systems afaik?

9:46 PM · Jan 1, 2022Twitter Web App

Replying to

and

I read more context of the tweet and you are right.