5 ms·
No worries! The comment was fine, I was simply gone so I couldn't reply. TBH, I haven't written anything impressive, just toy examples that are formally verifi
by nextos 2y ago
No worries! The comment was fine, I was simply gone so I couldn't reply.
TBH, I haven't written anything impressive, just toy examples that are formally verified.
I imagine making it practical for larger systems would require a lot more work.
- kragen 2y agoi'm curious to know what you mean by toy examples! are we talking about an assignment statement, an arithmetic expression, finding the maximum of a list, insertion sort, mergesort, a parser for a context-free language, a cooperative multithreading system?
- nextos 2y agoSome simple imperative data structures, including simple operations to add, remove, test membership, etc. with formal guarantees.
- kragen 2y agothat sounds awesome! what does the process of getting to one of those proofs look like? is there a lot of back and forth, or is it mostly autonomous?
- nextos 2y agoMostly autonomous, with a bit of guidance, but this might be because the training set has examples that are similar enough, making interpolation easy.
- kragen 2y agofantastic! i hope you decide to share more details; i'd love to hear them
- nextos 2y agoThanks. It's a toy at the minute, there is nothing super impressive. Taking this forward would require a lot more work and funding to pay for computation to fine-tune models further. It's an interesting topic, perhaps good for a startup or a research lab in case one finds a decent monetization stream.
- kragen 2y agopretty sure you'll be able to monetize writing correct software at scale with an llm