<kluk>
Regenaxer: re "symbols are globally statically visible and accessible in the current namespace search order, but they are bound at runtime by function parameters, let bodies etc to values" I am now reading more about it to investigate this. I appreciate the explanation.
<Regenaxer>
Hi kluk! Glad to hear :)
m42e has joined #picolisp
<kluk>
Regenaxer: If I am correct and this applies to every symbol (the idea of firstclassenvironments and its article is what I am reading now) such that you can have a program that uses (print ...) but that when run under (let (print print-amenable-to-testing) ...) then you basically have some sort of effect handler system built into this paradigm.
m42e has quit [Client Quit]
m42e has joined #picolisp
<kluk>
and hi!
<Regenaxer>
"applies to every symbol" is correct for internal symbols, and other symbols (transients and external) which are currently in-scope
<Regenaxer>
I would say environments refer to the bindings, not the scope
<kluk>
"I would say environments refer to the bindings, not the scope" I see that too.
<Regenaxer>
As far as I know about CL or Scheme, there is not much difference between scope and binding, as symbols are gone after compilation anyway
<Regenaxer>
They are just used for variable names
<kluk>
CL symbols are gone after compilation? I don't even think that is true in ECL.
<Regenaxer>
Not gone in the sense of garbage collected
<Regenaxer>
But not relevand
<Regenaxer>
relevant
<Regenaxer>
or used in any way
<Regenaxer>
unless you put a property or explicitly access them in some way
<kluk>
I'm not sure about that. Alan Kay got the idea of late binding from lisp.
<Regenaxer>
Yes, original Lisp
<Regenaxer>
but CL and Scheme focus on compilation
<Regenaxer>
and after compilation a variable is just a location on the stack
<Regenaxer>
no need to keep the symbol around
<kluk>
a yes, no need to keep a symbol for a variable around, true.
<kluk>
the firstclassenvironments article is well written and well-motivated and making sense so far, but what is the article to read about scope, then?
<Regenaxer>
I completely forgot that this article exists ;)
<kluk>
I get lost at Activation on the firstclassenvironments article :/
<Regenaxer>
Seems I wrote it
<Regenaxer>
Activation means that the bindings are avtive
<kluk>
okay, it makes sense, just wish there were more examples on that article
<Regenaxer>
Sorry, interrupted by phone
<Regenaxer>
There are some examples in the reference of 'bind' and 'job'
<Regenaxer>
'job' is the main vehicle
<Regenaxer>
'bind' is like 'let' or 'use', it takes an executable body
<Regenaxer>
(a 'prg' in the pil terminology)
<kluk>
no problem, I was reading the tutorial again
<kluk>
e.g. (in "@lib.l" (read)) this is today subsumed in algebra by what is called algebraic effects. I totally understand why someone would use your binding/scoping rules (what's it called anyway?) for this sort of advantage, as this is only currently being formalized in FP - I gave a talk about it at the chicken scheme coding jam this year in fact.
<kluk>
dynamic binding?
<Regenaxer>
yes, dynamic binding in pil, lexical binding in scheme, right?
<kluk>
yes
<kluk>
Regenaxer how do you see the aspiration to the requirement of enlisting the computer to aid in verification of the correctness of one's programs? clearly by using dynamic binding you abrogate the possibility for any sort of verification, so perhaps you deem them as bicycle training wheels or bowling with the bumpers up, or what exactly? I am very curious as to how you see this.
<Regenaxer>
Verification is only possible for certain parts of a program, I think most real-world code cannot be verified formally anyway
<Regenaxer>
But dynamic binding does not worsen the situation much
<Regenaxer>
I any case you have to follow rules
<Regenaxer>
So for dynamic binding certain rules should be obeyed
<Regenaxer>
There is @lib/lint.l which tries to statically check some rules
<Regenaxer>
Not at all fully possiale, of course, as a static check is very limited
<Regenaxer>
NIL means nothing obviously offending found
<kluk>
Interesting.
<Regenaxer>
The goal of lint is not correctness, but mostly pil coding conventions and common errors
<Regenaxer>
I use it very seldom, mostly forget about it
<Regenaxer>
But it is a good idea to call it now and then
<Regenaxer>
I use it seldom because most such errors are quickly found during the most basic tests
<Regenaxer>
One of the things lint checks are free variables, which are the main issue with dynamic binding in terms of provability
<Regenaxer>
"unbound" variables that is
<kluk>
I see.
<kluk>
Regenaxer I think advancements in this field and in that of OOP are ultimately divergente whereas in FP they are convergent, does that ring any true to you? For instance, peer into the chasm (http://lambda-the-ultimate.org/node/1332) where the relationship (isomorphism) between the Curiously Recurring Template Pattern, F-bounded quantification, System F-sub and Coalgebras is offered for discussion eliciting a total of 5 people commenting.
<kluk>
If there is a disinterest in the formalization of a given paradigm then is it not bound to eternal wandering and never settling?
<kluk>
The idea of correctness of a program is only up-to adhesion to the paradigm, i.e. it is about offering checks and guarantees that programs are well-formed, not correct; it is a subtle difference.
<Regenaxer>
Most programmers see this pragmatically
<Regenaxer>
In general there is not much interest
<Regenaxer>
(in provability)
<Regenaxer>
Let's say I write an ERP system. What will you prove in it?
<Regenaxer>
The plain math in it is trivial, the rest is not
<Regenaxer>
All you can prove in it is trivial
<kluk>
E.g. in FP type-checking is about witnesses (functions and other values) to well-formed-formulas (types) and the guarantees are just with regards to that level and they are only with regards to any business level to the extent to which you encode that business level in the type system, which leaves some room for the programmer to decide how much of their program should "go through the types" so to speak. Ruby is adopting optional types in
<kluk>
3.0, javascript has typescript now, it seems people want at least a way to opt-into some "help" from the type-checker.
<kluk>
The math in it is trivial? You mean the numeric math? What about the non-numeric math?
<Regenaxer>
Math in general
<kluk>
It's still not trivial enough that I want to carry it in my head.
<Regenaxer>
For example?
<Regenaxer>
Laws and tax rules?
<Regenaxer>
bookkeeping?
<kluk>
I'm not familiar with those fields.
<Regenaxer>
Or any other non-trivial real-world application?
<kluk>
in an ERP system, or whatever system, I still want to prove its parts are correct up to some standard.
<Regenaxer>
Yes, me too, but I see no way
<kluk>
no way to prove its parts?
<Regenaxer>
The provable part are trivial
<Regenaxer>
parts
<kluk>
what are the unprovable parts?
<kluk>
the non-trivial ones? let's see them
<Regenaxer>
Everything you have to deal with in the long term
<Regenaxer>
The formal stuff is easy, and done in an early stage of the program
<kluk>
I don't really understand the argument you are making.
<kluk>
It's too hand-wavy for me.
<kluk>
"the formal stuff is easy"
<Regenaxer>
yeah, because thats how it is
<kluk>
I don't even know how to unpeel that
<Regenaxer>
you cannot pin it down
<Regenaxer>
You model many aspects of the real world
<Regenaxer>
and the real world has not even well-defined fixed rules
<Regenaxer>
exceptions and special cases everywhere
<Regenaxer>
and changing all the time
<kluk>
I think this speaks quite a bit about why we have our preferences. I feel the way you are speaking is somewhat foggy and indeterminate. I feel I need types perhaps because I need things explained to me in a very detailed way.
<Regenaxer>
This is how my customers "speak" :)
<Regenaxer>
not my preferences for sure
<Regenaxer>
I need to model business processes
<Regenaxer>
I see nothing which can be proved here
<Regenaxer>
But even for simpler things: Take any part of software, for example @lib/vip.l
<Regenaxer>
A small simple editor
<Regenaxer>
What will you prove here? What is correct?
<kluk>
Okay, that I can answer
<kluk>
Look at Yi, it's an editor written in Haskell. To answer your question: every part of it can be proven correct.
<Regenaxer>
What means "correct" in an editor?
<kluk>
that there are witnesses (proof, implementations, values, code) for each well-formed-formula (type)
<Regenaxer>
How does it prove that the edited text is stored in the right place?
<Regenaxer>
That every change does not lose a character?
<Regenaxer>
That the correct charset is used?
<Regenaxer>
Editors have tons of side-effects
<Regenaxer>
No way to prove then
<Regenaxer>
Only trivial cases
<kluk>
How does it prove that the edited text is stored in the right place? |> the programmer has some choice on this. the more you tie the semantics of your denotation to the types, in other words the more you encode the meaning of your program through well-formed-formulas, the more things you can prove, including that "the edited text is stored in the right place", "that every change does not lose a character", "the correct charset is used", etc.
<kluk>
"only trivial cases" |> not at all, look at Idris, page 40 of this https://idris2.readthedocs.io/_/downloads/en/latest/pdf/ shows you a glimpse into how any state machine (hence any stateful program) can be proven simply through dependent types.
<kluk>
That statement is categorically incorrect.
<Regenaxer>
Haskell uses static types, completely opposite to (Pico)Lisp
<Regenaxer>
Haskell stresses static types
<Regenaxer>
The real world is dynamic
<Regenaxer>
everything changes
<Regenaxer>
Checking types is not enough. You may get the right type but still the value can be meaningless in the given situation
<kluk>
When you say "haskell stresses static types but the real world is dynamic" I think that is an inaccurate use of those words static/dynamic; the real world is dynamic but not in the same way that dynamic values are dynamic. The "dynamic" of variables is a Computer Science concept that is not the same "dynamic" of life.
<Regenaxer>
right
<kluk>
"everything changes" is perhaps too condensed of an argument for me to parse
<Regenaxer>
What I mean is that types are simple to check, so it is easy to handle them
<Regenaxer>
But in practical progragming I seldom have type problems
<kluk>
What types are you thinking of when you say that? What language do you have in mind when you say that? There are a few things you are picturing in your mind that I feel are not coming through.
<Regenaxer>
It is that what happens unexpectedly
<Regenaxer>
Independent of language
<Regenaxer>
Types in pil can be built-ins, like numbers, symbols and lists
<Regenaxer>
or classes of objects
<Regenaxer>
or just the "meaning"
<kluk>
So for example, parsing a JSON, the JSON is dynamic, we never know what it's going to be, yet it rolls out of the tongue to code one in FP langauges. What am I missing re ability to deal with the dynamic world? Maybe I need the example you have in mind when you say that.
<Regenaxer>
I have the right type, e.g. a person
<Regenaxer>
but I treat it the wrong way despite the formal type is right
<Regenaxer>
The code is right too
<Regenaxer>
But later it may be wrong
<Regenaxer>
cause some condition in the real world changed
<Regenaxer>
The problem is outside the proven code
<Regenaxer>
it includes the whole world
<Regenaxer>
because we are modelling the real world
<kluk>
That sounds like you are a natural coalgebraist/top-down thinker: "the problem is outside the proven code" is literally what the formula for Coalgebra says: x -> F(x), F is the world, F is "outside the code" because it is positive/covariant, "it includes the whole world" because it does not appear on the negative/contravariant side, "because we are modeling the real world" is literally what coalgebras do, build robotic simulations of the
<kluk>
real world. :)
<Regenaxer>
Let's take an even simpler case: How can we prove that PicoLisp's bigmath functions are correct? This I really would like to solve
<Regenaxer>
I run random test, and try to take care of border conditions, but how can I prove it?
<kluk>
That I am not interested in. I don't like numeric math.
<Regenaxer>
Me neither
<Regenaxer>
but if we cannot even prove that, we don't have a base for non~trivial things
<kluk>
that is a non-sequitur
<kluk>
arithmetic is explicitly passive of Gödel's incompleteness
<kluk>
Algebras are not.
peterhil has joined #picolisp
<kluk>
you do not have to wait for arithmetic to be proven in order for algebraic things to be proven
<Regenaxer>
Not proving arithmetics
<Regenaxer>
proving the *code*
<kluk>
numeric math is arithmetics
<Regenaxer>
the results are
<kluk>
You said: "but if we cannot even prove that [meaning: numeric math], we don't have a base for non~trivial things", I said: "you do not have to wait for arithmetic to be proven in order for algebraic things to be proven"
<Regenaxer>
but the manipulations of the bits need to be correct
<kluk>
but the manipulations of the bits need to be correct |> that is proven, actually
<Regenaxer>
bignum math is a program which needs to be correct
<Regenaxer>
How is it? Can you prove it for the llvm-ir code in pil?
<kluk>
Regenaxer that is tractable. Just extrapolate how they already prove math in cpus.
<kluk>
forget llvm
<kluk>
it is a red herring here
<Regenaxer>
ok, then assembly
<kluk>
think of the cpu
<kluk>
no
<kluk>
circuits
<kluk>
think of the cpu
<kluk>
it does math
<Regenaxer>
yeah!
<kluk>
its math is proven in a circuit checker
<Regenaxer>
Let's prove it :)
<kluk>
you can use that to prove bignum
<kluk>
not me, I don't like numeric math
<kluk>
it's boring
<kluk>
I prefer proving real-life programs
<kluk>
much more exciting
<Regenaxer>
For me (big)nums are the base of real programs
<kluk>
why does proving numeric math get you so excited whereas proving real-life programs does not?
<Regenaxer>
Both would be fine, but proving such a small part would be a good start
<Regenaxer>
Not "proving numeric math" but the code which should be "correct"
<kluk>
"For me (big)nums are the base of real programs" |> okay, but once you prove Bignum, are you going to stop there? You will have the base covered, are you then going to continue proving up?
<kluk>
the code is about numeric math
<kluk>
that is why I say it
<kluk>
it's boring code about arithmetics
<Regenaxer>
ok, but how to prove that it is correct?
<Regenaxer>
I can't
<Regenaxer>
I would like to
<kluk>
assume it's correct until you see a bug (very unlikely) and start proving the rest of your program
<Regenaxer>
Thats what I do with @misc/bigtest
<Regenaxer>
But it is no prove
<Regenaxer>
What I say is we cannot even prove such basic, simple "boring" stuff
<kluk>
Regenaxer I think if you write an implementation of Bignum in Haskell you will have what you are looking for.
<kluk>
That will amount to a proof for it.
<Regenaxer>
Perhaps, but I cannot
<Regenaxer>
In fact it is two proofs
<kluk>
"What I say is we cannot even prove such basic, simple "boring" stuff" |> But Regenaxer , arithmetic is *not* "more basic" than algebra, which can be used effectively today to prove algebraic programs are correct. Do you understand what I am saying here?
<Regenaxer>
No, it is not a problem of algebra at all
<Regenaxer>
Bignums manipulate words and patterns of different sizes
<kluk>
I didn't say "it is a problem of algebra
<Regenaxer>
(1) this algorithm is not proved yet
<Regenaxer>
(2) its implementation is neither
<Regenaxer>
Proving (1) is a formal task
<Regenaxer>
What is (2)?
<Regenaxer>
(2) can be done in Haskell
peterhil has quit [Quit: Must not waste too much time here...]
<Regenaxer>
But does this help?
peterhil has joined #picolisp
<Regenaxer>
in pil?
<Regenaxer>
tel again ...
<kluk>
We are using different nomenclature. What I mean by proof is not what you mean by it. I'm not ever talking about proving some implementation of Bignum correct up-to the ideal Platonic standard of Bignum. I am talking of proof in terms of Curry-Howard isomorphism. A program in FP is a proof, equivalent to how a program in Imperative Programming is an algorithm. If you write any Bignum implementation in Haskell that implementation *is* a
<kluk>
proof for *some* well-formed formulation of Bignums. How much of your code you choose to express in terms of formulations and how much in terms of proof is up to you, such that any implementation of Bignum in Haskell no matter how shoddy will still have *more provenly verified correctness* than any imperative implementation of Bignum. Notice again how that correctness is not up to the ideal Platonic standard but simply up to your choice
<kluk>
of level of well-formed formulations that you choose to represent provably in your program. Any effort in that direction (of writing Bignum in FP) will be a step-wise effort towards the Platonic proof.
peterhil has quit [Quit: Must not waste too much time here...]
<kluk>
Regenaxer here is an example of a naive translation of an imperative program to FP to show that even then there are "free guarantees" we get just by virtue of starting out from FP: https://pastebin.com/aSWesJ4D
<Regenaxer>
ret
<Regenaxer>
All that is fine and good, but I cannot see if it has any value in praxis for me
<Regenaxer>
It does not help with "real" problems
<Regenaxer>
Just now a customer called me becaus mysteriolly a booking changed from positive to negative. Why? Cosmic radiation? User mistype? GUI glitch? Browser bug?
<Regenaxer>
These are "real" problems
<Regenaxer>
I don't care if some trivial aspect of the wole system in terms of Curry-Howard isomorphism
<Regenaxer>
(not that I have the faintest idea what that is ;)
peterhil has joined #picolisp
peterhil has quit [Client Quit]
peterhil has joined #picolisp
peterhil has quit [Client Quit]
peterhil has joined #picolisp
peterhil has quit [Client Quit]
peterhil has joined #picolisp
peterhil has quit [Client Quit]
peterhil has joined #picolisp
peterhil has quit [Remote host closed the connection]
peterhil has joined #picolisp
peterhil has quit [Client Quit]
peterhil has joined #picolisp
peterhil has quit [Remote host closed the connection]
peterhil has joined #picolisp
peterhil has quit [Client Quit]
peterhil has joined #picolisp
peterhil has quit [Client Quit]
<Regenaxer>
Looked it up
<Regenaxer>
I see. This is a nice sport discipline in itself
<Regenaxer>
So our goals are very different
<Regenaxer>
Interesting. English Wikipedia talks about proofs-as-programs while the german one talks about interpretation of types as logical expressions
<Regenaxer>
Again "types". From the Eric Normand podcast I learned that for Haskell types are soo very important, everything centers about type
<Regenaxer>
While in my mind type are rather irrelevant. I don't care about them particularly
m42e has quit [Quit: WeeChat 3.1]
m42e has joined #picolisp
<Regenaxer>
They are nice, in changing behavior either when interpreting data or sending messages to objects, but not more. They are in some corner of my brain at most
<Regenaxer>
Looks like I think much more in behavior than in static types
aw- has joined #picolisp
<Regenaxer>
Regenaxer did the right thing with picolisp?
<Regenaxer>
22:47 <kluk> it's funny you should say that. I feel like math modified my internal reward function to be "learn more math to be increasingly happier"
<Regenaxer>
22:47 <beneroth> oh nothing wrong with that
<Regenaxer>
22:47 <kluk> (and it's working)
<Regenaxer>
22:47 <beneroth> considering that he wanted it to be forth first :D
Regenaxer has quit [Excess Flood]
Regenaxer has joined #picolisp
<Regenaxer>
oops
<Regenaxer>
Something went wrong. Pressed the wrong key and got Excess Flood
<Regenaxer>
But where does this come from? "12:38 <Regenaxer> Regenaxer did the right thing with picolisp?"
<Regenaxer>
Was pasted somehow it seems
<Regenaxer>
also the following linis
<Regenaxer>
lines
freeemint has joined #picolisp
tankf33der has joined #picolisp
<tankf33der>
hi all
<Regenaxer>
Hi tankf33der!
<tankf33der>
i have a question about name spaces and chess application you wrote
<Regenaxer>
What says pil on a greater search depth?
<tankf33der>
this was a 3
<tankf33der>
i will try later
<tankf33der>
afk.
<Regenaxer>
But no mate in sight
<Regenaxer>
OK, see you!
<tankf33der>
Problem is both moves are ok
<tankf33der>
both math in one
<tankf33der>
Just fails in comparison
v88m has quit [Remote host closed the connection]
<Regenaxer>
I see
<Regenaxer>
Any move with the black tower is all right
<Regenaxer>
So the test needs perhaps a list of possible solutions
<Regenaxer>
If depth is 1, pil moves g2-f2++
matthias1 is now known as m42e
rick42 has quit [Remote host closed the connection]
wineroots has joined #picolisp
<cess11>
wow, that was a big log
<cess11>
i know a bit of the lingo and algebra and sometimes dig into such matters for intellectual stimulation but i've never ever had use for it when delivering to customers
<cess11>
some habits haskell style demands are great, but also kind of trivial, like pushing side effects to the edges/IO-interfaces
<cess11>
i've dabbled some in z3 and coq and while i understand applications in static analysis it's rarely possible in b2b or b2c, because there's a deadline
<cess11>
a criminal or nefarious state or cryptographer has all the time in the world and can wring out bugs in binaries through proof assistants and whatnot, but i don't because the customers i serve are always in a hurry, always in fierce competition i need to help them overcome
<cess11>
as i see it picolisp also has types but they're simple, convenient and don't get in the way of interactive problem solving
<cess11>
numbers and symbols are different and neither is a list
<cess11>
but when an interface in an application can deal with all of them predictably it's probably safe, close to 'proven correct'
<Regenaxer>
Good summary cess11
<beneroth>
yeah, that's my point, too
<beneroth>
bbl
v88m has joined #picolisp
* kluk
looks around
<kluk>
Regenaxer [06:11:45] <Regenaxer>All that is fine and good, but I cannot see if it has any value in praxis for me |> And that is entirely understandable. I went into FP based on my seeing others enjoy it and code equivalents to imperative programs with fewer lines of code. After that I understood that the fewer lines, the fewer places for bugs to hide. Then I understood that in Algebra we are forced to future-debug the program
<kluk>
accidental complexity of CPUs creeps up to my code and flips a sign - that is a problem for CPU makers to put their CPUs in faraday cages or whatever.
<kluk>
ahead-of-time, and I liked that idea. So I decided to invest my time into learning it in earnest equipped with a tentative idea of what my destination would look like. And after almost a decade studying FP and its Categorical foundations I can now say it paid off. It does help me with real problems. I have never had a number mysteriously change signs nor do I see neutrinos are real problems. I don't care if some trivial aspect of the
<kluk>
[07:30:06] <Regenaxer> Interesting. English Wikipedia talks about proofs-as-programs while the german one talks about interpretation of types as logical expressions |> in FP, Types are no longer Sets, but formal logic propositions. The Type Bool is a proposition that Booleans exist. The values True and False are proofs for the proposition Bool. True and False in FP are not "elements" of Bool - just witnesses.
<kluk>
[07:31:19] <Regenaxer>Again "types". From the Eric Normand podcast I learned that for Haskell types are soo very important, everything centers about type; While in my mind type are rather irrelevant. I don't care about them particularly |> Respectfully I would surmise that this is because you only have experience with nominal types from Set-theory which are indeed quite useless and hard to miss - indeed they are totally irrelevant as can
<kluk>
be proven by the fact that BLISS was C-without-types before C. Nominal types are just a puppet show for kids - there is no reality in them or usefulness in them at all.
<kluk>
[07:37:07] <Regenaxer>Looks like I think much more in behavior than in static types |> That is a key defining characteristic of Coalgebraists/OOPers/Imperative programmers/Packers/Simulation-oriented/Bisimilarity-reasoning/Top-down thinking people. I cannot think of defining a value without first knowing why it exists - what is it a witness to - what does it prove - why is it in my code in the first place - what part of my code does it
<kluk>
fulfill?
<kluk>
cess11 [14:29:21] <cess11>i've dabbled some in z3 and coq and while i understand applications in static analysis it's rarely possible in b2b or b2c, because there's a deadline |> Have you ever considered that this may be because you are a natural Top-down thinker (coalgebraist) and that for Bottom-up thinkers (algebraists) the opposite is true? Namely, I think the same way you do, but about FP: I don't have time to fiddle with SOLID,
<kluk>
GRASP, GoF Design Patterns, Dependency Injection, Agile, TDD, BDD, UML, SysML, OOA, OOD, RUP, XP, DSLs, DRY, CQRS, Tell don't ask, DDD, Enterprise Patterns, Anti-patterns, Code smells, Missing Concepts, I have an actual program to deliver to my client and he only cares about the computer being able to do it, not about the opinions of a bunch of self-proclaimed experts with not an ounce of theory behind them.
<kluk>
Since there is no coalgebraic theory currently being followed by any programming language, coding in non-FP amounts to coding in a paradigm that is just someone's opinion, whereas coding in FP amounts to coding in reality - using the mathematical patterns captured by many people in non-technical fields.
<kluk>
And neither I nor my clients have time to allow me to squander on studying people's opinions on something that they don't want to formalize (seemingly on purpose, so they can continue selling conference tickets and books).
<kluk>
cess11: I also do not have time to relearn how to do a post call for the umpteenth time just because the OOP fads of the day have moved. I don't have time to relearn Computer Science concepts just because the opinions of the loudest people currently in our field have changed. I don't have time to keep track of this gossipy sort of programming where we keep track of what other people are doing in the industry.
<kluk>
cess11: Where do you get all that time? :P
<kluk>
And more importantly, do your clients know they are paying you to study unfounded opinions?
<kluk>
Would you drive a car that was build based on opinions instead of algebraic physics?
<kluk>
Then why do you give your clients programs based on opinions instead of algebraic discipline?
<kluk>
Etc.
<kluk>
If there is an old way of building skyscrapers that makes them collapse and kill everyone sometimes, and a new way of building skyscrapers that makes them not collapse, how long should we allow the old builders to continue building until we transition to the new, more-guaranteed way of building skyscrapers?
<kluk>
There are still clients for whom you can build a wooden house and they will be happy. Those people are top-down thinkers. I would never accept living in a wooden house, just as I wouldn't accept living in a wedding-cake house - both are food, one for termites, one for people; they are not a bottom-up building material (but they are a top-down building material that then comes with all of the problems usual to top-down solutions).
mtsd has quit [Quit: Leaving]
freeemint has quit [Ping timeout: 244 seconds]
<cess11>
you make really weird assumptions about how i work and how customers are in the field i'm in
<cess11>
hard to tell if it's based on experience or not
<cess11>
one characteristic of haskell, f# and the like is that in a big project you constantly need to remind yourself of the decisions implicit in type design or you end up moving slowly when you need to return to a piece of code or module later
<cess11>
you can't read it out from the code and it's nearly impossible to write it in a way that can tell you many moons later wtf you did and why not another way, so you need to both do the deep thinking to achieve decency in the design and write thorough documentation immediately
<cess11>
if you're in finance or academia it's likely you can get away with formal models and don't have to modify them but if you need to figure out a way to satisfy three hundred different companies doing things slightly different from each other it's unlikely you'll keep up with them and their competitors
peterhil has joined #picolisp
wineroots has quit [Remote host closed the connection]