what I think would be really cool is an interactive language/interface to go from generative, potentially-unsound, partially-verified thoughts and formally examine them by testing them, gradually making them more and more concrete, eventually to the level of formal logic. - ThreadSky

krismicinski.bsky.social • 21 days ago

what I think would be really cool is an interactive language/interface to go from generative, potentially-unsound, partially-verified thoughts and formally examine them by testing them, gradually making them more and more concrete, eventually to the level of formal logic.

Comments

jcenzo.bsky.social•21 days ago

Our gradual verification work has this flavor—a user can go from no formal specifications and incrementally specify more and more receiving verification (static and dynamic) feedback a long the way.

Combined with @neurocy.bsky.social’s live programming work might be even closer.

krismicinski.bsky.social•20 days ago

let me know if you all want to write a proposal on it someday

brendanzab.bsky.social•21 days ago

I’ve found Holbert fun for experimenting/learning about type theory stuff. Not sure how similar it is to what you’re imagining though!

krismicinski.bsky.social•21 days ago

Link? I don’t recognize it 😭

liamoc.net•21 days ago

https://liamoc.net/holbert

be warned there seem to be bugs currently.

liamoc.net•21 days ago

it's not like what you're describing though

brendanzab.bsky.social•21 days ago

Ah yeah, probably a bit of a stretch now re-reading the original post. Was thinking about how you could play around with logic and type theory stuff in a way that might not be sound or correct(?), but there was still a ton of value in that.

krismicinski.bsky.social•20 days ago

it's cool to see examples of demos regardless--I'll check it out.

krismicinski.bsky.social•21 days ago

something like gradual types at the level of reasoning specified in English, gradually transitioning out to work with code that has rich, highly-informative types attached to it.

joeyeremondi.bsky.social•21 days ago

Gradual depenent types have entered the chat

solalpirelli.bsky.social•21 days ago

For performance too. Start with GC, move the hot path to lifetime tracking, and the really hot path to dependent types that prove runtime checks like bounds checks aren't needed.

krismicinski.bsky.social•20 days ago

i agree

Comments

Posting Rules

Reply