5 ms·

I feel like this is the exact opposite of the conclusion I've been coming to. In an age where anyone can vibe code stuff at the drop of a hat, I want the abili

by bloaf 1mo ago

I feel like this is the exact opposite of the conclusion I've been coming to. In an age where anyone can vibe code stuff at the drop of a hat, I want the ability to assert guarantees/contracts at a high level, and then let AI work out the details. I want to force AI to work within the confines of an abstraction, not independently of it.

eru 1mo ago
Yes. Compare also https://www.khoury.northeastern.edu/home/cmartens/Courses/7400-f24/readings/theorems-for-free.pdf https://www.khoury.northeastern.edu/home/cmartens/Courses/74... where the abstraction itself mechanically enforces certain guarantees and contracts.
- AdieuToLogic 1mo ago
  The more semantically rich a programming language, the more it demands mathematical veracity. The more a language is mathematically sound, the more its linguistic constructs converge to enforce same. Programming languages which follow this path ultimately support similar capabilities; Applicatives, Functors, Monads, Monoids, and often meta-programming via higher-kinded types and/or intrinsic AST code generation.
winter_blue 1mo ago
> I want to force AI to work within the confines of an abstraction, not independently of it. Yes, this is the way. We need programming languages that make this easier.
- 9dev 1mo ago
  Just a few more months, and the industry will consider OOP the next big thing again. Interfaces as contracts between modules? Obviously superior!
rramadass 1mo ago
> I want the ability to assert guarantees/contracts at a high level, and then let AI work out the details. I want to force AI to work within the confines of an abstraction, Exactly right! More details in my comment here - https://news.ycombinator.com/item?id=49269323 https://news.ycombinator.com/item?id=49269323 See also, Software Abstractions: Logic, Language, and Analysis by Daniel Jackson - https://mitpress.mit.edu/9780262528900/software-abstractions/ https://mitpress.mit.edu/9780262528900/software-abstractions...
libertas_quae_s 1mo ago
I have the same thought on this. Having some abstraction where we have total control and we can make clear judgments is the perfect place where AI should. Removing this abstraction will just make things hard for us and just pray that all the guards around are sufficient.
xiaoyu2006 1mo ago
formal verification? maybe theorem prover or hoare logic can come into play here.

by bloaf 1mo ago

eru 1mo ago

Yes. Compare also https://www.khoury.northeastern.edu/home/cmartens/Courses/7400-f24/readings/theorems-for-free.pdf https://www.khoury.northeastern.edu/home/cmartens/Courses/74... where the abstraction itself mechanically enforces certain guarantees and contracts.

AdieuToLogic 1mo ago
The more semantically rich a programming language, the more it demands mathematical veracity. The more a language is mathematically sound, the more its linguistic constructs converge to enforce same. Programming languages which follow this path ultimately support similar capabilities; Applicatives, Functors, Monads, Monoids, and often meta-programming via higher-kinded types and/or intrinsic AST code generation.

winter_blue 1mo ago

> I want to force AI to work within the confines of an abstraction, not independently of it. Yes, this is the way. We need programming languages that make this easier.

9dev 1mo ago
Just a few more months, and the industry will consider OOP the next big thing again. Interfaces as contracts between modules? Obviously superior!

rramadass 1mo ago

> I want the ability to assert guarantees/contracts at a high level, and then let AI work out the details. I want to force AI to work within the confines of an abstraction, Exactly right! More details in my comment here - https://news.ycombinator.com/item?id=49269323 https://news.ycombinator.com/item?id=49269323 See also, Software Abstractions: Logic, Language, and Analysis by Daniel Jackson - https://mitpress.mit.edu/9780262528900/software-abstractions/ https://mitpress.mit.edu/9780262528900/software-abstractions...

libertas_quae_s 1mo ago

I have the same thought on this. Having some abstraction where we have total control and we can make clear judgments is the perfect place where AI should. Removing this abstraction will just make things hard for us and just pray that all the guards around are sufficient.

xiaoyu2006 1mo ago

formal verification? maybe theorem prover or hoare logic can come into play here.