Hacker News new | ask | show | jobs
by practal 386 days ago
I have not defined any "abstract lattice extension" explicitly; which is nice, why would I need to know about lattices for something as simple as this? It is just a convention I suggest to get a useful Defined predicate, actually. Nobody can stop you from defining mul 0 ⊥ = 0, for example, and that might make sense sometimes.

I would suggest that abstraction logic compares to type theory as Lisp compares to Standard ML; but that is just an analogy and not precise.
1 comments
thechao 386 days ago
My problem with your interaction on this forum, so far, is that it kind of ignores the practical (artisan) craft of programming. The use of static type systems by working engineers isn't math; it's more akin to "fast, formal checking". You can assert that you don't like types, or they're useless all day long; but, every working engineer knows you're wrong: static type systems have solved a real problem. Your arguments need to be rooted in the basic experience of a working engineer. Single-level programming has its place, but runtime checking is too error prone in reality to build large software. If you think this isn't true, then you need to show up to the table with large scale untyped software. For instance: the FORTH community has real advantages they've demonstrated. Where's your OS? Your database? Your browser? If you have real advantages then you'd have these things in hand, already.

Otherwise, you're just another academic blowhard using a thin veneer of formalism to justify your own motivated reasoning.

link
practal 386 days ago
Strong opinion! Also, it seems you didn't read my interaction so far carefully enough. You also didn't read the summary I linked to, otherwise you would know that I fully approve the current use of types in programming languages, as they provide lightweight formal methods (another name for what you call "fast, formal checking"). But I think we will be able to do much better, we will have fast, formal checking without static types. Not today, not tomorrow, but certainly not more than 10 years from here.
link
thechao 385 days ago
I'm reading through your paper, and I really like your ideas. I just think you're approaching the engineers wrong.
link