That much I'm aware, but that's just about feature availability. I was wondering how far the implementations have progressed internally, despite the features being unavailable.
Thanks, yeah, I was worried that might be the case. Given how complicated these features sound, it makes me wonder if they're gonna finish before the decade is over...
OpenCode's creator acknowledged that the ease of shipping has let them ship prototype features that probably weren't worth shipping and that they need to invest more time cleaning up and fixing things.
Uff. This is exactly what Casey Muratori and his friend was talking about in of their more recent podcast. Features that would never get implemented because of time constraints now do thanks to LLMs and now they have a huge codebase to maintain
I was curious why some expressions in the code used the character ù, such as “If Zù500”. It looks like a character encoding error, but the code presumably works correctly. ChatGPT says the byte value for ≤ in TI-BASIC is the same as ù in ANSI/Windows-1252 (0xF9).
Looks like LLMs also find Dafny easier to write than Lean. This study, “A benchmark for vericoding: formally verified program synthesis”, reports:
> We present and test the largest benchmark for vericoding, LLM-generation of formally verified code from formal specifications … We find vericoding success rates of 27% in Lean, 44% in Verus/Rust and 82% in Dafny using off-the-shelf LLMs.
Not surprising, as Dafny is a bit less expressive (refinement instead of dependent types) and therefore easier to write. IMHO, it hits a very nice sweet spot. The disadvantage of Dafny is the lack of manual tactics to prove things when SAT/SMT automation fails. But this is getting fixed.
If you haven't already, check out Microsoft's "The Windows® 95 User Interface: A Case Study in Usability Engineering" report summarizing some of the Windows 95 designers' user research:
I read it and it partially inspired the entire project. It made me realise how inaccessible modern design is despite being held up as best in class and easy to use
> That would be like antropic and google crying about china stealing the weights that were originally built by scraping as fuck stolen content :-)
do you really see a relation between the two, or are you just willfully 'buying an advertisement' by trying to shape a metaphor from the social qualms that you wish to rebroadcast to people?
in other words, no -- this isn't at all similar to the companies that steal media in order to train models only to complain about similar theft from other companies targetted towards them -- but I agree with the motivation, fuck em; they're crooks...
but don't weaken metaphors simply to advertise a social injustice. If you want to do that, don't hijack conversations abroad.
https://clang.llvm.org/cxx_status.html
https://gcc.gnu.org/projects/cxx-status.html
reply